[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-multdiv
enrich
   real-abs, 
   real-min-max
with
   functions 
       . * . : Real × Real → Real prio 10 right;
   
   variables 
       r : Real;
       i : Int;
       j : Int;
   
   partial functions 
       . ^-1 : Real → Real with λ r. r ≠ 0.r;
       . / . : Real × Real → Real prio 11 right with λ r0, r. r ≠ 0.r;
   
   axioms 
      div-def: r ≠ 0.r ⊦ r0 / r = r0 * r.^-1;
      used for: s, ls;
      
      inv-def: r * r.^-1 = 1.r;
      used for: s, ls;
      
      two-def: 2.r = 1.r + 1.r;
      
      mult-one: 1.r * r = r;
      used for: s, ls;
      
      mult-com: r * r0 = r0 * r;
      used for: s, ls;
      
      mult-ass: (r * r0) * r1 = r * r0 * r1;
      used for: s, ls;
      
      distr: r * (r0 + r1) = r * r0 + r * r1;
      used for: ls;
      comment: used as local simprule only;
      
      order: r > 0.r ∧ r0 > 0.r → r * r0 > 0.r;
   
   theorems 
      mult-zero: 0.r * r = 0.r;
      used for: s, ls;
   
   
end enrich