[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-basic
enrich
   int-abs
with
   sorts Real;
   functions 
       . + . : Real × Real → Real;
       ~ . : Real → Real;
       . .r : Int → Real;
      comment: embedding of int's into reals;
   
   predicates 
       . < . : Real × Real;
   
   variables 
       r : Real;
       i : Int;
       j : Int;
   
   
   axioms 
      neg: ~ r + r = 0.r;
      used for: s, ls;
      
      add-comm: r + r0 = r0 + r;
      used for: s, ls;
      
      add-zero: r + 0.r = r;
      used for: s, ls;
      
      add-assoc: (r + r0) + r1 = r + r0 + r1;
      used for: s, ls;
      
      less-add-cancel-l: r + r0 < r + r1 ↔ r0 < r1;
      used for: s, ls;
      
      irref: ¬ r < r;
      used for: s, ls;
      
      trans: r < r0 ∧ r0 < r1 → r < r1;
      used for: f, lf;
      
      total: r < r0 ∨ r = r0 ∨ r0 < r;
      
      ls-num: i.r < j.r ↔ i < j;
      used for: s, ls;
      
      eqint-num: i.r = j.r ↔ i = j;
      used for: s, ls;
      
      eqint-add: (* i).r + (* j).r = (i + j).r;
      used for: s, ls;
   
   
end enrich