Changes between Version 9 and Version 10 of TypeNats/Interact1


Ignore:
Timestamp:
Dec 19, 2010 5:04:45 AM (5 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Interact1

    v9 v10  
    5454(a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists
    5555(a ^ 0 ~ b) <=> b ~ 1
    56 (1 ^ a ~ b) <=> b ~ 1
     56(a ^ 1 ~ b) <=> a ~ b
     57(1 ^ a ~ b) <=> b ~ 1
    5758(m ^ a ~ a) <=> False           -- m /= 1
     59(a ^ m ~ a) <=> (a <= 1)        -- 2 <= m
    5860}}}