Changeset 2192

Timestamp:

07/17/12 02:06:18 (10 months ago)

Author:

sacerdot

Message:

Shuffling around.

Location:

src/ASM

Files:

• Arithmetic.ma (modified) (1 diff)
• Assembly.ma (modified) (1 diff)

src/ASM/Arithmetic.ma

@@ -711 +711 @@
    add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
 
+(* CSC: corollary of add_bitvector_of_nat *)
+axiom add_overflow:
+ ∀n,m,r. m + r = 2^n →
+  add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n.
+
 example add_SO:
   ∀n: nat.

src/ASM/Assembly.ma

@@ -1047 +1047 @@
             [ #X <plus_n_Sm <plus_n_O @X
             | #abs @⊥
-              cut (∀n,m,r. m + r = 2^n → add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n)
-              [ cases daemon (* CSC: put in library *) ] #add_overflow
               <(bitvector_of_nat_inverse_nat_of_bitvector … ppc) in LT;
               >add_overflow [2: <plus_n_Sm <plus_n_O assumption ]