Changeset 2209 for src/ASM/AssemblyProof.ma

Timestamp:

Jul 18, 2012, 2:56:12 PM (8 years ago)

Author:

mulligan

Message:

Closed major daemons in the supporting lemmas of the main lemma.

File:

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

src/ASM/AssemblyProof.ma

@@ -473 +473 @@
          ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
     | INDIRECT i ⇒
-       let d ≝ get_register … s [[false;false;i]] in
-       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M))
+        let d ≝ get_register … s [[false;false;i]] in
+        let address ≝ bit_address_of_register … s [[false;false;i]] in
+          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧
+            ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
     | EXT_INDIRECT _ ⇒ true
     | REGISTER r ⇒