[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification nat
enrich
   nat-basic2
with
   

   
   
   functions  . - . : nat × nat → nat prio 8 left;
   predicates  . ≤ . : nat × nat;
               . > . : nat × nat;
               . ≥ . : nat × nat;
   
   
   
   

   

   axioms sub-base :  ⊦ m - 0 = m;
          sub-rec :  ⊦ m - n +1 = (m - n)-1;
          le-def :  ⊦ m ≤ n ↔ ¬ n < m;
          gr-def :  ⊦ m > n ↔ n < m;
          ge-def :  ⊦ m ≥ n ↔ ¬ m < n;

   

   
end enrich