module SIMPLE-NAT {
	[ Zero NzNat < Nat ]
	op 0 : -> Zero
	op s : Nat -> NzNat
	op _+_ : Nat Nat -> Nat
	vars N N' : Nat
	eq 0 + N = N .
	eq N + s(N') = s(N + N') .
}

eof