wiki:TypeNats/LEQ

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

--

One step relation:

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

Transitivity and Cycles...