[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: even((* i)) ↔ i % 2 = 0;
      used for: ls, s;
      
      Odd: odd((* i)) ↔ i % 2 ≠ 0;
      used for: ls, s;
   
   
end enrich