YES TRS: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} DP: Strict: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> U41#(isNatKind(activate(V1))), activate#(n__0()) -> 0#(), activate#(n__plus(X1, X2)) -> plus#(X1, X2), activate#(n__s(X)) -> s#(X), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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) -> U15#(isNat(activate(V1)), activate(V2)), U14#(tt(), V1, V2) -> isNat#(activate(V1)), U15#(tt(), V2) -> activate#(V2), U15#(tt(), V2) -> isNat#(activate(V2)), U15#(tt(), V2) -> U16#(isNat(activate(V2))), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U31#(tt(), V2) -> U32#(isNatKind(activate(V2))), U52#(tt(), N) -> activate#(N), U51#(tt(), N) -> isNatKind#(activate(N)), U51#(tt(), N) -> activate#(N), U51#(tt(), N) -> U52#(isNatKind(activate(N)), activate(N)), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> s#(plus(activate(N), activate(M))), U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U61#(isNat(M), M, N), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U51#(isNat(N), N)} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} EDG: { (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (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__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#()) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (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#()) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> U41#(isNatKind(activate(V1)))) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> activate#(V1)) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> U41#(isNatKind(activate(V1)))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> activate#(V1)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> U41#(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)) -> isNatKind#(activate(V1))) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (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)) -> activate#(V1)) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> U41#(isNatKind(activate(V1)))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U41#(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)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (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)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(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__s(V1)) -> activate#(V1)) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (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__plus(V1, V2)) -> activate#(V2)) (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)) -> isNatKind#(activate(V1))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U41#(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)) -> U31#(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))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U41#(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)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U61#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U61#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U61#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U64#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U64#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U64#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U52#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U52#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U52#(tt(), N) -> activate#(N), activate#(n__0()) -> 0#()) (U62#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U62#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U62#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U63#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U63#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U63#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (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))) (U14#(tt(), V1, V2) -> U15#(isNat(activate(V1)), activate(V2)), U15#(tt(), V2) -> U16#(isNat(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) -> activate#(V2)) (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)) (U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> U51#(isNat(N), N)) (U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> isNat#(N)) (U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> U61#(isNat(M), M, N)) (U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M)) (U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2))) (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) -> activate#(V1)) (U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U12#(tt(), V1, V2) -> isNatKind#(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))) (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))) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N))) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> isNat#(activate(N))) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> activate#(M)) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> activate#(N)) (plus#(N, 0()) -> U51#(isNat(N), N), U51#(tt(), N) -> U52#(isNatKind(activate(N)), activate(N))) (plus#(N, 0()) -> U51#(isNat(N), N), U51#(tt(), N) -> activate#(N)) (plus#(N, 0()) -> U51#(isNat(N), N), U51#(tt(), N) -> isNatKind#(activate(N))) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (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__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#()) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N))) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> activate#(M)) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> activate#(N)) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> isNatKind#(activate(M))) (U31#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U31#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U31#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (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)) (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)) (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)) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N)) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(M)) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> s#(plus(activate(N), activate(M)))) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> plus#(activate(N), activate(M))) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N))) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> activate#(N)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> activate#(M)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N))) (U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> 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) -> 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))) (U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> isNatKind#(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) -> activate#(V2)) (U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2))) (U51#(tt(), N) -> U52#(isNatKind(activate(N)), activate(N)), U52#(tt(), N) -> activate#(N)) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> isNatKind#(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) -> U22#(isNatKind(activate(V1)), activate(V1))) (isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> isNatKind#(activate(V2))) (isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> U32#(isNatKind(activate(V2)))) (U64#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U64#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U64#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U61#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U61#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U61#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U51#(tt(), N) -> activate#(N), activate#(n__0()) -> 0#()) (U51#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U51#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V1)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V2)) (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__s(V1)) -> isNatKind#(activate(V1))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> activate#(V1)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U63#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U63#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U63#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U62#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U62#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U62#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (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__s(V1)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (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)) -> U31#(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)) -> U41#(isNatKind(activate(V1)))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> 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)) -> U41#(isNatKind(activate(V1)))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (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__s(V1)) -> activate#(V1)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> U41#(isNatKind(activate(V1)))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (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__s(V1)) -> isNatKind#(activate(V1))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> activate#(V1)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> 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)) -> U41#(isNatKind(activate(V1)))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> activate#(V1)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> U41#(isNatKind(activate(V1)))) (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)) -> U61#(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()) -> U51#(isNat(N), N)) (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)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (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)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (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)) } SCCS: Scc: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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) -> U15#(isNat(activate(V1)), activate(V2)), U14#(tt(), V1, V2) -> isNat#(activate(V1)), U15#(tt(), V2) -> activate#(V2), U15#(tt(), V2) -> isNat#(activate(V2)), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U52#(tt(), N) -> activate#(N), U51#(tt(), N) -> isNatKind#(activate(N)), U51#(tt(), N) -> activate#(N), U51#(tt(), N) -> U52#(isNatKind(activate(N)), activate(N)), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U61#(isNat(M), M, N), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U51#(isNat(N), N)} SCC: Strict: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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) -> U15#(isNat(activate(V1)), activate(V2)), U14#(tt(), V1, V2) -> isNat#(activate(V1)), U15#(tt(), V2) -> activate#(V2), U15#(tt(), V2) -> isNat#(activate(V2)), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U52#(tt(), N) -> activate#(N), U51#(tt(), N) -> isNatKind#(activate(N)), U51#(tt(), N) -> activate#(N), U51#(tt(), N) -> U52#(isNatKind(activate(N)), activate(N)), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U61#(isNat(M), M, N), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U51#(isNat(N), N)} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} POLY: Argument Filtering: pi(0) = [], pi(n__s) = 0, pi(n__plus) = [0,1], pi(n__0) = [], pi(plus#) = [0,1], pi(plus) = [0,1], pi(s) = 0, pi(U64#) = [1,2], pi(U64) = [1,2], pi(U63#) = [1,2], pi(U63) = [1,2], pi(U61#) = [1,2], pi(U61) = [1,2], pi(U62#) = [1,2], pi(U62) = [1,2], pi(U51#) = 1, pi(U51) = 1, pi(U52#) = 1, pi(U52) = 1, pi(U41) = [], pi(U31#) = 1, pi(U31) = [], pi(U32) = [], pi(U23) = [], pi(U21#) = 1, pi(U21) = [], pi(U22#) = 1, pi(U22) = [], pi(U16) = [], pi(isNat#) = 0, pi(isNat) = [], pi(U15#) = 1, pi(U15) = [], pi(U14#) = [1,2], pi(U14) = [], pi(U13#) = [1,2], pi(U13) = [], pi(tt) = [], pi(U11#) = [1,2], pi(U11) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNatKind#) = 0, pi(isNatKind) = [], pi(U12#) = [1,2], pi(U12) = [] Usable Rules: {} Interpretation: [U64#](x0, x1) = x0 + x1, [U63#](x0, x1) = x0 + x1, [U61#](x0, x1) = x0 + x1, [U62#](x0, x1) = x0 + x1, [U14#](x0, x1) = x0 + x1, [U13#](x0, x1) = x0 + x1, [U11#](x0, x1) = x0 + x1, [U12#](x0, x1) = x0 + x1, [plus#](x0, x1) = x0 + x1, [n__plus](x0, x1) = x0 + x1, [0] = 1 Strict: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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) -> U15#(isNat(activate(V1)), activate(V2)), U14#(tt(), V1, V2) -> isNat#(activate(V1)), U15#(tt(), V2) -> activate#(V2), U15#(tt(), V2) -> isNat#(activate(V2)), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U52#(tt(), N) -> activate#(N), U51#(tt(), N) -> isNatKind#(activate(N)), U51#(tt(), N) -> activate#(N), U51#(tt(), N) -> U52#(isNatKind(activate(N)), activate(N)), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U61#(isNat(M), M, N)} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} EDG: { (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) -> activate#(V2)) (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)) (U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> U61#(isNat(M), M, N)) (U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U15#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U31#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> activate#(V1)) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U51#(tt(), N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> activate#(V1)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> 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)) -> isNatKind#(activate(V1))) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (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)) -> activate#(V1)) (U13#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> 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)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (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)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(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__s(V1)) -> activate#(V1)) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (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__plus(V1, V2)) -> activate#(V2)) (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)) -> 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)) -> U31#(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))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U51#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U61#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U64#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U22#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U62#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U63#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (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))) (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) -> isNat#(activate(V1))) (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) -> activate#(V2)) (U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> activate#(V1)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N))) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> activate#(M)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> activate#(N)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N))) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> plus#(activate(N), activate(M))) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(M)) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N)) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> activate#(N)) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> activate#(M)) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> isNat#(activate(N))) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N))) (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) -> isNatKind#(activate(V1))) (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) -> 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))) (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)) -> U61#(isNat(M), M, N)) (U64#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U61#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> isNatKind#(activate(M))) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> activate#(N)) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> activate#(M)) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N))) (U63#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U62#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U52#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (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__s(V1)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (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)) -> U31#(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)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (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__s(V1)) -> activate#(V1)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (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__s(V1)) -> isNatKind#(activate(V1))) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> activate#(V1)) (U15#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U51#(tt(), N) -> U52#(isNatKind(activate(N)), activate(N)), U52#(tt(), N) -> activate#(N)) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> isNatKind#(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) -> U22#(isNatKind(activate(V1)), activate(V1))) (isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> isNatKind#(activate(V2))) (isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> activate#(V2)) } SCCS: Scc: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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) -> U15#(isNat(activate(V1)), activate(V2)), U14#(tt(), V1, V2) -> isNat#(activate(V1)), U15#(tt(), V2) -> activate#(V2), U15#(tt(), V2) -> isNat#(activate(V2)), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U61#(isNat(M), M, N)} SCC: Strict: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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) -> U15#(isNat(activate(V1)), activate(V2)), U14#(tt(), V1, V2) -> isNat#(activate(V1)), U15#(tt(), V2) -> activate#(V2), U15#(tt(), V2) -> isNat#(activate(V2)), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U61#(isNat(M), M, N)} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} POLY: Argument Filtering: pi(0) = [], pi(n__s) = 0, pi(n__plus) = [0,1], pi(n__0) = [], pi(plus#) = [0,1], pi(plus) = [0,1], pi(s) = 0, pi(U64#) = [1,2], pi(U64) = [1,2], pi(U63#) = [1,2], pi(U63) = [1,2], pi(U61#) = [1,2], pi(U61) = [1,2], pi(U62#) = [1,2], pi(U62) = [1,2], pi(U51) = [1], pi(U52) = 1, pi(U41) = [], pi(U31#) = 1, pi(U31) = [], pi(U32) = [], pi(U23) = 0, pi(U21#) = 1, pi(U21) = 1, pi(U22#) = 1, pi(U22) = 1, pi(U16) = 0, pi(isNat#) = 0, pi(isNat) = 0, pi(U15#) = [0,1], pi(U15) = 1, pi(U14#) = [1,2], pi(U14) = 2, pi(U13#) = [1,2], pi(U13) = 2, pi(tt) = [], pi(U11#) = [1,2], pi(U11) = [1,2], pi(activate#) = 0, pi(activate) = 0, pi(isNatKind#) = 0, pi(isNatKind) = [], pi(U12#) = [1,2], pi(U12) = [1,2] Usable Rules: {} Interpretation: [U64#](x0, x1) = x0 + x1, [U63#](x0, x1) = x0 + x1, [U61#](x0, x1) = x0 + x1, [U62#](x0, x1) = x0 + x1, [U14#](x0, x1) = x0 + x1, [U13#](x0, x1) = x0 + x1, [U11#](x0, x1) = x0 + x1, [U12#](x0, x1) = x0 + x1, [plus#](x0, x1) = x0 + x1, [U15#](x0, x1) = x0 + x1, [n__plus](x0, x1) = x0 + x1, [tt] = 1 Strict: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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) -> U15#(isNat(activate(V1)), activate(V2)), U14#(tt(), V1, V2) -> isNat#(activate(V1)), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U61#(isNat(M), M, N)} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} EDG: { (U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2))) (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) -> activate#(V1)) (U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U12#(tt(), V1, V2) -> isNatKind#(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))) (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))) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N))) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> isNat#(activate(N))) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> activate#(M)) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> activate#(N)) (isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(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))) (U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> U61#(isNat(M), M, N)) (U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, s(M)) -> U61#(isNat(M), M, N)) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, s(M)) -> isNat#(M)) (U61#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U64#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U62#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U63#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (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))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> 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)) -> U31#(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))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> activate#(V1)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> 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)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (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)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(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__s(V1)) -> activate#(V1)) (U14#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (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__plus(V1, V2)) -> activate#(V2)) (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)) -> 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)) -> U31#(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))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U22#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (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__s(V1)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (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)) -> U31#(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)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (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__s(V1)) -> activate#(V1)) (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)) -> U31#(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)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__s(V1)) -> activate#(V1)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__s(V1)) -> activate#(V1)) (U64#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U61#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> isNatKind#(activate(M))) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> activate#(N)) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> activate#(M)) (plus#(N, s(M)) -> U61#(isNat(M), M, N), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N))) (U63#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U62#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U31#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U21#(tt(), V1) -> U22#(isNatKind(activate(V1)), activate(V1)), U22#(tt(), V1) -> activate#(V1)) (U21#(tt(), V1) -> U22#(isNatKind(activate(V1)), activate(V1)), U22#(tt(), V1) -> isNat#(activate(V1))) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N)) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(M)) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> plus#(activate(N), activate(M))) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N))) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> activate#(N)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> activate#(M)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N))) (U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> 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) -> 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))) (U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> isNatKind#(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) -> activate#(V2)) (U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2)), U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2))) } SCCS: Scc: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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)), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U61#(isNat(M), M, N)} SCC: Strict: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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)), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U61#(isNat(M), M, N)} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} POLY: Argument Filtering: pi(0) = [], pi(n__s) = [0], pi(n__plus) = [0,1], pi(n__0) = [], pi(plus#) = [0,1], pi(plus) = [0,1], pi(s) = [0], pi(U64#) = [1,2], pi(U64) = [1,2], pi(U63#) = [1,2], pi(U63) = [1,2], pi(U61#) = [1,2], pi(U61) = [1,2], pi(U62#) = [1,2], pi(U62) = [1,2], pi(U51) = [1], pi(U52) = [1], pi(U41) = [], pi(U31#) = 1, pi(U31) = [], pi(U32) = [], pi(U23) = [], pi(U21#) = 1, pi(U21) = [], pi(U22#) = 1, pi(U22) = [], pi(U16) = [], pi(isNat#) = 0, pi(isNat) = [], pi(U15) = [], pi(U14#) = [1,2], pi(U14) = [], pi(U13#) = [1,2], pi(U13) = [], pi(tt) = [], pi(U11#) = [1,2], pi(U11) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNatKind#) = 0, pi(isNatKind) = [], pi(U12#) = [1,2], pi(U12) = [] Usable Rules: {} Interpretation: [U64#](x0, x1) = x0 + x1, [U63#](x0, x1) = x0 + x1, [U61#](x0, x1) = x0 + x1, [U62#](x0, x1) = x0 + x1, [U14#](x0, x1) = x0 + x1, [U13#](x0, x1) = x0 + x1, [U11#](x0, x1) = x0 + x1, [U12#](x0, x1) = x0 + x1, [plus#](x0, x1) = x0 + x1, [n__plus](x0, x1) = x0 + x1, [n__s](x0) = x0 + 1, [s](x0) = x0 + 1 Strict: { 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)), 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)) -> U31#(isNatKind(activate(V1)), activate(V2)), activate#(n__plus(X1, X2)) -> plus#(X1, X2), U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> 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)), 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)), 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)), U31#(tt(), V2) -> isNatKind#(activate(V2)), U31#(tt(), V2) -> activate#(V2), U62#(tt(), M, N) -> activate#(N), U62#(tt(), M, N) -> activate#(M), U62#(tt(), M, N) -> isNat#(activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U61#(tt(), M, N) -> isNatKind#(activate(M)), U61#(tt(), M, N) -> activate#(N), U61#(tt(), M, N) -> activate#(M), U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N)), U63#(tt(), M, N) -> activate#(N), U63#(tt(), M, N) -> activate#(M), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N), U64#(tt(), M, N) -> activate#(M), U64#(tt(), M, N) -> plus#(activate(N), activate(M))} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} EDG: { (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U62#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U12#(tt(), V1, V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U31#(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))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U31#(tt(), V2) -> isNatKind#(activate(V2)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U11#(tt(), V1, V2) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(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))) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (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)) -> activate#(V1)) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U21#(tt(), V1) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(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)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U13#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U62#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U63#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (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) -> 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)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N))) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> activate#(M)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> activate#(N)) (U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N)), U63#(tt(), M, N) -> isNatKind#(activate(N))) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> plus#(activate(N), activate(M))) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(M)) (U63#(tt(), M, N) -> U64#(isNatKind(activate(N)), activate(M), activate(N)), U64#(tt(), M, N) -> activate#(N)) (U61#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U64#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U63#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U62#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> activate#(N)) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> activate#(M)) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> isNat#(activate(N))) (U61#(tt(), M, N) -> U62#(isNatKind(activate(M)), activate(M), activate(N)), U62#(tt(), M, N) -> U63#(isNat(activate(N)), activate(M), activate(N))) (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) -> isNatKind#(activate(V1))) (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) -> 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))) (U64#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U61#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U31#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> isNatKind#(activate(V2))) (isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> activate#(V2)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U22#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U22#(tt(), V1) -> 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__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))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(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)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U63#(tt(), M, N) -> isNatKind#(activate(N)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (U61#(tt(), M, N) -> isNatKind#(activate(M)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2))) (U22#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U14#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U12#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) } SCCS: Scc: {isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> isNatKind#(activate(V2))} Scc: { 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) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))} SCC: Strict: {isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> U31#(isNatKind(activate(V1)), activate(V2)), U31#(tt(), V2) -> isNatKind#(activate(V2))} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} POLY: Argument Filtering: pi(0) = [], pi(n__s) = [], pi(n__plus) = [0,1], pi(n__0) = [], pi(plus) = [0,1], pi(s) = [], pi(U64) = [], pi(U63) = [], pi(U61) = [], pi(U62) = [], pi(U51) = 1, pi(U52) = 1, pi(U41) = [], pi(U31#) = 1, pi(U31) = [], pi(U32) = [], pi(U23) = [], pi(U21) = [], pi(U22) = [], pi(U16) = [], pi(isNat) = [], pi(U15) = [], pi(U14) = [], pi(U13) = [], pi(tt) = [], pi(U11) = [], pi(activate) = 0, pi(isNatKind#) = 0, pi(isNatKind) = [], pi(U12) = [] Usable Rules: {} Interpretation: [n__plus](x0, x1) = x0 + x1 + 1 Strict: {U31#(tt(), V2) -> isNatKind#(activate(V2))} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} EDG: {} SCCS: Qed SCC: Strict: { 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) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> U11#(isNatKind(activate(V1)), activate(V1), activate(V2))} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} POLY: Argument Filtering: pi(0) = [], pi(n__s) = [], pi(n__plus) = [0,1], pi(n__0) = [], pi(plus) = [0,1], pi(s) = [], pi(U64) = [], pi(U63) = [], pi(U61) = [], pi(U62) = [], pi(U51) = 1, pi(U52) = 1, pi(U41) = [], pi(U31) = [], pi(U32) = [], pi(U23) = [], pi(U21) = [], pi(U22) = [], pi(U16) = [], pi(isNat#) = 0, pi(isNat) = [], pi(U15) = [], pi(U14#) = 1, pi(U14) = [], pi(U13#) = 1, pi(U13) = [], pi(tt) = [], pi(U11#) = [1,2], pi(U11) = [], pi(activate) = 0, pi(isNatKind) = [], pi(U12#) = [1,2], pi(U12) = [] Usable Rules: {} Interpretation: [U11#](x0, x1) = x0 + x1, [U12#](x0, x1) = x0 + x1, [n__plus](x0, x1) = x0 + x1 + 1 Strict: {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) -> isNat#(activate(V1))} Weak: { U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)), isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(X1, X2), activate(n__s(X)) -> s(X), 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))), 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)), U16(tt()) -> tt(), U22(tt(), V1) -> U23(isNat(activate(V1))), U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)), U23(tt()) -> tt(), U32(tt()) -> tt(), U31(tt(), V2) -> U32(isNatKind(activate(V2))), U41(tt()) -> tt(), U52(tt(), N) -> activate(N), U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)), U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)), U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)), U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)), U64(tt(), M, N) -> s(plus(activate(N), activate(M))), s(X) -> n__s(X), plus(N, s(M)) -> U61(isNat(M), M, N), plus(N, 0()) -> U51(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} EDG: {(U11#(tt(), V1, V2) -> U12#(isNatKind(activate(V1)), activate(V1), activate(V2)), U12#(tt(), V1, V2) -> U13#(isNatKind(activate(V2)), activate(V1), activate(V2))) (U13#(tt(), V1, V2) -> U14#(isNatKind(activate(V2)), activate(V1), activate(V2)), U14#(tt(), V1, V2) -> isNat#(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)))} SCCS: Qed