Changes between Version 1 and Version 2 of TypeNats/Rules


Ignore:
Timestamp:
Dec 15, 2010 6:01:18 PM (5 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Rules

    v1 v2  
    55}}} 
    66 
    7 Top-level interaction for +. 
     7Top-level interactions for {{{TypeNat}}}: 
     8{{{ 
     9TypeNat m 
     10}}} 
     11 
     12Top-level interactions for <= 
     13{{{ 
     14m <= n   <=> {m <= n} = True 
     150 <= a   <=> True 
     16a <= 0   <=> a ~ 0 
     17}}} 
     18 
     19Top-level interactions for +. 
    820{{{ 
    921(m + n ~ k) <=> {m + n} = k 
     
    1729(a + a ~ b) <=> (2 * a ~ b) 
    1830}}} 
     31 
     32Top-level 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 
     45Top-level 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}  -- m-th root of n exists 
     50(a ^ 0 ~ b) <=> b ~ 1 
     51(1 ^ a ~ b) <=> b ~ 1  
     52}}}