Changeset 1404 for src/ASM/Arithmetic.ma
- Timestamp:
- Oct 18, 2011, 3:39:56 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Arithmetic.ma
r1207 r1404 141 141 λn,v. nat_of_bitvector_aux n O v. 142 142 143 axiom bitvector_of_nat_ok: 144 ∀n,x,y.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y. 145 (* if anyone wants to prove this... *) 146 143 147 definition two_complement_negation ≝ 144 148 λn: nat.
Note: See TracChangeset
for help on using the changeset viewer.