YES TRS: { U12(tt()) -> tt(), isNat(n__0()) -> tt(), isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)), isNat(n__s(V1)) -> U21(isNat(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)), activate(n__s(X)) -> s(activate(X)), U11(tt(), V2) -> U12(isNat(activate(V2))), U21(tt()) -> tt(), U31(tt(), N) -> activate(N), U42(tt(), M, N) -> s(plus(activate(N), activate(M))), U41(tt(), M, N) -> U42(isNat(activate(N)), activate(M), activate(N)), s(X) -> n__s(X), plus(N, s(M)) -> U41(isNat(M), M, N), plus(N, 0()) -> U31(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} DP: Strict: { isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2), isNat#(n__plus(V1, V2)) -> activate#(V1), isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2)), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNat(activate(V1))), activate#(n__0()) -> 0#(), activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)), U11#(tt(), V2) -> U12#(isNat(activate(V2))), U11#(tt(), V2) -> isNat#(activate(V2)), U11#(tt(), V2) -> activate#(V2), U31#(tt(), N) -> activate#(N), U42#(tt(), M, N) -> activate#(N), U42#(tt(), M, N) -> activate#(M), U42#(tt(), M, N) -> s#(plus(activate(N), activate(M))), U42#(tt(), M, N) -> plus#(activate(N), activate(M)), U41#(tt(), M, N) -> isNat#(activate(N)), U41#(tt(), M, N) -> activate#(N), U41#(tt(), M, N) -> activate#(M), U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(isNat(M), M, N), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U31#(isNat(N), N)} Weak: { U12(tt()) -> tt(), isNat(n__0()) -> tt(), isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)), isNat(n__s(V1)) -> U21(isNat(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)), activate(n__s(X)) -> s(activate(X)), U11(tt(), V2) -> U12(isNat(activate(V2))), U21(tt()) -> tt(), U31(tt(), N) -> activate(N), U42(tt(), M, N) -> s(plus(activate(N), activate(M))), U41(tt(), M, N) -> U42(isNat(activate(N)), activate(M), activate(N)), s(X) -> n__s(X), plus(N, s(M)) -> U41(isNat(M), M, N), plus(N, 0()) -> U31(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} EDG: { (U31#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (U31#(tt(), N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U31#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U31#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2)) (U31#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1)) (U31#(tt(), N) -> activate#(N), activate#(n__0()) -> 0#()) (U41#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (U41#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U41#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U41#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2)) (U41#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1)) (U41#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> activate#(X)) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> activate#(X2)) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> activate#(X1)) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__0()) -> 0#()) (U11#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U11#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U11#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U11#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X2)) (U11#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X1)) (U11#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X2)) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X1)) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))) (U41#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (U41#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U41#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (U41#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2))) (U41#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U41#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U41#(tt(), M, N) -> isNat#(activate(N)), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))) (plus#(N, 0()) -> U31#(isNat(N), N), U31#(tt(), N) -> activate#(N)) (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, 0()) -> U31#(isNat(N), N)) (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, 0()) -> isNat#(N)) (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, s(M)) -> U41#(isNat(M), M, N)) (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, s(M)) -> isNat#(M)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (U42#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(activate(X))) (U42#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (U42#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U42#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X2)) (U42#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X1)) (U42#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> activate#(V1)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> isNat#(activate(V1))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), 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)) -> activate#(V2)) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))) (U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), U42#(tt(), M, N) -> activate#(N)) (U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), U42#(tt(), M, N) -> activate#(M)) (U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), U42#(tt(), M, N) -> s#(plus(activate(N), activate(M)))) (U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), U42#(tt(), M, N) -> plus#(activate(N), activate(M))) (U41#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U41#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X1)) (U41#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X2)) (U41#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U41#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (U41#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(activate(X))) (plus#(N, s(M)) -> U41#(isNat(M), M, N), U41#(tt(), M, N) -> isNat#(activate(N))) (plus#(N, s(M)) -> U41#(isNat(M), M, N), U41#(tt(), M, N) -> activate#(N)) (plus#(N, s(M)) -> U41#(isNat(M), M, N), U41#(tt(), M, N) -> activate#(M)) (plus#(N, s(M)) -> U41#(isNat(M), M, N), U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N))) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (U42#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M)) (U42#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> U41#(isNat(M), M, N)) (U42#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> isNat#(N)) (U42#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> U31#(isNat(N), N)) (isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2)), U11#(tt(), V2) -> U12#(isNat(activate(V2)))) (isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2)), U11#(tt(), V2) -> isNat#(activate(V2))) (isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2)), U11#(tt(), V2) -> activate#(V2)) (U11#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))) (U11#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U11#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U11#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2))) (U11#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (U11#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> activate#(V1)) (U11#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))) (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2))) (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X1)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X2)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1))) (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)) -> U11#(isNat(activate(V1)), activate(V2))) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> isNat#(activate(V1))) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> activate#(V1)) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (U42#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U42#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1)) (U42#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2)) (U42#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U42#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U42#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__0()) -> 0#()) (activate#(n__s(X)) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) } SCCS: Scc: { isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2), isNat#(n__plus(V1, V2)) -> activate#(V1), isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2)), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), activate#(n__s(X)) -> activate#(X), U11#(tt(), V2) -> isNat#(activate(V2)), U11#(tt(), V2) -> activate#(V2), U31#(tt(), N) -> activate#(N), U42#(tt(), M, N) -> activate#(N), U42#(tt(), M, N) -> activate#(M), U42#(tt(), M, N) -> plus#(activate(N), activate(M)), U41#(tt(), M, N) -> isNat#(activate(N)), U41#(tt(), M, N) -> activate#(N), U41#(tt(), M, N) -> activate#(M), U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(isNat(M), M, N), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U31#(isNat(N), N)} SCC: Strict: { isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2), isNat#(n__plus(V1, V2)) -> activate#(V1), isNat#(n__plus(V1, V2)) -> U11#(isNat(activate(V1)), activate(V2)), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), activate#(n__s(X)) -> activate#(X), U11#(tt(), V2) -> isNat#(activate(V2)), U11#(tt(), V2) -> activate#(V2), U31#(tt(), N) -> activate#(N), U42#(tt(), M, N) -> activate#(N), U42#(tt(), M, N) -> activate#(M), U42#(tt(), M, N) -> plus#(activate(N), activate(M)), U41#(tt(), M, N) -> isNat#(activate(N)), U41#(tt(), M, N) -> activate#(N), U41#(tt(), M, N) -> activate#(M), U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(isNat(M), M, N), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U31#(isNat(N), N)} Weak: { U12(tt()) -> tt(), isNat(n__0()) -> tt(), isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)), isNat(n__s(V1)) -> U21(isNat(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)), activate(n__s(X)) -> s(activate(X)), U11(tt(), V2) -> U12(isNat(activate(V2))), U21(tt()) -> tt(), U31(tt(), N) -> activate(N), U42(tt(), M, N) -> s(plus(activate(N), activate(M))), U41(tt(), M, N) -> U42(isNat(activate(N)), activate(M), activate(N)), s(X) -> n__s(X), plus(N, s(M)) -> U41(isNat(M), M, N), plus(N, 0()) -> U31(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(U41#) = [1,2], pi(U41) = [0,1,2], pi(U42#) = [1,2], pi(U42) = [0,1,2], pi(U31#) = [1], pi(U31) = 1, pi(U21) = 0, pi(tt) = [], pi(U11#) = [1], pi(U11) = 0, pi(activate#) = [0], pi(activate) = 0, pi(isNat#) = [0], pi(isNat) = [], pi(U12) = [] Usable Rules: {} Interpretation: [U41#](x0, x1) = x0 + x1 + 1, [U42#](x0, x1) = x0 + x1 + 1, [plus#](x0, x1) = x0 + x1 + 1, [U31#](x0) = x0 + 1, [U11#](x0) = x0 + 1, [activate#](x0) = x0 + 1, [isNat#](x0) = x0 + 1, [n__plus](x0, x1) = x0 + x1 + 1, [n__s](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 0 Strict: { U11#(tt(), V2) -> isNat#(activate(V2)), U11#(tt(), V2) -> activate#(V2), U31#(tt(), N) -> activate#(N), U42#(tt(), M, N) -> activate#(N), U42#(tt(), M, N) -> activate#(M), U42#(tt(), M, N) -> plus#(activate(N), activate(M)), U41#(tt(), M, N) -> isNat#(activate(N)), U41#(tt(), M, N) -> activate#(N), U41#(tt(), M, N) -> activate#(M), U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U31#(isNat(N), N)} Weak: { U12(tt()) -> tt(), isNat(n__0()) -> tt(), isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)), isNat(n__s(V1)) -> U21(isNat(activate(V1))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)), activate(n__s(X)) -> s(activate(X)), U11(tt(), V2) -> U12(isNat(activate(V2))), U21(tt()) -> tt(), U31(tt(), N) -> activate(N), U42(tt(), M, N) -> s(plus(activate(N), activate(M))), U41(tt(), M, N) -> U42(isNat(activate(N)), activate(M), activate(N)), s(X) -> n__s(X), plus(N, s(M)) -> U41(isNat(M), M, N), plus(N, 0()) -> U31(isNat(N), N), plus(X1, X2) -> n__plus(X1, X2), 0() -> n__0()} EDG: {(U42#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> U31#(isNat(N), N)) (U42#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> isNat#(N)) (plus#(N, 0()) -> U31#(isNat(N), N), U31#(tt(), N) -> activate#(N)) (U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), U42#(tt(), M, N) -> activate#(N)) (U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), U42#(tt(), M, N) -> activate#(M)) (U41#(tt(), M, N) -> U42#(isNat(activate(N)), activate(M), activate(N)), U42#(tt(), M, N) -> plus#(activate(N), activate(M)))} SCCS: Qed