Changes between Version 2 and Version 3 of TypeNats/Interact2


Ignore:
Timestamp:
Dec 16, 2010 2:00:20 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Interact2

    v2 v3  
    1010 
    1111m + b ~ c 
    12   n + d ~ c <=> d ~ {m - n} + b   -- m >= n 
    13   n + d ~ c <=> b ~ {n - m} + d   -- n >= m 
     12  n + d ~ c <=> {m - n} + b ~ d  -- n <= m 
     13  n + d ~ c <=> {n - m} + d ~ b  -- m >=m 
    1414}}} 
     15 
     16 
     17{{{ 
     18a * b ~ c 
     19  a * b ~ d <=> c ~ d 
     20  b * a ~ d <=> c ~ d 
     21 
     22m * b ~ c 
     23  n * b ~ c <=> (b ~ 0, c ~ 0)    -- m /= n 
     24  n * d ~ c <=> {m / g} * b ~ {n / g} * d    -- g = gcd m n, g /= 1, replaces both assumptions 
     25}}}