Changeset 2051 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 12, 2012, 5:49:02 PM (7 years ago)
Author:
mulligan
Message:

Finished the Jmp case in the main theorem.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2047 r2051  
    11701170
    11711171lemma execute_1_ok: ∀cm.∀s.
    1172   let instr_pc_ticks ≝ fetch cm (program_counter … s) in
    1173     (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
     1172  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
     1173    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
    11741174      (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
    11751175        program_counter ? cm (execute_1 cm s) =
Note: See TracChangeset for help on using the changeset viewer.