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

(U101 1)
(U102 1)
(U103 1)
(U104 1)
(U11 1)
(U12 1)
(U13 1)
(U14 1)
(U15 1)
(U16 1)
(U21 1)
(U22 1)
(U23 1)
(U31 1)
(U32 1)
(U33 1)
(U34 1)
(U35 1)
(U36 1)
(U41 1)
(U42 1)
(U51 1)
(U61 1)
(U62 1)
(U71 1)
(U72 1)
(U81 1)
(U82 1)
(U83 1)
(U84 1)
(U91 1)
(U92 1)
(isNat )
(isNatKind )



)
(RULES
U101(tt,M,N) -> U102(isNatKind(M),M,N)

U102(tt,M,N) -> U103(isNat(N),M,N)

U103(tt,M,N) -> U104(isNatKind(N),M,N)

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

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,V1,V2) -> U32(isNatKind(V1),V1,V2)

U32(tt,V1,V2) -> U33(isNatKind(V2),V1,V2)

U33(tt,V1,V2) -> U34(isNatKind(V2),V1,V2)

U34(tt,V1,V2) -> U35(isNat(V1),V2)

U35(tt,V2) -> U36(isNat(V2))

U36(tt) -> tt

U41(tt,V2) -> U42(isNatKind(V2))

U42(tt) -> tt

U51(tt) -> tt

U61(tt,V2) -> U62(isNatKind(V2))

U62(tt) -> tt

U71(tt,N) -> U72(isNatKind(N),N)

U72(tt,N) -> N

U81(tt,M,N) -> U82(isNatKind(M),M,N)

U82(tt,M,N) -> U83(isNat(N),M,N)

U83(tt,M,N) -> U84(isNatKind(N),M,N)

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

U91(tt,N) -> U92(isNatKind(N))

U92(tt) -> 0

isNat(0) -> tt

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

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

isNat(x(V1,V2)) -> U31(isNatKind(V1),V1,V2)

isNatKind(0) -> tt

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

isNatKind(s(V1)) -> U51(isNatKind(V1))

isNatKind(x(V1,V2)) -> U61(isNatKind(V1),V2)

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

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

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

x(N,s(M)) -> U101(isNat(M),M,N)
)