Changes between Version 5 and Version 6 of TypeNats/LEQ


Ignore:
Timestamp:
Dec 24, 2010 4:14:23 AM (4 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/LEQ

    v5 v6  
    1 One step relation: 
     1One step relation (in a model M): 
    22{{{ 
    33(a + b ~ c) => (a <= c, b <= c) 
    4 (m * b ~ c) => (b <= c)                   -- 1 <= m 
     4(a * b ~ c) => (b <= c)                   -- M |- 1 <= a 
     5(a * b ~ c) => (a <= c)                   -- M |- 1 <= b 
    56(a ^ b ~ a) => (a <= 1) 
    6 (m ^ b ~ c) => (b <= c)                   -- 2 <= m 
     7(a ^ b ~ c) => (b <= c)                   -- M |- 2 <= a 
    78(0 ^ b ~ c) => (c <= 1) 
    8 (a ^ m ~ c) => (a <= c)                   -- 1 <= m 
     9(a ^ b ~ c) => (a <= c)                   -- M |- 1 <= b 
    910}}} 
    1011