Changeset 2192


Ignore:
Timestamp:
Jul 17, 2012, 2:06:18 AM (5 years ago)
Author:
sacerdot
Message:

Shuffling around.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2177 r2192  
    711711   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
    712712
     713(* CSC: corollary of add_bitvector_of_nat *)
     714axiom add_overflow:
     715 ∀n,m,r. m + r = 2^n →
     716  add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n.
     717
    713718example add_SO:
    714719  ∀n: nat.
  • src/ASM/Assembly.ma

    r2191 r2192  
    10471047            [ #X <plus_n_Sm <plus_n_O @X
    10481048            | #abs @⊥
    1049               cut (∀n,m,r. m + r = 2^n → add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n)
    1050               [ cases daemon (* CSC: put in library *) ] #add_overflow
    10511049              <(bitvector_of_nat_inverse_nat_of_bitvector … ppc) in LT;
    10521050              >add_overflow [2: <plus_n_Sm <plus_n_O assumption ]
Note: See TracChangeset for help on using the changeset viewer.