[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-abs
enrich
   real-basic
with
   functions 
       . - . : Real × Real → Real prio 8 left;
       abs : Real → Real;
   
   predicates 
       . ≤ . : Real × Real;
       . > . : Real × Real;
       . ≥ . : Real × Real;
   
   variables 
       r : Real;
       i : Int;
       j : Int;
   
   
   axioms 
      sub-def: r - r0 = r + ~ r0;
      used for: s, ls;
      
      Abs-neg: r < 0.r → abs(r) = ~ r;
      used for: ls, lc;
      
      Abs-pos: ¬ r < 0.r → abs(r) = r;
      used for: s, ls;
      
      le-def: r ≤ r0 ↔ ¬ r0 < r;
      used for: ls, ss;
      comment: ≤ in suc is replaced with < in ant;
      
      gr-def: r > r0 ↔ r0 < r;
      used for: ls, s;
      comment: > is always replaced with <;
      
      ge-def: r ≥ r0 ↔ r0 ≤ r;
      used for: ls, ss;
      comment: ≤ in suc is always replaced with ≤;
   
   theorems 
      le-lem: r < r0 ↔ ¬ r0 ≤ r;
      used for: ss;
      comment:  < in suc is replaced with ≤ in ant;
   
   
end enrich