Changeset 1037 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 23, 2011, 2:56:20 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1036 r1037 1980 1980 pbu)). 1981 1981 1982 lemma Some_Some_elim: 1983 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P. 1984 #T #x #y #P #H #K @H @option_destruct_Some // 1985 qed. 1986 1982 1987 theorem main_thm: 1983 1988 ∀M,M',ps,pol. … … 2030 2035 change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE; 2031 2036 >EQ2 whd in ⊢ (??(??%??)? → ?) #SAFE 2032 2033 XX 2034 2035 whd in match execute_1_pseudo_instruction 2036 2037 whd in match expand_pseudo_instruction normalize nodelta; 2038 whd in match execute_1_pseudo_instruction (*!!! USARE 0 !!!*) normalize nodelta; >EQ0 2039 normalize in match (\snd 〈preamble,instr_list〉); 2040 cases (fetch_pseudo_instruction instr_list (program_counter pseudo_assembly_program ps)) in MAP ⊢ % 2041 #pi #newppc normalize nodelta; #MAP 2042 cases pi in MAP; normalize nodelta; 2043 [2,3: (* Comment, Cost *) #ARG #MAP whd in ⊢ (% → ?) #H2 #EQ %[1,3:@0] 2044 generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M'; 2045 (* 2046 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 i 2047 n H2; whd in ⊢ (% → ?) 2048 #H2*) >(eq_bv_eq … H2) >EQ % 2037 whd in EQps':(???%); <EQ1 in EQps'; >EQ2 normalize nodelta 2038 generalize in match H1; -H1; generalize in match instructions -instructions 2039 * #instructions >EQ2 change in match (\fst 〈pi,newppc〉) with pi 2040 whd in match ticks_of normalize nodelta <EQ1 >EQ2 2041 cases pi in SAFE 2042 [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?) 2043 @Some_Some_elim #MAP #EQ3 @(Some_Some_elim ????? EQ3) #EQ3' 2044 whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?) 2045 #H2 #EQ %[1,3:@0] 2046 <MAP >(eq_bv_eq … H2) >EQ % 2049 2047 2050 2048 lemma main_thm0:
Note: See TracChangeset
for help on using the changeset viewer.