Changeset 1963 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
May 17, 2012, 2:23:37 AM (8 years ago)
Author:
sacerdot
Message:

More progress in restoring the original proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1955 r1963  
    544544    add … l (add … c r) = add … (add … l c) r.
    545545
     546axiom add_commutative:
     547  ∀n: nat.
     548  ∀l, r: BitVector n.
     549    add … l r = add … r l.
     550
    546551example add_SO:
    547552  ∀n: nat.
Note: See TracChangeset for help on using the changeset viewer.