Ignore:
Timestamp:
Jun 9, 2011, 10:45:16 AM (9 years ago)
Author:
sacerdot
Message:

Readable main theorem statement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r911 r912  
    15871587 >execute_1_pseudo_instruction_preserves_code_memory
    15881588 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
    1589  change with (? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) = ?)
    1590  whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    1591  generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
    1592  
    1593  cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
     1589 change with (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) ?) = ?)
     1590 change with (? = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory (\fst 〈cm,costs〉))) ?)
Note: See TracChangeset for help on using the changeset viewer.