Changes between Version 13 and Version 14 of TypeNats/Interact1


Ignore:
Timestamp:
Dec 19, 2010 5:55:17 PM (4 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Interact1

    v13 v14  
    1515(m + n ~ k) <=> {m + n == k} 
    1616(m + a ~ n) <=> a ~ {n - m}    -- n >= m 
    17 (a + m ~ n) <=> a ~ {n - m}    -- n >= m 
    1817(0 + a ~ b) <=> a ~ b 
    19 (a + 0 ~ b) <=> a ~ b 
    2018(a + b ~ 0) <=> (a ~ 0, b ~ 0) 
    2119(a + b ~ a) <=> (b ~ 0) 
     
    2826{{{ 
    2927(m * n ~ k) <=> {m * n == k} 
    30 (m * a ~ n) <=> a ~ {n / m}     -- m `divides` n 
    31 (a * m ~ n) <=> a ~ {n / m}     -- m `divides` n 
     28(m * a ~ n) <=> {m / g} * a ~ {n / g}     -- g = gcd m n, 2 <= g 
     29 
    3230(0 * a ~ b) <=> b ~ 0 
    33 (a * 0 ~ b) <=> b ~ 0 
    3431(1 * a ~ b) <=> a ~ b 
    35 (a * 1 ~ b) <=> a ~ b 
     32(m * a ~ a) <=> a ~ 0                     -- 2 <= m 
     33 
    3634(a * b ~ 1) <=> (a ~ 1, b ~ 1) 
    3735(a * a ~ b) <=> a ^ 2 ~ b 
    38 (m * a ~ a) <=> a ~ 0            -- 2 <= m 
     36 
     37(a * m ~ b) <=> (m * a ~ b)      -- simple normalization cuts down on some rules 
    3938}}} 
    4039