Changeset 2027


Ignore:
Timestamp:
Jun 7, 2012, 5:53:27 PM (5 years ago)
Author:
mulligan
Message:

Got the main lemma to apply in the proof of main theorem again and closed the preinstruction goals.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2026 r2027  
    1 include "ASM/AssemblyProofSplitSplit.ma".
     1include "ASM/AssemblyProofSplit.ma".
    22
    33theorem main_thm:
     
    9797      ps ppc EQppc labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
    9898      EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
    99       (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1))) (refl …))
    100     cases daemon
     99      (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
     100      (refl …) ? (refl …))
     101    try assumption >assembly_refl <EQppc assumption
     102    check status_of_pseudo_status
    101103  |4:
    102104    #arg1
Note: See TracChangeset for help on using the changeset viewer.