(COMMENT generated from Maude module 'MYNAT' by 'nokinds' transformation)
(VAR M N V1 V2 X Z Y)
(STRATEGY CONTEXTSENSITIVE

(U11 1)
(U21 1)
(U31 1)
(U41 1)
(and 1)
(isNat )



)
(RULES
U11(tt,N) -> N

U21(tt,M,N) -> s(plus(N,M))

U31(tt) -> 0

U41(tt,M,N) -> plus(x(N,M),N)

and(tt,X) -> X

isNat(0) -> tt

isNat(plus(V1,V2)) -> and(isNat(V1),isNat(V2))

isNat(s(V1)) -> isNat(V1)

isNat(x(V1,V2)) -> and(isNat(V1),isNat(V2))

plus(N,0) -> U11(isNat(N),N)

plus(N,s(M)) -> U21(and(isNat(M),isNat(N)),M,N)

x(N,0) -> U31(isNat(N))

x(N,s(M)) -> U41(and(isNat(M),isNat(N)),M,N)
)