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