Top-level interactions for TypeNat:

TypeNat m

Top-level interactions for <=

m <= n   <=> {m <= n}
0 <= a   <=> True
a <= 0   <=> a ~ 0

Top-level interactions for +.

(m + n ~ k) <=> {m + n == k}
(m + a ~ n) <=> a ~ {n - m}    -- n >= m
(0 + a ~ b) <=> a ~ b
(a + b ~ 0) <=> (a ~ 0, b ~ 0)
(a + b ~ a) <=> (b ~ 0)
(a + b ~ b) <=> (a ~ 0)
(a + a ~ b) <=> (2 * a ~ b)
(a + m ~ b) <=> (m + a ~ b)    -- simple normalization cuts down on some rules

Top-level interactions for *.

(m * n ~ k) <=> {m * n == k}
(m * a ~ n) <=> a ~ { n / m }    -- m `divides` n, False otherwise

(0 * a ~ b) <=> b ~ 0
(1 * a ~ b) <=> a ~ b
(m * a ~ a) <=> a ~ 0            -- 2 <= m

(a * b ~ 1) <=> (a ~ 1, b ~ 1)
(a * a ~ b) <=> a ^ 2 ~ b

(a * m ~ b) <=> (m * a ~ b)      -- simple normalization cuts down on some rules

Top-level interactions for ^

(m ^ n ~ k) <=> {m ^ n == k}

(m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists, False otherwise
(1 ^ a ~ b) <=> b ~ 1
(m ^ a ~ a) <=> False           -- m /= 1

(a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists, False otherwise
(a ^ 0 ~ b) <=> b ~ 1
(a ^ 1 ~ b) <=> a ~ b
(a ^ m ~ a) <=> (a <= 1)        -- 2 <= m