[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