Changeset 2899 for src/ASM/AssemblyProofSplitSplit.ma
- Timestamp:
- Mar 19, 2013, 12:33:13 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplitSplit.ma
r2278 r2899 45 45 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) = 46 46 status_of_pseudo_status M' … 47 (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps)sigma policy) ps program_counter_in_bounds) sigma policy.47 (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy. 48 48 #M #M' * #preamble #instr_list #program_in_bounds 49 49 @pair_elim #labels #cost #create_label_cost_refl
Note: See TracChangeset
for help on using the changeset viewer.