Changeset 925 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 9, 2011, 4:42:50 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r924 r925 1617 1617 [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H 1618 1618 #abs @⊥ normalize in abs; destruct (abs) ] 1619 * #labels #costs cases (code_memory … ps) #preamble #instr_list normalize nodelta; 1619 * #labels #costs generalize in match (refl … (code_memory … ps)) 1620 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ normalize nodelta; 1620 1621 generalize in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) *; normalize nodelta; 1621 1622 [ #EQ >EQ #_ #abs @⊥ normalize in abs; destruct (abs) ] … … 1631 1632 whd in match (\snd 〈final_pc,assembled〉) in H; 1632 1633 s s'' labels costs final_ppc final_pc; 1634 letin ps' ≝ (execute_1_pseudo_instruction ticks_of ps) 1633 1635 (* NICE STATEMENT HERE *) 1636 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; ps'; #ps' 1637 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ normalize nodelta; 1638 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) 1639 #pi #newppc normalize nodelta; * #instructions * 1640 cases pi normalize nodelta; 1641 [ (* Instruction *) 1642  (* Comment *) #comment #H1 #H2 #EQ normalize in H1 generalize in match (option_destruct_Some ??? H1) #K1 1643 >K1 in H2 whd in ⊢ (% → ?) #H2 whd in ⊢ (??%?) 1644  (* Cost *) 1645  (* Jmp *) 1646  (* Call *) 1647  (* Mov *) 1648 ] 1649 qed.
Note: See TracChangeset
for help on using the changeset viewer.