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(X1, X2), activate(n__s(X)) -> s(X), activate(n__x(X1, X2)) -> x(X1, 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()} DP: Strict: { U102#(tt(), M, N) -> activate#(M), U102#(tt(), M, N) -> activate#(N), U102#(tt(), M, N) -> U103#(isNat(activate(N)), activate(M), activate(N)), U102#(tt(), M, N) -> isNat#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1), isNatKind#(n__plus(V1, V2)) -> activate#(V2), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1))), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1), isNatKind#(n__x(V1, V2)) -> activate#(V2), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2)), activate#(n__0()) -> 0#(), activate#(n__plus(X1, X2)) -> plus#(X1, X2), activate#(n__s(X)) -> s#(X), activate#(n__x(X1, X2)) -> x#(X1, X2), U101#(tt(), M, N) -> U102#(isNatKind(activate(M)), activate(M), activate(N)), U101#(tt(), M, N) -> isNatKind#(activate(M)), U101#(tt(), M, N) -> activate#(M), U101#(tt(), M, N) -> activate#(N), U103#(tt(), M, N) -> isNatKind#(activate(N)), U103#(tt(), M, N) -> activate#(M), U103#(tt(), M, N) -> activate#(N), U103#(tt(), M, N) -> U104#(isNatKind(activate(N)), activate(M), activate(N)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1), isNat#(n__plus(V1, V2)) -> activate#(V2), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNat#(n__x(V1, V2)) -> activate#(V1), isNat#(n__x(V1, V2)) -> activate#(V2), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2)), U104#(tt(), M, N) -> activate#(M), U104#(tt(), M, N) -> activate#(N), U104#(tt(), M, N) -> plus#(x(activate(N), activate(M)), activate(N)), U104#(tt(), M, N) -> x#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U81#(isNat(M), M, N), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U71#(isNat(N), N), x#(N, s(M)) -> U101#(isNat(M), M, N), x#(N, s(M)) -> isNat#(M), x#(N, 0()) -> isNat#(N), x#(N, 0()) -> U91#(isNat(N), N), U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), U12#(tt(), V1, V2) -> activate#(V1), U12#(tt(), V1, V2) -> activate#(V2), U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> activate#(V2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), U13#(tt(), V1, V2) -> activate#(V1), U13#(tt(), V1, V2) -> activate#(V2), U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> activate#(V1), U14#(tt(), V1, V2) -> activate#(V2), U14#(tt(), V1, V2) -> isNat#(activate(V1)), U14#(tt(), V1, V2) -> U15#(isNat(activate(V1)), activate(V2)), U15#(tt(), V2) -> activate#(V2), U15#(tt(), V2) -> isNat#(activate(V2)), U15#(tt(), V2) -> U16#(isNat(activate(V2))), U22#(tt(), V1) -> activate#(V1), U22#(tt(), V1) -> isNat#(activate(V1)), U22#(tt(), V1) -> U23#(isNat(activate(V1))), U21#(tt(), V1) -> isNatKind#(activate(V1)), U21#(tt(), V1) -> activate#(V1), U21#(tt(), V1) -> U22#(isNatKind(activate(V1)), activate(V1)), U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), U32#(tt(), V1, V2) -> activate#(V1), U32#(tt(), V1, V2) -> activate#(V2), U32#(tt(), V1, V2) -> U33#(isNatKind(activate(V2)), activate(V1), activate(V2)), U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), U31#(tt(), V1, V2) -> activate#(V1), U31#(tt(), V1, V2) -> activate#(V2), U31#(tt(), V1, V2) -> U32#(isNatKind(activate(V1)), activate(V1), activate(V2)), U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), U33#(tt(), V1, V2) -> activate#(V1), U33#(tt(), V1, V2) -> activate#(V2), U33#(tt(), V1, V2) -> U34#(isNatKind(activate(V2)), activate(V1), activate(V2)), U34#(tt(), V1, V2) -> activate#(V1), U34#(tt(), V1, V2) -> activate#(V2), U34#(tt(), V1, V2) -> isNat#(activate(V1)), U34#(tt(), V1, V2) -> U35#(isNat(activate(V1)), activate(V2)), U35#(tt(), V2) -> activate#(V2), U35#(tt(), V2) -> isNat#(activate(V2)), U35#(tt(), V2) -> U36#(isNat(activate(V2))), U41#(tt(), V2) -> isNatKind#(activate(V2)), U41#(tt(), V2) -> activate#(V2), U41#(tt(), V2) -> U42#(isNatKind(activate(V2))), U61#(tt(), V2) -> isNatKind#(activate(V2)), U61#(tt(), V2) -> activate#(V2), U61#(tt(), V2) -> U62#(isNatKind(activate(V2))), U72#(tt(), N) -> activate#(N), U71#(tt(), N) -> isNatKind#(activate(N)), U71#(tt(), N) -> activate#(N), U71#(tt(), N) -> U72#(isNatKind(activate(N)), activate(N)), U82#(tt(), M, N) -> activate#(M), U82#(tt(), M, N) -> activate#(N), U82#(tt(), M, N) -> isNat#(activate(N)), U82#(tt(), M, N) -> U83#(isNat(activate(N)), activate(M), activate(N)), U81#(tt(), M, N) -> isNatKind#(activate(M)), U81#(tt(), M, N) -> activate#(M), U81#(tt(), M, N) -> activate#(N), U81#(tt(), M, N) -> U82#(isNatKind(activate(M)), activate(M), activate(N)), U83#(tt(), M, N) -> isNatKind#(activate(N)), U83#(tt(), M, N) -> activate#(M), U83#(tt(), M, N) -> activate#(N), U83#(tt(), M, N) -> U84#(isNatKind(activate(N)), activate(M), activate(N)), U84#(tt(), M, N) -> activate#(M), U84#(tt(), M, N) -> activate#(N), U84#(tt(), M, N) -> plus#(activate(N), activate(M)), U84#(tt(), M, N) -> s#(plus(activate(N), activate(M))), U92#(tt()) -> 0#(), U91#(tt(), N) -> isNatKind#(activate(N)), U91#(tt(), N) -> activate#(N), U91#(tt(), N) -> U92#(isNatKind(activate(N)))} Weak: { 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__x(X1, X2)) -> x(X1, 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()} EDG: { (x#(N, 0()) -> U91#(isNat(N), N), U91#(tt(), N) -> U92#(isNatKind(activate(N)))) (x#(N, 0()) -> U91#(isNat(N), N), U91#(tt(), N) -> activate#(N)) (x#(N, 0()) -> U91#(isNat(N), N), U91#(tt(), N) -> isNatKind#(activate(N))) (activate#(n__x(X1, X2)) -> x#(X1, X2), x#(N, 0()) -> U91#(isNat(N), N)) (activate#(n__x(X1, X2)) -> x#(X1, X2), x#(N, 0()) -> isNat#(N)) (activate#(n__x(X1, X2)) -> x#(X1, X2), x#(N, s(M)) -> isNat#(M)) (activate#(n__x(X1, X2)) -> x#(X1, X2), x#(N, s(M)) -> U101#(isNat(M), M, N)) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__x(V1, V2)) -> activate#(V2)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__x(V1, V2)) -> activate#(V1)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> activate#(V1)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U41#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> activate#(V2)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__x(V1, V2)) -> activate#(V2)) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__x(V1, V2)) -> activate#(V1)) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U102#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> activate#(V1)) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U71#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> activate#(V1)) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U83#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> activate#(V1)) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U101#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2)), U41#(tt(), V2) -> U42#(isNatKind(activate(V2)))) (isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2)), U41#(tt(), V2) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2)), U41#(tt(), V2) -> isNatKind#(activate(V2))) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> U22#(isNatKind(activate(V1)), activate(V1))) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> activate#(V1)) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> isNatKind#(activate(V1))) (U104#(tt(), M, N) -> x#(activate(N), activate(M)), x#(N, 0()) -> U91#(isNat(N), N)) (U104#(tt(), M, N) -> x#(activate(N), activate(M)), x#(N, 0()) -> isNat#(N)) (U104#(tt(), M, N) -> x#(activate(N), activate(M)), x#(N, s(M)) -> isNat#(M)) (U104#(tt(), M, N) -> x#(activate(N), activate(M)), x#(N, s(M)) -> U101#(isNat(M), M, N)) (x#(N, s(M)) -> U101#(isNat(M), M, N), U101#(tt(), M, N) -> activate#(N)) (x#(N, s(M)) -> U101#(isNat(M), M, N), U101#(tt(), M, N) -> activate#(M)) (x#(N, s(M)) -> U101#(isNat(M), M, N), U101#(tt(), M, N) -> isNatKind#(activate(M))) (x#(N, s(M)) -> U101#(isNat(M), M, N), U101#(tt(), M, N) -> U102#(isNatKind(activate(M)), activate(M), activate(N))) (U21#(tt(), V1) -> U22#(isNatKind(activate(V1)), activate(V1)), U22#(tt(), V1) -> U23#(isNat(activate(V1)))) (U21#(tt(), V1) -> U22#(isNatKind(activate(V1)), activate(V1)), U22#(tt(), V1) -> isNat#(activate(V1))) (U21#(tt(), V1) -> U22#(isNatKind(activate(V1)), activate(V1)), U22#(tt(), V1) -> activate#(V1)) (U71#(tt(), N) -> U72#(isNatKind(activate(N)), activate(N)), U72#(tt(), N) -> activate#(N)) (U102#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U102#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U102#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U102#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U103#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U103#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U103#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U103#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (plus#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> activate#(V2)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> activate#(V1)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> activate#(V1)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V2)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V1)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U82#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U82#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U82#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U82#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U83#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U83#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U83#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U83#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U102#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U102#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U102#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U102#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U103#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U103#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U103#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U103#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (plus#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (plus#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> activate#(V2)) (plus#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> activate#(V1)) (plus#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> activate#(V1)) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V2)) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V1)) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U72#(tt(), N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U72#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U72#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U72#(tt(), N) -> activate#(N), activate#(n__0()) -> 0#()) (U82#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U82#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U82#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U82#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U83#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U83#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U83#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U83#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U91#(tt(), N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U91#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U91#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U91#(tt(), N) -> activate#(N), activate#(n__0()) -> 0#()) (U101#(tt(), M, N) -> U102#(isNatKind(activate(M)), activate(M), activate(N)), U102#(tt(), M, N) -> isNat#(activate(N))) (U101#(tt(), M, N) -> U102#(isNatKind(activate(M)), activate(M), activate(N)), U102#(tt(), M, N) -> U103#(isNat(activate(N)), activate(M), activate(N))) (U101#(tt(), M, N) -> U102#(isNatKind(activate(M)), activate(M), activate(N)), U102#(tt(), M, N) -> activate#(N)) (U101#(tt(), M, N) -> U102#(isNatKind(activate(M)), activate(M), activate(N)), U102#(tt(), M, N) -> activate#(M)) (isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2))) (isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> activate#(V2)) (isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> activate#(V1)) (isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1))) (U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2))) (U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> activate#(V2)) (U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> activate#(V1)) (U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> isNatKind#(activate(V2))) (U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> U15#(isNat(activate(V1)), activate(V2))) (U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> isNat#(activate(V1))) (U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> activate#(V2)) (U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> activate#(V1)) (U31#(tt(), V1, V2) -> U32#(isNatKind(activate(V1)), activate(V1), activate(V2)), U32#(tt(), V1, V2) -> U33#(isNatKind(activate(V2)), activate(V1), activate(V2))) (U31#(tt(), V1, V2) -> U32#(isNatKind(activate(V1)), activate(V1), activate(V2)), U32#(tt(), V1, V2) -> activate#(V2)) (U31#(tt(), V1, V2) -> U32#(isNatKind(activate(V1)), activate(V1), activate(V2)), U32#(tt(), V1, V2) -> activate#(V1)) (U31#(tt(), V1, V2) -> U32#(isNatKind(activate(V1)), activate(V1), activate(V2)), U32#(tt(), V1, V2) -> isNatKind#(activate(V2))) (U82#(tt(), M, N) -> U83#(isNat(activate(N)), activate(M), activate(N)), U83#(tt(), M, N) -> U84#(isNatKind(activate(N)), activate(M), activate(N))) (U82#(tt(), M, N) -> U83#(isNat(activate(N)), activate(M), activate(N)), U83#(tt(), M, N) -> activate#(N)) (U82#(tt(), M, N) -> U83#(isNat(activate(N)), activate(M), activate(N)), U83#(tt(), M, N) -> activate#(M)) (U82#(tt(), M, N) -> U83#(isNat(activate(N)), activate(M), activate(N)), U83#(tt(), M, N) -> isNatKind#(activate(N))) (U83#(tt(), M, N) -> U84#(isNatKind(activate(N)), activate(M), activate(N)), U84#(tt(), M, N) -> s#(plus(activate(N), activate(M)))) (U83#(tt(), M, N) -> U84#(isNatKind(activate(N)), activate(M), activate(N)), U84#(tt(), M, N) -> plus#(activate(N), activate(M))) (U83#(tt(), M, N) -> U84#(isNatKind(activate(N)), activate(M), activate(N)), U84#(tt(), M, N) -> activate#(N)) (U83#(tt(), M, N) -> U84#(isNatKind(activate(N)), activate(M), activate(N)), U84#(tt(), M, N) -> activate#(M)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__x(V1, V2)) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNat#(n__x(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNat#(n__x(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__x(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U14#(tt(), V1, V2) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U14#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U21#(tt(), V1) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__0()) -> 0#()) (U31#(tt(), V1, V2) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U31#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U31#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U31#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U34#(tt(), V1, V2) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U34#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U34#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U34#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__x(V1, V2)) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNatKind#(n__x(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (isNatKind#(n__x(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__x(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNat#(n__x(V1, V2)) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNat#(n__x(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (isNat#(n__x(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__x(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U14#(tt(), V1, V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U14#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U32#(tt(), V1, V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U32#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U32#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U32#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U33#(tt(), V1, V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U33#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U33#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U33#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U35#(tt(), V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U35#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U35#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U35#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U61#(tt(), V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U61#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U61#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U61#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U41#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U41#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U41#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U41#(tt(), V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U34#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U34#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U34#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U34#(tt(), V1, V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U31#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U31#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U31#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U31#(tt(), V1, V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U15#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U15#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U15#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U15#(tt(), V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U13#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U13#(tt(), V1, V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U33#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U33#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U33#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U33#(tt(), V1, V2) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U32#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U32#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U32#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U32#(tt(), V1, V2) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U22#(tt(), V1) -> activate#(V1), activate#(n__0()) -> 0#()) (U22#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U22#(tt(), V1) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U22#(tt(), V1) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U13#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U13#(tt(), V1, V2) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U12#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U12#(tt(), V1, V2) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNatKind#(n__x(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__x(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__x(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNatKind#(n__x(V1, V2)) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U81#(tt(), M, N) -> U82#(isNatKind(activate(M)), activate(M), activate(N)), U82#(tt(), M, N) -> activate#(M)) (U81#(tt(), M, N) -> U82#(isNatKind(activate(M)), activate(M), activate(N)), U82#(tt(), M, N) -> activate#(N)) (U81#(tt(), M, N) -> U82#(isNatKind(activate(M)), activate(M), activate(N)), U82#(tt(), M, N) -> isNat#(activate(N))) (U81#(tt(), M, N) -> U82#(isNatKind(activate(M)), activate(M), activate(N)), U82#(tt(), M, N) -> U83#(isNat(activate(N)), activate(M), activate(N))) (U33#(tt(), V1, V2) -> U34#(isNatKind(activate(V2)), activate(V1), activate(V2)), U34#(tt(), V1, V2) -> activate#(V1)) (U33#(tt(), V1, V2) -> U34#(isNatKind(activate(V2)), activate(V1), activate(V2)), U34#(tt(), V1, V2) -> activate#(V2)) (U33#(tt(), V1, V2) -> U34#(isNatKind(activate(V2)), activate(V1), activate(V2)), U34#(tt(), V1, V2) -> isNat#(activate(V1))) (U33#(tt(), V1, V2) -> U34#(isNatKind(activate(V2)), activate(V1), activate(V2)), U34#(tt(), V1, V2) -> U35#(isNat(activate(V1)), activate(V2))) (U32#(tt(), V1, V2) -> U33#(isNatKind(activate(V2)), activate(V1), activate(V2)), U33#(tt(), V1, V2) -> isNatKind#(activate(V2))) (U32#(tt(), V1, V2) -> U33#(isNatKind(activate(V2)), activate(V1), activate(V2)), U33#(tt(), V1, V2) -> activate#(V1)) (U32#(tt(), V1, V2) -> U33#(isNatKind(activate(V2)), activate(V1), activate(V2)), U33#(tt(), V1, V2) -> activate#(V2)) (U32#(tt(), V1, V2) -> U33#(isNatKind(activate(V2)), activate(V1), activate(V2)), U33#(tt(), V1, V2) -> U34#(isNatKind(activate(V2)), activate(V1), activate(V2))) (U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U12#(tt(), V1, V2) -> isNatKind#(activate(V2))) (U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U12#(tt(), V1, V2) -> activate#(V1)) (U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U12#(tt(), V1, V2) -> activate#(V2)) (U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2))) (isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2)), U31#(tt(), V1, V2) -> isNatKind#(activate(V1))) (isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2)), U31#(tt(), V1, V2) -> activate#(V1)) (isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2)), U31#(tt(), V1, V2) -> activate#(V2)) (isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2)), U31#(tt(), V1, V2) -> U32#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U103#(tt(), M, N) -> U104#(isNatKind(activate(N)), activate(M), activate(N)), U104#(tt(), M, N) -> activate#(M)) (U103#(tt(), M, N) -> U104#(isNatKind(activate(N)), activate(M), activate(N)), U104#(tt(), M, N) -> activate#(N)) (U103#(tt(), M, N) -> U104#(isNatKind(activate(N)), activate(M), activate(N)), U104#(tt(), M, N) -> plus#(x(activate(N), activate(M)), activate(N))) (U103#(tt(), M, N) -> U104#(isNatKind(activate(N)), activate(M), activate(N)), U104#(tt(), M, N) -> x#(activate(N), activate(M))) (U102#(tt(), M, N) -> U103#(isNat(activate(N)), activate(M), activate(N)), U103#(tt(), M, N) -> isNatKind#(activate(N))) (U102#(tt(), M, N) -> U103#(isNat(activate(N)), activate(M), activate(N)), U103#(tt(), M, N) -> activate#(M)) (U102#(tt(), M, N) -> U103#(isNat(activate(N)), activate(M), activate(N)), U103#(tt(), M, N) -> activate#(N)) (U102#(tt(), M, N) -> U103#(isNat(activate(N)), activate(M), activate(N)), U103#(tt(), M, N) -> U104#(isNatKind(activate(N)), activate(M), activate(N))) (U84#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U84#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U84#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U84#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U81#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U81#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U81#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U81#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U71#(tt(), N) -> activate#(N), activate#(n__0()) -> 0#()) (U71#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U71#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U71#(tt(), N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (x#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (x#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V1)) (x#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V2)) (x#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (x#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (x#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> activate#(V1)) (x#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (x#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (x#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> activate#(V1)) (x#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> activate#(V2)) (x#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U104#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U104#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U104#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U104#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U101#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U101#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U101#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U101#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U84#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U84#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U84#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U84#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U81#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U81#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U81#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U81#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2)) (x#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (x#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V1)) (x#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V2)) (x#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (x#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (x#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> activate#(V1)) (x#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (x#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (x#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> activate#(V1)) (x#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> activate#(V2)) (x#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U104#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U104#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U104#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U104#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U101#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U101#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U101#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U101#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2)) (U84#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M)) (U84#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> U81#(isNat(M), M, N)) (U84#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> isNat#(N)) (U84#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> U71#(isNat(N), N)) (U34#(tt(), V1, V2) -> U35#(isNat(activate(V1)), activate(V2)), U35#(tt(), V2) -> activate#(V2)) (U34#(tt(), V1, V2) -> U35#(isNat(activate(V1)), activate(V2)), U35#(tt(), V2) -> isNat#(activate(V2))) (U34#(tt(), V1, V2) -> U35#(isNat(activate(V1)), activate(V2)), U35#(tt(), V2) -> U36#(isNat(activate(V2)))) (U14#(tt(), V1, V2) -> U15#(isNat(activate(V1)), activate(V2)), U15#(tt(), V2) -> activate#(V2)) (U14#(tt(), V1, V2) -> U15#(isNat(activate(V1)), activate(V2)), U15#(tt(), V2) -> isNat#(activate(V2))) (U14#(tt(), V1, V2) -> U15#(isNat(activate(V1)), activate(V2)), U15#(tt(), V2) -> U16#(isNat(activate(V2)))) (plus#(N, s(M)) -> U81#(isNat(M), M, N), U81#(tt(), M, N) -> isNatKind#(activate(M))) (plus#(N, s(M)) -> U81#(isNat(M), M, N), U81#(tt(), M, N) -> activate#(M)) (plus#(N, s(M)) -> U81#(isNat(M), M, N), U81#(tt(), M, N) -> activate#(N)) (plus#(N, s(M)) -> U81#(isNat(M), M, N), U81#(tt(), M, N) -> U82#(isNatKind(activate(M)), activate(M), activate(N))) (U104#(tt(), M, N) -> plus#(x(activate(N), activate(M)), activate(N)), plus#(N, s(M)) -> isNat#(M)) (U104#(tt(), M, N) -> plus#(x(activate(N), activate(M)), activate(N)), plus#(N, s(M)) -> U81#(isNat(M), M, N)) (U104#(tt(), M, N) -> plus#(x(activate(N), activate(M)), activate(N)), plus#(N, 0()) -> isNat#(N)) (U104#(tt(), M, N) -> plus#(x(activate(N), activate(M)), activate(N)), plus#(N, 0()) -> U71#(isNat(N), N)) (isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2)), U61#(tt(), V2) -> isNatKind#(activate(V2))) (isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2)), U61#(tt(), V2) -> activate#(V2)) (isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2)), U61#(tt(), V2) -> U62#(isNatKind(activate(V2)))) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> activate#(V1)) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U81#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> activate#(V1)) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U91#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__x(V1, V2)) -> activate#(V1)) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__x(V1, V2)) -> activate#(V2)) (U82#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> activate#(V1)) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U103#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> activate#(V1)) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> activate#(V2)) (U34#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> activate#(V1)) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> activate#(V2)) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U61#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> activate#(V1)) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__x(V1, V2)) -> activate#(V1)) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__x(V1, V2)) -> activate#(V2)) (U35#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2))) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> U51#(isNatKind(activate(V1)))) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1))) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V1)) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> activate#(V2)) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2))) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, s(M)) -> isNat#(M)) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, s(M)) -> U81#(isNat(M), M, N)) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, 0()) -> isNat#(N)) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, 0()) -> U71#(isNat(N), N)) (U91#(tt(), N) -> U92#(isNatKind(activate(N))), U92#(tt()) -> 0#()) (plus#(N, 0()) -> U71#(isNat(N), N), U71#(tt(), N) -> isNatKind#(activate(N))) (plus#(N, 0()) -> U71#(isNat(N), N), U71#(tt(), N) -> activate#(N)) (plus#(N, 0()) -> U71#(isNat(N), N), U71#(tt(), N) -> U72#(isNatKind(activate(N)), activate(N))) } SCCS: Scc: { U102#(tt(), M, N) -> activate#(M), U102#(tt(), M, N) -> activate#(N), U102#(tt(), M, N) -> U103#(isNat(activate(N)), activate(M), activate(N)), U102#(tt(), M, N) -> isNat#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1), isNatKind#(n__plus(V1, V2)) -> activate#(V2), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1), isNatKind#(n__x(V1, V2)) -> activate#(V2), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2)), activate#(n__plus(X1, X2)) -> plus#(X1, X2), activate#(n__x(X1, X2)) -> x#(X1, X2), U101#(tt(), M, N) -> U102#(isNatKind(activate(M)), activate(M), activate(N)), U101#(tt(), M, N) -> isNatKind#(activate(M)), U101#(tt(), M, N) -> activate#(M), U101#(tt(), M, N) -> activate#(N), U103#(tt(), M, N) -> isNatKind#(activate(N)), U103#(tt(), M, N) -> activate#(M), U103#(tt(), M, N) -> activate#(N), U103#(tt(), M, N) -> U104#(isNatKind(activate(N)), activate(M), activate(N)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1), isNat#(n__plus(V1, V2)) -> activate#(V2), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNat#(n__x(V1, V2)) -> activate#(V1), isNat#(n__x(V1, V2)) -> activate#(V2), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2)), U104#(tt(), M, N) -> activate#(M), U104#(tt(), M, N) -> activate#(N), U104#(tt(), M, N) -> plus#(x(activate(N), activate(M)), activate(N)), U104#(tt(), M, N) -> x#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U81#(isNat(M), M, N), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U71#(isNat(N), N), x#(N, s(M)) -> U101#(isNat(M), M, N), x#(N, s(M)) -> isNat#(M), x#(N, 0()) -> isNat#(N), x#(N, 0()) -> U91#(isNat(N), N), U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), U12#(tt(), V1, V2) -> activate#(V1), U12#(tt(), V1, V2) -> activate#(V2), U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> activate#(V2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), U13#(tt(), V1, V2) -> activate#(V1), U13#(tt(), V1, V2) -> activate#(V2), U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> activate#(V1), U14#(tt(), V1, V2) -> activate#(V2), U14#(tt(), V1, V2) -> isNat#(activate(V1)), U14#(tt(), V1, V2) -> U15#(isNat(activate(V1)), activate(V2)), U15#(tt(), V2) -> activate#(V2), U15#(tt(), V2) -> isNat#(activate(V2)), U22#(tt(), V1) -> activate#(V1), U22#(tt(), V1) -> isNat#(activate(V1)), U21#(tt(), V1) -> isNatKind#(activate(V1)), U21#(tt(), V1) -> activate#(V1), U21#(tt(), V1) -> U22#(isNatKind(activate(V1)), activate(V1)), U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), U32#(tt(), V1, V2) -> activate#(V1), U32#(tt(), V1, V2) -> activate#(V2), U32#(tt(), V1, V2) -> U33#(isNatKind(activate(V2)), activate(V1), activate(V2)), U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), U31#(tt(), V1, V2) -> activate#(V1), U31#(tt(), V1, V2) -> activate#(V2), U31#(tt(), V1, V2) -> U32#(isNatKind(activate(V1)), activate(V1), activate(V2)), U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), U33#(tt(), V1, V2) -> activate#(V1), U33#(tt(), V1, V2) -> activate#(V2), U33#(tt(), V1, V2) -> U34#(isNatKind(activate(V2)), activate(V1), activate(V2)), U34#(tt(), V1, V2) -> activate#(V1), U34#(tt(), V1, V2) -> activate#(V2), U34#(tt(), V1, V2) -> isNat#(activate(V1)), U34#(tt(), V1, V2) -> U35#(isNat(activate(V1)), activate(V2)), U35#(tt(), V2) -> activate#(V2), U35#(tt(), V2) -> isNat#(activate(V2)), U41#(tt(), V2) -> isNatKind#(activate(V2)), U41#(tt(), V2) -> activate#(V2), U61#(tt(), V2) -> isNatKind#(activate(V2)), U61#(tt(), V2) -> activate#(V2), U72#(tt(), N) -> activate#(N), U71#(tt(), N) -> isNatKind#(activate(N)), U71#(tt(), N) -> activate#(N), U71#(tt(), N) -> U72#(isNatKind(activate(N)), activate(N)), U82#(tt(), M, N) -> activate#(M), U82#(tt(), M, N) -> activate#(N), U82#(tt(), M, N) -> isNat#(activate(N)), U82#(tt(), M, N) -> U83#(isNat(activate(N)), activate(M), activate(N)), U81#(tt(), M, N) -> isNatKind#(activate(M)), U81#(tt(), M, N) -> activate#(M), U81#(tt(), M, N) -> activate#(N), U81#(tt(), M, N) -> U82#(isNatKind(activate(M)), activate(M), activate(N)), U83#(tt(), M, N) -> isNatKind#(activate(N)), U83#(tt(), M, N) -> activate#(M), U83#(tt(), M, N) -> activate#(N), U83#(tt(), M, N) -> U84#(isNatKind(activate(N)), activate(M), activate(N)), U84#(tt(), M, N) -> activate#(M), U84#(tt(), M, N) -> activate#(N), U84#(tt(), M, N) -> plus#(activate(N), activate(M)), U91#(tt(), N) -> isNatKind#(activate(N)), U91#(tt(), N) -> activate#(N)} SCC: Strict: { U102#(tt(), M, N) -> activate#(M), U102#(tt(), M, N) -> activate#(N), U102#(tt(), M, N) -> U103#(isNat(activate(N)), activate(M), activate(N)), U102#(tt(), M, N) -> isNat#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1), isNatKind#(n__plus(V1, V2)) -> activate#(V2), isNatKind#(n__plus(V1, V2)) -> U41#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__x(V1, V2)) -> activate#(V1), isNatKind#(n__x(V1, V2)) -> activate#(V2), isNatKind#(n__x(V1, V2)) -> U61#(isNatKind(activate(V1)), activate(V2)), activate#(n__plus(X1, X2)) -> plus#(X1, X2), activate#(n__x(X1, X2)) -> x#(X1, X2), U101#(tt(), M, N) -> U102#(isNatKind(activate(M)), activate(M), activate(N)), U101#(tt(), M, N) -> isNatKind#(activate(M)), U101#(tt(), M, N) -> activate#(M), U101#(tt(), M, N) -> activate#(N), U103#(tt(), M, N) -> isNatKind#(activate(N)), U103#(tt(), M, N) -> activate#(M), U103#(tt(), M, N) -> activate#(N), U103#(tt(), M, N) -> U104#(isNatKind(activate(N)), activate(M), activate(N)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1), isNat#(n__plus(V1, V2)) -> activate#(V2), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), isNat#(n__x(V1, V2)) -> isNatKind#(activate(V1)), isNat#(n__x(V1, V2)) -> activate#(V1), isNat#(n__x(V1, V2)) -> activate#(V2), isNat#(n__x(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V1), activate(V2)), U104#(tt(), M, N) -> activate#(M), U104#(tt(), M, N) -> activate#(N), U104#(tt(), M, N) -> plus#(x(activate(N), activate(M)), activate(N)), U104#(tt(), M, N) -> x#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U81#(isNat(M), M, N), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U71#(isNat(N), N), x#(N, s(M)) -> U101#(isNat(M), M, N), x#(N, s(M)) -> isNat#(M), x#(N, 0()) -> isNat#(N), x#(N, 0()) -> U91#(isNat(N), N), U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), U12#(tt(), V1, V2) -> activate#(V1), U12#(tt(), V1, V2) -> activate#(V2), U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> activate#(V2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), U13#(tt(), V1, V2) -> activate#(V1), U13#(tt(), V1, V2) -> activate#(V2), U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> activate#(V1), U14#(tt(), V1, V2) -> activate#(V2), U14#(tt(), V1, V2) -> isNat#(activate(V1)), U14#(tt(), V1, V2) -> U15#(isNat(activate(V1)), activate(V2)), U15#(tt(), V2) -> activate#(V2), U15#(tt(), V2) -> isNat#(activate(V2)), U22#(tt(), V1) -> activate#(V1), U22#(tt(), V1) -> isNat#(activate(V1)), U21#(tt(), V1) -> isNatKind#(activate(V1)), U21#(tt(), V1) -> activate#(V1), U21#(tt(), V1) -> U22#(isNatKind(activate(V1)), activate(V1)), U32#(tt(), V1, V2) -> isNatKind#(activate(V2)), U32#(tt(), V1, V2) -> activate#(V1), U32#(tt(), V1, V2) -> activate#(V2), U32#(tt(), V1, V2) -> U33#(isNatKind(activate(V2)), activate(V1), activate(V2)), U31#(tt(), V1, V2) -> isNatKind#(activate(V1)), U31#(tt(), V1, V2) -> activate#(V1), U31#(tt(), V1, V2) -> activate#(V2), U31#(tt(), V1, V2) -> U32#(isNatKind(activate(V1)), activate(V1), activate(V2)), U33#(tt(), V1, V2) -> isNatKind#(activate(V2)), U33#(tt(), V1, V2) -> activate#(V1), U33#(tt(), V1, V2) -> activate#(V2), U33#(tt(), V1, V2) -> U34#(isNatKind(activate(V2)), activate(V1), activate(V2)), U34#(tt(), V1, V2) -> activate#(V1), U34#(tt(), V1, V2) -> activate#(V2), U34#(tt(), V1, V2) -> isNat#(activate(V1)), U34#(tt(), V1, V2) -> U35#(isNat(activate(V1)), activate(V2)), U35#(tt(), V2) -> activate#(V2), U35#(tt(), V2) -> isNat#(activate(V2)), U41#(tt(), V2) -> isNatKind#(activate(V2)), U41#(tt(), V2) -> activate#(V2), U61#(tt(), V2) -> isNatKind#(activate(V2)), U61#(tt(), V2) -> activate#(V2), U72#(tt(), N) -> activate#(N), U71#(tt(), N) -> isNatKind#(activate(N)), U71#(tt(), N) -> activate#(N), U71#(tt(), N) -> U72#(isNatKind(activate(N)), activate(N)), U82#(tt(), M, N) -> activate#(M), U82#(tt(), M, N) -> activate#(N), U82#(tt(), M, N) -> isNat#(activate(N)), U82#(tt(), M, N) -> U83#(isNat(activate(N)), activate(M), activate(N)), U81#(tt(), M, N) -> isNatKind#(activate(M)), U81#(tt(), M, N) -> activate#(M), U81#(tt(), M, N) -> activate#(N), U81#(tt(), M, N) -> U82#(isNatKind(activate(M)), activate(M), activate(N)), U83#(tt(), M, N) -> isNatKind#(activate(N)), U83#(tt(), M, N) -> activate#(M), U83#(tt(), M, N) -> activate#(N), U83#(tt(), M, N) -> U84#(isNatKind(activate(N)), activate(M), activate(N)), U84#(tt(), M, N) -> activate#(M), U84#(tt(), M, N) -> activate#(N), U84#(tt(), M, N) -> plus#(activate(N), activate(M)), U91#(tt(), N) -> isNatKind#(activate(N)), U91#(tt(), N) -> activate#(N)} Weak: { 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__x(X1, X2)) -> x(X1, 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