Ignore:
Timestamp:
Jun 23, 2011, 2:56:20 AM (8 years ago)
Author:
sacerdot
Message:

Main theorem: comments are working again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1036 r1037  
    19801980        pbu)).
    19811981
     1982lemma 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 //
     1985qed.
     1986
    19821987theorem main_thm:
    19831988 ∀M,M',ps,pol.
     
    20302035 change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE;
    20312036 >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 %
    20492047
    20502048lemma main_thm0:
Note: See TracChangeset for help on using the changeset viewer.