Changeset 1928 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 9, 2012, 1:36:35 PM (8 years ago)
Author:
mulligan
Message:

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1910 r1928  
    10891089qed-. (*x Andrea: indexing takes ages here *)
    10901090
     1091lemma execute_1_ok_clock:
     1092  ∀cm.
     1093  ∀s.
     1094    clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
     1095  #cm #s cases (execute_1_ok cm s) #clock_assm #_ assumption
     1096qed-.
     1097
    10911098definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
    10921099  λticks,cm,s,instr,pc.
Note: See TracChangeset for help on using the changeset viewer.