Specification int-abs

[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,

enrich
   int-basic2
with
   functions 
       . - . : Int × Int → Int prio 8 left;
       ~ . : Int → Int;
       abs : Int → Int;
   
   predicates 
       . ≤ . : Int × Int;
       . > . : Int × Int;
       . ≥ . : Int × Int;
   
   variables 
       i : Int;
       j : Int;
   
   
   axioms 
      Sub-def: i + (j - i) = j;
      used for: s, ls;
      
      Minus-def: ~ i = 0 - i;
      used for: ls;
      
      Abs-neg: j < 0 → abs(j) = 0 - j;
      used for: ls, lc;
      
      Abs-pos: ¬ j < 0 → abs(j) = j;
      used for: s, ls;
      
      le-def: i ≤ j ↔ ¬ j < i;
      
      gr-def: i > j ↔ j < i;
      
      ge-def: i ≥ j ↔ ¬ i < j;
   
   
end enrich