(COMMENT generated from Maude module 'MYNAT' by 'complete' transformation) (VAR M N V1 V2 X Z Y) (STRATEGY CONTEXTSENSITIVE (U11 1) (U12 1) (U13 1) (U21 1) (U22 1) (U31 1) (U32 1) (U33 1) (U41 1) (U51 1) (U61 1) (U71 1) (and 1) (isNat ) (isNatKind ) ) (RULES U11(tt,V1,V2) -> U12(isNat(V1),V2) U12(tt,V2) -> U13(isNat(V2)) U13(tt) -> tt U21(tt,V1) -> U22(isNat(V1)) U22(tt) -> tt U31(tt,V1,V2) -> U32(isNat(V1),V2) U32(tt,V2) -> U33(isNat(V2)) U33(tt) -> tt U41(tt,N) -> N U51(tt,M,N) -> s(plus(N,M)) U61(tt) -> 0 U71(tt,M,N) -> plus(x(N,M),N) and(tt,X) -> X isNat(0) -> tt isNat(plus(V1,V2)) -> U11(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(s(V1)) -> U21(isNatKind(V1),V1) isNat(x(V1,V2)) -> U31(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNatKind(0) -> tt isNatKind(plus(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(s(V1)) -> isNatKind(V1) isNatKind(x(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) plus(N,0) -> U41(and(isNat(N),isNatKind(N)),N) plus(N,s(M)) -> U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) x(N,0) -> U61(and(isNat(N),isNatKind(N))) x(N,s(M)) -> U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) )