Ignore:
Timestamp:
Nov 26, 2010, 3:33:32 PM (9 years ago)
Author:
mulligan
Message:

Added axioms for addition for claudio.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVector.ma

    r275 r313  
    217217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    218218    ].
     219   
     220naxiom half_add:
     221  ∀n: Nat.
     222  ∀b, c: BitVector n.
     223    Bool × (BitVector n).
     224   
     225naxiom full_add:
     226  ∀n: Nat.
     227  ∀b, c: BitVector n.
     228  ∀d: Bit.
     229    Bool × (BitVector n).
Note: See TracChangeset for help on using the changeset viewer.