Changeset 2183 for src/ASM/Test.ma
- Timestamp:
- Jul 13, 2012, 5:03:15 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2181 r2183 11 11 ∀policy. 12 12 ∀s, s'. 13 ∀new_ppc. 13 ∀new_ppc, new_ppc'. 14 sigma new_ppc = new_ppc' → 14 15 status_of_pseudo_status M cm s sigma policy = s' → 15 16 set_program_counter (BitVectorTrie Byte 16) 16 17 (code_memory_of_pseudo_assembly_program cm sigma policy) 17 s' 18 (sigma new_ppc) = 18 s' new_ppc' = 19 19 status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy. 20 #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl // 20 #M #cm #sigma #policy #s #s' #new_ppc #new_ppc' 21 #new_ppc_refl #s_refl <new_ppc_refl <s_refl // 21 22 qed. 22 23
Note: See TracChangeset
for help on using the changeset viewer.