Ignore:
Timestamp:
Dec 1, 2010, 1:10:53 PM (10 years ago)
Author:
mulligan
Message:

less axioms

File:
1 edited

Legend:

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

    r349 r350  
    147147nqed.
    148148
    149 ndefinition full_add:
    150   ∀n: Nat.
    151   ∀b, c: BitVector n.
    152   ∀d: Bit.
    153     fold_left_i ? ? (
    154       λb1, b2: Bool.
    155       λd.
     149ndefinition full_add ≝
     150  λn: Nat.
     151  λb, c: BitVector n.
     152  λd: Bit.
     153    fold_right2_i ? ? ? (
     154      λn.
     155       λb1, b2: Bool.
     156        λd: Bit × (BitVector n).
    156157        let 〈c1,r〉 ≝ d in
    157158          〈inclusive_disjunction (conjunction b1 b2)
    158159                                 (conjunction c1 (inclusive_disjunction b1 b2)),
    159            (exclusive_disjunction (exclusive_disjunction b1 b2) c1) :: r〉)
    160              b c 〈c, [ ]〉.
    161    
    162     (fun b1 b2 (c,r) -> b1 & b2 || c & (b1 || b2),xor (xor b1 b2) c::r) l r (c,[])
     160           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
     161     〈d, [[ ]]〉 ? b c.
    163162   
    164163ndefinition half_add ≝
Note: See TracChangeset for help on using the changeset viewer.