Changeset 2258 for src/ASM/Test.ma

Timestamp:

Jul 25, 2012, 1:47:01 PM (9 years ago)

Author:

sacerdot

Message:

1. lemma generalized
2. automation replaced with expansion to make everything faster

File:

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

src/ASM/Test.ma

@@ -982 +982 @@
   ∀cm.
   ∀ps.
-  ∀addr: [[dptr]].
-  ∀v: Word.
+  ∀addr,addr': [[dptr]].
+  ∀v,v': Word.
   ∀M. ∀sigma. ∀policy. ∀s'.
     status_of_pseudo_status M cm ps sigma policy = s' →
+    v=v' → addr=addr' →
       set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
-      s' v addr =
+      s' v' addr' =
       status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
-  #cm #ps #addr #v #M #sigma #policy #s' #s_refl <s_refl
+  #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl
+  <addr_refl #v_refl <v_refl 
   @(subaddressing_mode_elim … addr)
   whd in match set_arg_16; normalize nodelta