Changeset 2127 for src/ASM/AssemblyProofSplitSplit.ma

Timestamp:

Jun 27, 2012, 4:59:10 PM (9 years ago)

Author:

sacerdot

Message:

Last daemon closed

File:

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

src/ASM/AssemblyProofSplitSplit.ma

@@ -203 +203 @@
     |2:
       whd in ⊢ (??(?%%)%);
-      cut (∃b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11. address = [[b1;b2;b3;b4;b5;b6;b7;b8;b9;b10;b11]])
-      [1:
-        cases daemon (* XXX: easy but massive proof, move into separate lemma *)
-      |2:
-        * * * * * * * #b4 * #b5
-        * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
-        normalize in match (fetch ??); <plus_n_Sm @eq_f
-        @commutative_plus
-      ]
+      cases (bitvector_11_cases address)
+      * * * * * * #b4 * #b5
+      * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
+      normalize in match (fetch ??); <plus_n_Sm @eq_f
+      @commutative_plus
     ]
   |5: (* Call *)