MAYBE MAYBE TRS: { U102(tt(), M, N) -> U103(isNat(activate(N)), activate(M), activate(N)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U51(isNatKind(activate(V1))), isNatKind(n__x(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)), activate(n__s(X)) -> s(activate(X)), activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)), U101(tt(), M, N) -> U102(isNatKind(activate(M)), activate(M), activate(N)), U103(tt(), M, N) -> U104(isNatKind(activate(N)), activate(M), activate(N)), isNat(n__0()) -> tt(), isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)), isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)), isNat(n__x(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V1), activate(V2)), U104(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)), plus(N, s(M)) -> U81(isNat(M), M, N), plus(N, 0()) -> U71(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), x(N, s(M)) -> U101(isNat(M), M, N), x(N, 0()) -> U91(isNat(N), N), x(X1, X2) -> n__x(X1, X2), U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)), U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)), U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)), U15(tt(), V2) -> U16(isNat(activate(V2))), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt(), V1, V2) -> U33(isNatKind(activate(V2)), activate(V1), activate(V2)), U31(tt(), V1, V2) -> U32(isNatKind(activate(V1)), activate(V1), activate(V2)), U33(tt(), V1, V2) -> U34(isNatKind(activate(V2)), activate(V1), activate(V2)), U34(tt(), V1, V2) -> U35(isNat(activate(V1)), activate(V2)), U35(tt(), V2) -> U36(isNat(activate(V2))), U36(tt()) -> tt(), U42(tt()) -> tt(), U41(tt(), V2) -> U42(isNatKind(activate(V2))), U51(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatKind(activate(V2))), U72(tt(), N) -> activate(N), U71(tt(), N) -> U72(isNatKind(activate(N)), activate(N)), U82(tt(), M, N) -> U83(isNat(activate(N)), activate(M), activate(N)), U81(tt(), M, N) -> U82(isNatKind(activate(M)), activate(M), activate(N)), U83(tt(), M, N) -> U84(isNatKind(activate(N)), activate(M), activate(N)), U84(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), U92(tt()) -> 0(), U91(tt(), N) -> U92(isNatKind(activate(N))), 0() -> n__0() } DUP: We consider a duplicating system. Trs: { U102(tt(), M, N) -> U103(isNat(activate(N)), activate(M), activate(N)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U51(isNatKind(activate(V1))), isNatKind(n__x(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)), activate(n__s(X)) -> s(activate(X)), activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)), U101(tt(), M, N) -> U102(isNatKind(activate(M)), activate(M), activate(N)), U103(tt(), M, N) -> U104(isNatKind(activate(N)), activate(M), activate(N)), isNat(n__0()) -> tt(), isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)), isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)), isNat(n__x(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V1), activate(V2)), U104(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)), plus(N, s(M)) -> U81(isNat(M), M, N), plus(N, 0()) -> U71(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), x(N, s(M)) -> U101(isNat(M), M, N), x(N, 0()) -> U91(isNat(N), N), x(X1, X2) -> n__x(X1, X2), U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)), U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)), U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)), U15(tt(), V2) -> U16(isNat(activate(V2))), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt(), V1, V2) -> U33(isNatKind(activate(V2)), activate(V1), activate(V2)), U31(tt(), V1, V2) -> U32(isNatKind(activate(V1)), activate(V1), activate(V2)), U33(tt(), V1, V2) -> U34(isNatKind(activate(V2)), activate(V1), activate(V2)), U34(tt(), V1, V2) -> U35(isNat(activate(V1)), activate(V2)), U35(tt(), V2) -> U36(isNat(activate(V2))), U36(tt()) -> tt(), U42(tt()) -> tt(), U41(tt(), V2) -> U42(isNatKind(activate(V2))), U51(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatKind(activate(V2))), U72(tt(), N) -> activate(N), U71(tt(), N) -> U72(isNatKind(activate(N)), activate(N)), U82(tt(), M, N) -> U83(isNat(activate(N)), activate(M), activate(N)), U81(tt(), M, N) -> U82(isNatKind(activate(M)), activate(M), activate(N)), U83(tt(), M, N) -> U84(isNatKind(activate(N)), activate(M), activate(N)), U84(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), U92(tt()) -> 0(), U91(tt(), N) -> U92(isNatKind(activate(N))), 0() -> n__0() } Fail