fmod NAT is
    sorts Nat NzNat Zero .
    subsorts Zero NzNat < Nat .
    op 0 : -> Zero .
    op s_ : Nat -> NzNat .
    op p_ : NzNat -> Nat .
    op _+_ : Nat Nat -> Nat [comm] .
    op _*_ : Nat Nat -> Nat [comm] .
    op _*_ : NzNat NzNat -> NzNat [comm] .
    op _>_ : Nat Nat -> Bool .
    op d : Nat Nat -> Nat [comm] .
    op quot : Nat NzNat -> Nat .
    op gcd : NzNat NzNat -> NzNat [comm] .
    vars N M : Nat . 
    vars N' M' : NzNat .
    eq p s N = N .
    eq N + 0 = N .
    eq (s N) + (s M) = s s (N + M) .
    eq N * 0 = 0 .
    eq (s N) * (s M) = s (N + (M + (N * M))) .
    eq 0 > M = false .
    eq N' > 0 = true .
    eq s N > s M = N > M .
    eq d(0, N) = N .
    eq d(s N, s M) = d(N, M) .
    ceq quot(N, M') = s quot(d(N, M'), M') if N > M' .
    eq quot(M', M') = s 0 .
    ceq quot(N, M') = 0 if M' > N .
    eq gcd(N', N') = N' .
    ceq gcd(N', M') =  gcd(d(N', M'), M') if N' > M' .
  endfm

  fmod INT is
    sorts Int NzInt .
    protecting NAT .
    subsort Nat < Int .
    subsorts NzNat < NzInt < Int .
    op -_ : Int -> Int .
    op -_ : NzInt -> NzInt .
    op _+_ : Int Int -> Int [comm] .
    op _*_ : Int Int -> Int [comm] .
    op _*_ : NzInt NzInt -> NzInt [comm] .
    op quot : Int NzInt -> Int .
    op gcd : NzInt NzInt -> NzNat [comm] .
    vars I J : Int . 
    vars I' J' : NzInt .
    vars N' M' : NzNat .
    eq - - I = I .
    eq - 0 = 0 .
    eq I + 0 = I .
    eq M' + (- M') = 0 .
    ceq M' + (- N') = - d(N', M') if N' > M' .
    ceq M' + (- N') = d(N', M') if M' > N' .         
    eq (- I) + (- J) = - (I + J) .
    eq I * 0 = 0 .
    eq I * (- J) = - (I * J) .
    eq quot(0, I') = 0 .
    eq quot(- I', J') = - quot(I', J') .
    eq quot(I', - J') = - quot(I', J') .
    eq gcd(- I', J') = gcd(I', J') .
  endfm
  
  fmod RAT is
    sorts Rat NzRat .
    protecting INT .
    subsort Int < Rat .
    subsorts NzInt < NzRat < Rat .
    op _/_ : Rat NzRat -> Rat .
    op _/_ : NzRat NzRat -> NzRat .
    op -_  : Rat -> Rat .
    op -_  : NzRat -> NzRat .
    op _+_ : Rat Rat -> Rat [comm] .
    op _*_ : Rat Rat -> Rat [comm] .
    op _*_ : NzRat NzRat -> NzRat [comm] .
    vars I' J' : NzInt . vars R S : Rat .
    vars R' S' : NzRat .
    eq R / (R' / S') = (R * S') / R' .
    eq (R / R') / S' = R / (R' * S') .
    ceq J' / I'
      = quot(J', gcd(J', I')) / quot(I', gcd(J', I'))
        if gcd(J', I') > s 0 .
    eq R / s 0 = R .
    eq 0 / R' = 0 .
    eq R / (- R') = (- R) / R' .
    eq - (R / R') = (- R) / R' .
    eq R + (S / R') = ((R * R') + S) / R' .
    eq R * (S / R') = (R * S) / R' .
  endfm