(fmod PEANO-NAT is
    sorts Boolean Nat NzNat .
    subsorts NzNat < Nat .
    ops false true : -> Boolean .
    op 0 : -> Nat .
    ops 1 2 3 4 5 6 7 : -> NzNat .
    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 -> Boolean .
    op _<_ : Nat Nat -> Boolean .
    op d : Nat Nat -> Nat [comm] .
    op quot : Nat NzNat -> Nat .
    op gcd : Nat Nat -> Nat [comm] .
    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 N < M = M > N .
    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' = true .
    eq quot(M',M') = s 0 .
    ceq quot(N,M') = 0 if M' > N = true .
    eq gcd(0,N) = 0 .
    eq gcd(N',N') = N' .
    ceq gcd(N',M') =  gcd(d(N',M'),M') if N' > M' = true .
    eq 1 = s 0 .
    eq 2 = s s 0 .
    eq 3 = s s s 0 .
    eq 4 = s s s s 0 .
    eq 5 = s s s s s 0 .
    eq 6 = s s s s s s 0 .
    eq 7 = s s s s s s s 0 .
   endfm)