Changes between Version 1 and Version 2 of TypeNats/Rules
 Timestamp:
 Dec 15, 2010 6:01:18 PM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Rules
v1 v2 5 5 }}} 6 6 7 Toplevel interaction for +. 7 Toplevel interactions for {{{TypeNat}}}: 8 {{{ 9 TypeNat m 10 }}} 11 12 Toplevel interactions for <= 13 {{{ 14 m <= n <=> {m <= n} = True 15 0 <= a <=> True 16 a <= 0 <=> a ~ 0 17 }}} 18 19 Toplevel interactions for +. 8 20 {{{ 9 21 (m + n ~ k) <=> {m + n} = k … … 17 29 (a + a ~ b) <=> (2 * a ~ b) 18 30 }}} 31 32 Toplevel interactions for *. 33 {{{ 34 (m * n ~ k) <=> {m * n} = k 35 (m * a ~ n) <=> a ~ {n / m}  m `divides` n 36 (a * m ~ n) <=> a ~ {n / m}  m `divides` n 37 (0 * a ~ b) <=> b ~ 0 38 (a * 0 ~ b) <=> b ~ 0 39 (1 * a ~ b) <=> a ~ b 40 (a * 1 ~ b) <=> a ~ b 41 (a * b ~ 1) <=> (a ~ 1, b ~ 1) 42 (a + a ~ b) <=> 2 ^ a ~ b 43 }}} 44 45 Toplevel interactions for ^ 46 {{{ 47 (m ^ n ~ k) <=> {m ^ n} = k 48 (m ^ a ~ n) <=> a ~ {log m n}  log (base m) of n exists 49 (a ^ m ~ n) <=> a ~ {root m n}  mth root of n exists 50 (a ^ 0 ~ b) <=> b ~ 1 51 (1 ^ a ~ b) <=> b ~ 1 52 }}}