Changes between Version 10 and Version 11 of TypeNats/Axioms


Ignore:
Timestamp:
Dec 29, 2010 9:17:48 PM (5 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Axioms

    v10 v11  
    2727addDef:      m + n ~ k     -- if "m + n == k"
    2828addUnit:     0 + t ~ t
    29 addAssoc:    (r + s) + t ~ r + (s + t)
    30 addCommutes: t + s ~ s + t
    31 addCancel:   (r + s ~ r + t) => s ~ t
     29addAssoc:    (r + s) + t ~ r + (s + t)                   | (r + s = u, s + t = v, r + v = w1, u + t = w2) => w1 ~ w2
     30addCommutes: t + s ~ s + t                               | (r + s ~ t) => (s + r ~ t)
     31addCancel:   (r + s ~ r + t) => s ~ t                    | (r + s ~ u, r + t = u) => s ~ t
    3232}}}
    3333