wiki:TypeNats/LEQ

Version 5 (modified by diatchki, 3 years ago) (diff)

--

One step relation:

(a + b ~ c) => (a <= c, b <= c)
(m * b ~ c) => (b <= c)                   -- 1 <= m
(a ^ b ~ a) => (a <= 1)
(m ^ b ~ c) => (b <= c)                   -- 2 <= m
(0 ^ b ~ c) => (c <= 1)
(a ^ m ~ c) => (a <= c)                   -- 1 <= m

Transitivity and Cycles...