[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 int-min
enrich
   int-div
with
   functions 
       sgn : int → int;
       max : int × int → int;
       min : int × int → int;
   
   predicates 
       odd : int;
       even : int;
   
   variables 
       i : int;
       j : int;
   
   
   axioms 
      Max-right: j < i → max(j, i) = i;
      used for: s, ls, lc;
      
      Max-left: ¬ j < i → max(j, i) = j;
      used for: s, ls;
      
      Min-left: j < i → min(j, i) = j;
      used for: s, ls, lc;
      
      Min-right: ¬ j < i → min(j, i) = i;
      used for: s, ls;
      
      Sign-neg: j < 0 → sgn(j) = 0 -1;
      used for: ls, lc;
      
      Sign-pos: ¬ j < 0 → sgn(j) = 0 +1;
      used for: ls;
      
      even-def: even(i) ↔ (∃ j. i = j + j);
      
      odd-def: odd(i) ↔ (∃ j. i = j + j + 1);
   
   
end enrich