fmod NUMBERS is
   sorts Nat NzNat Nat3 .
   subsort NzNat < Nat .

   op zero : -> Nat .
   op s_ : Nat -> NzNat .
   op _+_ : Nat Nat -> Nat [assoc comm] .
   op _+_ : NzNat NzNat -> NzNat [assoc comm] .
   ops 0 1 2 : -> Nat3 .
   op _+_ : Nat3 Nat3 -> Nat3 [comm] .
   op i : Nat3 -> Nat .

   vars N M : Nat .
   var N3 : Nat3 .

   eq N + zero = N .
   eq N + s M = s (N + M) .
   eq N3 + 0 = N3 .
   eq 1 + 1 = 2 .
   eq 1 + 2 = 0 .
   eq 2 + 2 = 1 .
   eq i(0) = zero .
   eq i(1) = s zero .
   eq i(2) = s s zero .
endfm

red i(2 + (2 + 1)) + i((2 + 1) + 1) .
***(
reduce in NUMBERS : i(1 + (1 + 2)) + i(2 + (1 + 2)) .
rewrites: 7 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s s s zero
)