mod! BASIC-NAT {
 [Zero NzNat < Nat]
 op 0  : -> Zero
 op s_ : Nat -> NzNat
}

mod! NAT- {
 pr(BASIC-NAT)
 op _-_ : Nat Nat -> Nat 
 vars M N : Nat
 eq   0 -   N = 0 .
 eq s M -   0 = s M .
 eq s M - s N = M - N .
}

select NAT-
red s s s s 0 - s s 0 .
red s s 0 - s s s 0 .

mod! NAT>{
 pr(NAT-)
 op _>_ : Nat Nat -> Bool
 vars M N : Nat
 eq   0 >   N = false .
 eq s M >   0 = true .
 eq s M > s N = M > N .
}

select NAT>
red s s s 0 > s s 0 .
red s s s 0 > s s s 0 .
red s s 0 > s s s 0 .

mod! NAT-mod{
 pr(NAT>)
 op _mod_ : Nat NzNat -> Nat
 vars M N : Nat
 var P : NzNat
  eq P mod P = 0 .
 ceq N mod P = N if P > N .
 ceq N mod P = N - P mod P if N > P .
}

open NAT-mod
ops 10 11 12 : -> Nat .
eq 10 = s s s s s s s s s s 0 .
eq 11 = s 10 .
eq 12 = s 11 .
red 10 mod s s s 0 .
red 11 mod s s s 0 .
red 12 mod s s s 0 .
red 10 mod s s s s 0 .
red 11 mod s s s s 0 .
red 12 mod s s s s 0 .
close

mod! NAT-gcd {
 pr(NAT-mod)
 op gcd : Nat Nat -> Nat
 vars M N : Nat
  eq gcd(N, 0) = N .
  eq gcd(s N, s N) = s N .
 ceq gcd(M, s N) = gcd(s N, M mod s N) if M > s N .
 ceq gcd(M, s N) = gcd(s N, M) if s N > M .
}

open NAT-gcd
ops 10 12 15 : -> Nat .
eq 10 = s s s s s s s s s s 0 .
eq 12 = s s 10 .
eq 15 = s s s 12 .
red gcd(10, 12) .
red gcd(10, 15) .
red gcd(12, 15) .
close