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

(U11 1)
(U12 1)
(U13 1)
(U14 1)
(U15 1)
(U16 1)
(U21 1)
(U22 1)
(U23 1)
(U31 1)
(U32 1)
(U41 1)
(U51 1)
(U52 1)
(U61 1)
(U62 1)
(U63 1)
(U64 1)
(isNat )
(isNatKind )


)
(RULES
U11(tt,V1,V2) -> U12(isNatKind(V1),V1,V2)

U12(tt,V1,V2) -> U13(isNatKind(V2),V1,V2)

U13(tt,V1,V2) -> U14(isNatKind(V2),V1,V2)

U14(tt,V1,V2) -> U15(isNat(V1),V2)

U15(tt,V2) -> U16(isNat(V2))

U16(tt) -> tt

U21(tt,V1) -> U22(isNatKind(V1),V1)

U22(tt,V1) -> U23(isNat(V1))

U23(tt) -> tt

U31(tt,V2) -> U32(isNatKind(V2))

U32(tt) -> tt

U41(tt) -> tt

U51(tt,N) -> U52(isNatKind(N),N)

U52(tt,N) -> N

U61(tt,M,N) -> U62(isNatKind(M),M,N)

U62(tt,M,N) -> U63(isNat(N),M,N)

U63(tt,M,N) -> U64(isNatKind(N),M,N)

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

isNat(0) -> tt

isNat(plus(V1,V2)) -> U11(isNatKind(V1),V1,V2)

isNat(s(V1)) -> U21(isNatKind(V1),V1)

isNatKind(0) -> tt

isNatKind(plus(V1,V2)) -> U31(isNatKind(V1),V2)

isNatKind(s(V1)) -> U41(isNatKind(V1))

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

plus(N,s(M)) -> U61(isNat(M),M,N)
)