Changeset 1946 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
May 15, 2012, 12:01:30 AM (8 years ago)
Author:
sacerdot
Message:

\snd half_add => add everywhere

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1934 r1946  
    529529    full_add n b c false.
    530530
    531 example half_add_SO:
     531definition add ≝
     532  λn: nat.
     533  λl, r: BitVector n.
     534    \snd (half_add n l r).
     535
     536axiom add_zero:
     537  ∀n: nat.
     538  ∀l: BitVector n.
     539    l = add n l (zero …).
     540
     541axiom add_associative:
     542  ∀n: nat.
     543  ∀l, c, r: BitVector n.
     544    add … l (add … c r) = add … (add … l c) r.
     545
     546example add_SO:
    532547 ∀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).
    534549 cases daemon.
    535550qed.
Note: See TracChangeset for help on using the changeset viewer.