[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 real-min-max
enrich
   real-abs
with
   functions 
       max : Real × Real → Real;
       min : Real × Real → Real;
   
   variables 
       r : Real;
       i : Int;
   
   
   axioms 
      Max-left: r1 < r2 → max(r1, r2) = r2;
      used for: s, ls, lc;
      
      Max-right: ¬ r1 < r2 → max(r1, r2) = r1;
      used for: s, ls;
      
      Min-left: r1 < r2 → min(r1, r2) = r1;
      used for: s, ls, lc;
      
      Min-right: ¬ r1 < r2 → min(r1, r2) = r2;
      used for: s, ls;
   
   
end enrich