Changeset 2183 for src/ASM/Test.ma

Timestamp:

Jul 13, 2012, 5:03:15 PM (8 years ago)

Author:

mulligan

Message:

More progress on main lemma proof.

File:

• src/ASM/Test.ma (modified) (1 diff)

src/ASM/Test.ma

@@ -11 +11 @@
   ∀policy.
   ∀s, s'.
-  ∀new_ppc.
+  ∀new_ppc, new_ppc'.
+    sigma new_ppc = new_ppc' →
     status_of_pseudo_status M cm s sigma policy = s' →
     set_program_counter (BitVectorTrie Byte 16)
       (code_memory_of_pseudo_assembly_program cm sigma policy)
-      s'
-      (sigma new_ppc) =
+      s' new_ppc' =
     status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
-  #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
+  #M #cm #sigma #policy #s #s' #new_ppc #new_ppc'
+  #new_ppc_refl #s_refl <new_ppc_refl <s_refl //
 qed.