Changeset 1946 for src/ASM/Arithmetic.ma
 Timestamp:
 May 15, 2012, 12:01:30 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r1934 r1946 529 529 full_add n b c false. 530 530 531 example half_add_SO: 531 definition add ≝ 532 λn: nat. 533 λl, r: BitVector n. 534 \snd (half_add n l r). 535 536 axiom add_zero: 537 ∀n: nat. 538 ∀l: BitVector n. 539 l = add n l (zero …). 540 541 axiom add_associative: 542 ∀n: nat. 543 ∀l, c, r: BitVector n. 544 add … l (add … c r) = add … (add … l c) r. 545 546 example add_SO: 532 547 ∀pc. 533 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).548 add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1) = bitvector_of_nat … (S pc). 534 549 cases daemon. 535 550 qed.
Note: See TracChangeset
for help on using the changeset viewer.