enrich
   int-gcd

with
   

   sorts rationals;
   constants  0r : rationals;
              1r : rationals;
   functions  rational : int × int → rationals;
              . .num : rationals → int;
             comment: the numerator (i in i/j) carries the sign.;
              . .denom : rationals → int;
             comment: denumerator (j in i/j), always > 0.;
              . + . : rationals × rationals → rationals;
              . - . : rationals × rationals → rationals prio 8 left;
              . * . : rationals × rationals → rationals prio 10 right;
              . / . : rationals × rationals → rationals prio 11 right;
              ~ . : rationals → rationals;
              abs : rationals → rationals;
   predicates  . < . : rationals × rationals;
               . ≤ . : rationals × rationals;
               . > . : rationals × rationals;
               . ≥ . : rationals × rationals;
   
   variables  ri : rationals;
              rj : rationals;
              ri0 : rationals;
              ri1 : rationals;
              rj0 : rationals;
              rj1 : rationals;
   
   

   induction rationals generated by rational;

   axioms Equality :  ⊦ ri = rj ↔ ri.num = rj.num ∧ ri.denom = rj.denom;
          numerator-zero :  ⊦ rational(0, j).num = 0;
          used for: ls;
          numerator-pos :  ⊦ i ≠ 0 ∧ 0 < j → rational(i, j).num = i / gcd(i, j);
          used for: ls;
          comment: gcd is always positive.;
          numerator-neg1 :  ⊦ 0 < i ∧ j < 0 → rational(i, j).num = ~(i / gcd(i, j));
          used for: ls;
          numerator-neg2 :  ⊦ i < 0 ∧ j < 0 → rational(i, j).num = abs(i) / gcd(i, j);
          used for: ls;
          numerator-zero-den :  ⊦ i ≠ 0 → rational(i, 0).num = i;
          used for: ls;
          denominator-zero :  ⊦ rational(0, j).denom = 1;
          used for: ls;
          denominator-pos :  ⊦ i ≠ 0 ∧ j ≠ 0 → rational(i, j).denom = abs(j) / gcd(i, j);
          used for: ls;
          denominator-zero-den :  ⊦ i ≠ 0 → rational(i, 0).denom = 1;
          used for: ls;
          zero-def :  ⊦ 0r = rational(0, 1);
          used for: ls;
          one-def :  ⊦ 1r = rational(1, 1);
          used for: ls;
          add-def :  ⊦ ri + rj = rational(ri.num * rj.denom + ri.denom * rj.num, ri.denom * rj.denom);
          used for: ls;
          sub-def :  ⊦ ri - rj = rational(ri.num * rj.denom - ri.denom * rj.num, ri.denom * rj.denom);
          used for: ls;
          mult-def :  ⊦ ri * rj = rational(ri.num * rj.num, ri.denom * rj.denom);
          used for: ls;
          div-def :  ⊦ ri / rj = rational(ri.num * rj.denom, ri.denom * rj.num);
          used for: ls;
          neg-def :  ⊦ ~ ri = 0r - ri;
          used for: ls;
          abs-def :  ⊦ abs(ri) = rational(abs(ri.num), ri.denom);
          used for: ls;
          Ls-def :  ⊦ ri < rj ↔ (ri - rj).num < 0;
          used for: ls;
          Le-def :  ⊦ ri ≤ rj ↔ ¬ rj < ri;
          used for: ls;
          Gr-def :  ⊦ ri > rj ↔ rj < ri;
          used for: s, ls;
          Ge-def :  ⊦ ri ≥ rj ↔ ¬ ri < rj;
          used for: s, ls;

   

   
end enrich