 Timestamp:
 Jul 17, 2012, 2:06:18 AM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2177 r2192 711 711 add n (bitvector_of_nat n m1) (bitvector_of_nat n m2). 712 712 713 (* CSC: corollary of add_bitvector_of_nat *) 714 axiom 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 713 718 example add_SO: 714 719 ∀n: nat. 
src/ASM/Assembly.ma
r2191 r2192 1047 1047 [ #X <plus_n_Sm <plus_n_O @X 1048 1048  #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_overflow1051 1049 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc) in LT; 1052 1050 >add_overflow [2: <plus_n_Sm <plus_n_O assumption ]
Note: See TracChangeset
for help on using the changeset viewer.