Changes between Version 2 and Version 3 of TypeNats/Axioms
 Timestamp:
 Nov 27, 2010 9:09:00 PM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Axioms
v2 v3 5 5 The actual algorithm for constructing the evidence is described as set of rules (interactions) which are described separately. 6 6 7 The "*Def" axioms bellow look a bit odd but all they are saying is that the predicates which are being defined behave like their corresponding mathematical operations. 7 8 8 9 9 10 Notation: 10 11 {{{ 11 m,n:literals of kind Nat12 k,m,n: literals of kind Nat 12 13 r,s,t: arbitrary terms of kind Nat 13 {expr}:14 14 }}} 15 15 … … 24 24 Addition: 25 25 {{{ 26 addDef: m + n ~ {m + n}26 addDef: m + n ~ k  if "m + n == k" 27 27 addUnit: 0 + t ~ t 28 28 addAssoc: (r + s) + t ~ r + (s + t) … … 33 33 Multiplication: 34 34 {{{ 35 mulDef: m * n ~ {m * n}35 mulDef: m * n ~ k  if "m * n == k" 36 36 mulUnit: 1 * t ~ t 37 37 mulAssoc: (r * s) * t ~ r * (s * t)