wiki:TypeNats/LEQ

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

--

One step relation (in a model M):

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

Transitivity and Cycles...