Changeset 2282 for src/ASM/AssemblyProofSplit.ma
- Timestamp:
- Jul 31, 2012, 6:08:00 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2279 r2282 1157 1157 ] 1158 1158 ] 1159 | *)12: (* JC *)1159 |12: (* JC *) 1160 1160 >EQP -P normalize nodelta 1161 1161 whd in match assembly_1_pseudoinstruction; normalize nodelta … … 1923 1923 cases bitone #bit_one_seven_bits_refl normalize nodelta 1924 1924 [ @eq_bv_elim #seven_bits_refl normalize nodelta 1925 | inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]1925 | FUFFA inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry] 1926 1926 #lookup_from_internal_ram_refl ] 1927 @Some_Some_elim #Mrefl destruct(Mrefl)#fetch_many_assm %{1}1927 @Some_Some_elim #Mrefl <Mrefl -M' #fetch_many_assm %{1} 1928 1928 whd in ⊢ (??%?); 1929 1929 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1930 whd in ⊢ (??%?); 1931 @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta 1932 @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl)) 1933 [1,3,5,7: 1934 @eq_f2 try % 1935 @(pose … (set_clock ????)) #status #status_refl 1936 @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl -status_refl try % 1937 @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl % 1938 |*: 1939 >EQs >EQticks <instr_refl 1940 @(write_at_stack_pointer_status_of_pseudo_status 〈low,high,accA〉) 1941 [2,4,6,8: @set_8051_sfr_status_of_pseudo_status try % 1942 | >get_8051_sfr_set_8051_sfr 1943 cut (new_sp = (add … (get_8051_sfr … ps SFR_SP) (bitvector_of_nat … 1))) 1944 [ >(pair_destruct_2 ????? (sym_eq … carry_new_sp_refl)) 1945 change with (add ??? = ?); @eq_f2 try % 1946 cases daemon (*CSC: use @get_8051_sfr_status_of_pseudo_status*) ] #EQnew_sp 1947 >EQnew_sp 1948 @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram 1949 1950 1951 XXX 1952 (*CSC: lemma here*) 1953 cases accA 1954 whd in match overwrite_or_delete_from_internal_ram; normalize nodelta 1955 [ whd whd in match delete_from_internal_ram; normalize nodelta 1956 @pair_elim #bit_one 1957 | 1958 ] 1959 | 1960 | 1961 ] 1930 whd in match execute_1_0; normalize nodelta 1931 whd in match execute_1_preinstruction; normalize nodelta 1932 >bit_one_seven_bits_refl 1933 [ alias id "write_at_stack_pointer_accA" = "cic:/matita/cerco/ASM/Test3/write_at_stack_pointer_accA.def(29)". 1934 >seven_bits_refl 1935 @(write_at_stack_pointer_status_of_pseudo_status_accA … 〈low,high,accA〉) 1936 [ @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y 1937 try % 1938 change with (add ??? = ?); @eq_f2 try % 1939 @(pose … (set_clock ????)) #status #status_refl 1940 @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl % 1941 | >EQs /demod nohyps/ >add_commutative % ] 1942 | 1943 | 1944 | 1962 1945 ] 1963 1946 |43: (* POP *)
Note: See TracChangeset
for help on using the changeset viewer.