[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-inf
specification
   using nat
   data types 
      Natinf = ⌜ . ⌝(. n : Nat)
             | ∞
             ;
   
   variables 
       n∞ : Natinf;
       n : Nat;
   
   functions 
       . + . : Natinf × Natinf → Natinf;
       min : Natinf × Natinf → Natinf;
   
   predicates 
       . < . : Natinf × Natinf;
   
   variables 
       m : Nat;
       n : Nat;
       n∞ : Natinf;
   
   axioms 
      add-fin: ⌜m + n⌝  = ⌜m⌝  + ⌜n⌝ ;
      used for: ls, s;
      
      add-inf1: ∞ + ⌜m⌝  = ∞;
      used for: ls, s;
      
      add-inf2: ⌜m⌝  + ∞ = ∞;
      used for: ls, s;
      
      add-inf: ∞ + ∞ = ∞;
      used for: ls, s;
      
      less-fin: ⌜m⌝  < ⌜n⌝  ↔ m < n;
      
      less-inf2: ⌜m⌝  < ∞;
      
      less-inf1: ¬ ∞ < n∞;
      
      min-def: min(n∞, n∞0) = (n∞ < n∞0 ⊃ n∞;n∞0);
   
   
end specification