Changes between Version 15 and Version 16 of TypeNats/Interact1


Ignore:
Timestamp:
Dec 19, 2010 6:00:20 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Interact1

    v15 v16  
    2626{{{ 
    2727(m * n ~ k) <=> {m * n == k} 
    28 (m * a ~ n) <=> a ~ { n / m }  -- m `divides` n, False otherwise 
     28(m * a ~ n) <=> a ~ { n / m }    -- m `divides` n, False otherwise 
    2929 
    3030(0 * a ~ b) <=> b ~ 0 
    3131(1 * a ~ b) <=> a ~ b 
    32 (m * a ~ a) <=> a ~ 0                     -- 2 <= m 
     32(m * a ~ a) <=> a ~ 0            -- 2 <= m 
    3333 
    3434(a * b ~ 1) <=> (a ~ 1, b ~ 1) 
     
    4242(m ^ n ~ k) <=> {m ^ n == k} 
    4343 
    44 (m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists 
     44(m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists, False otherwise 
    4545(1 ^ a ~ b) <=> b ~ 1 
    4646(m ^ a ~ a) <=> False           -- m /= 1 
    4747 
    48 (a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists 
     48(a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists, False otherwise 
    4949(a ^ 0 ~ b) <=> b ~ 1 
    5050(a ^ 1 ~ b) <=> a ~ b