MAYBE TRS: { U12(tt(), V2) -> U13(isNat(activate(V2))), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__plus(V1, V2)) -> U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)), activate(X) -> X, activate(n__0()) -> 0(), activate(n__isNatKind(X)) -> isNatKind(X), activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)), activate(n__s(X)) -> s(activate(X)), activate(n__and(X1, X2)) -> and(activate(X1), X2), activate(n__isNat(X)) -> isNat(X), U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)), U13(tt()) -> tt(), U22(tt()) -> tt(), U21(tt(), V1) -> U22(isNat(activate(V1))), U31(tt(), N) -> activate(N), s(X) -> n__s(X), plus(N, s(M)) -> U41(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), plus(N, 0()) -> U31(and(isNat(N), n__isNatKind(N)), N), plus(X1, X2) -> n__plus(X1, X2), U41(tt(), M, N) -> s(plus(activate(N), activate(M))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNatKind(X) -> n__isNatKind(X), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), isNatKind(n__s(V1)) -> isNatKind(activate(V1)), 0() -> n__0()} DP: Strict: { U12#(tt(), V2) -> isNat#(activate(V2)), U12#(tt(), V2) -> activate#(V2), U12#(tt(), V2) -> U13#(isNat(activate(V2))), isNat#(n__plus(V1, V2)) -> activate#(V1), isNat#(n__plus(V1, V2)) -> activate#(V2), isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1)), activate#(n__0()) -> 0#(), activate#(n__isNatKind(X)) -> isNatKind#(X), 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)), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2), activate#(n__isNat(X)) -> isNat#(X), U11#(tt(), V1, V2) -> U12#(isNat(activate(V1)), activate(V2)), U11#(tt(), V1, V2) -> isNat#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> activate#(V2), U21#(tt(), V1) -> isNat#(activate(V1)), U21#(tt(), V1) -> activate#(V1), U21#(tt(), V1) -> U22#(isNat(activate(V1))), U31#(tt(), N) -> activate#(N), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M)), plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U31#(and(isNat(N), n__isNatKind(N)), N), plus#(N, 0()) -> and#(isNat(N), n__isNatKind(N)), U41#(tt(), M, N) -> activate#(N), U41#(tt(), M, N) -> activate#(M), U41#(tt(), M, N) -> s#(plus(activate(N), activate(M))), U41#(tt(), M, N) -> plus#(activate(N), activate(M)), and#(tt(), X) -> activate#(X), isNatKind#(n__plus(V1, V2)) -> activate#(V1), isNatKind#(n__plus(V1, V2)) -> activate#(V2), isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__plus(V1, V2)) -> U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)), activate(X) -> X, activate(n__0()) -> 0(), activate(n__isNatKind(X)) -> isNatKind(X), activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)), activate(n__s(X)) -> s(activate(X)), activate(n__and(X1, X2)) -> and(activate(X1), X2), activate(n__isNat(X)) -> isNat(X), U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)), U13(tt()) -> tt(), U22(tt()) -> tt(), U21(tt(), V1) -> U22(isNat(activate(V1))), U31(tt(), N) -> activate(N), s(X) -> n__s(X), plus(N, s(M)) -> U41(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), plus(N, 0()) -> U31(and(isNat(N), n__isNatKind(N)), N), plus(X1, X2) -> n__plus(X1, X2), U41(tt(), M, N) -> s(plus(activate(N), activate(M))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNatKind(X) -> n__isNatKind(X), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), isNatKind(n__s(V1)) -> isNatKind(activate(V1)), 0() -> n__0()} EDG: { (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__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(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)) (U11#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U11#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U11#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U11#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U11#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (U11#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) (U11#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U11#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__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)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> U22#(isNat(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) -> isNat#(activate(V1))) (U11#(tt(), V1, V2) -> U12#(isNat(activate(V1)), activate(V2)), U12#(tt(), V2) -> U13#(isNat(activate(V2)))) (U11#(tt(), V1, V2) -> U12#(isNat(activate(V1)), activate(V2)), U12#(tt(), V2) -> activate#(V2)) (U11#(tt(), V1, V2) -> U12#(isNat(activate(V1)), activate(V2)), U12#(tt(), V2) -> isNat#(activate(V2))) (plus#(N, 0()) -> and#(isNat(N), n__isNatKind(N)), and#(tt(), X) -> activate#(X)) (plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), and#(tt(), X) -> activate#(X)) (isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> activate#(V2)) (isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> activate#(V1)) (isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> isNat#(activate(V1))) (isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), U11#(tt(), V1, V2) -> U12#(isNat(activate(V1)), activate(V2))) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__and(X1, X2)) -> activate#(X1)) (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__isNatKind(X)) -> isNatKind#(X)) (activate#(n__plus(X1, X2)) -> activate#(X2), activate#(n__0()) -> 0#()) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X2)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (activate#(n__s(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (activate#(n__s(X)) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatKind(X)) -> isNatKind#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__0()) -> 0#()) (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X2)) (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__isNatKind(X)) -> isNatKind#(X)) (and#(tt(), X) -> activate#(X), activate#(n__0()) -> 0#()) (U41#(tt(), M, N) -> activate#(M), activate#(n__isNat(X)) -> isNat#(X)) (U41#(tt(), M, N) -> activate#(M), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U41#(tt(), M, N) -> activate#(M), activate#(n__and(X1, X2)) -> activate#(X1)) (U41#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(activate(X))) (U41#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (U41#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U41#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X2)) (U41#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> activate#(X1)) (U41#(tt(), M, N) -> activate#(M), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U41#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> activate#(V1)) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 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)) (isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), and#(tt(), X) -> activate#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (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__plus(X1, X2)) -> activate#(X2)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X1)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X1)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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__isNatKind(X)) -> isNatKind#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (U21#(tt(), V1) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (U21#(tt(), V1) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (U21#(tt(), V1) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U21#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1)) (U21#(tt(), V1) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), U41#(tt(), M, N) -> activate#(N)) (plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), U41#(tt(), M, N) -> activate#(M)) (plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), U41#(tt(), M, N) -> s#(plus(activate(N), activate(M)))) (plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), U41#(tt(), M, N) -> plus#(activate(N), activate(M))) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X1)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> activate#(X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (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))) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X1)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X2)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (U12#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U12#(tt(), V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U12#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X1)) (U12#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> activate#(X2)) (U12#(tt(), V2) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U12#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U12#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U12#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (U12#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U12#(tt(), V2) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), and#(tt(), X) -> activate#(X)) (U41#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U41#(tt(), M, N) -> activate#(N), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U41#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1)) (U41#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2)) (U41#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U41#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U41#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (U41#(tt(), M, N) -> activate#(N), activate#(n__and(X1, X2)) -> activate#(X1)) (U41#(tt(), M, N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U41#(tt(), M, N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), N) -> activate#(N), activate#(n__0()) -> 0#()) (U31#(tt(), N) -> activate#(N), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U31#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X1)) (U31#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> activate#(X2)) (U31#(tt(), N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2))) (U31#(tt(), N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U31#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (U31#(tt(), N) -> activate#(N), activate#(n__and(X1, X2)) -> activate#(X1)) (U31#(tt(), N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U31#(tt(), N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X)) (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#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> 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))) (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> activate#(V2)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__s(V1)) -> activate#(V1)) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__plus(X1, X2)) -> activate#(X1)) (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)) -> plus#(activate(X1), activate(X2))) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__plus(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (plus#(N, 0()) -> U31#(and(isNat(N), n__isNatKind(N)), N), U31#(tt(), N) -> activate#(N)) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(M)) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M))) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> isNat#(N)) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> U31#(and(isNat(N), n__isNatKind(N)), N)) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> and#(isNat(N), n__isNatKind(N))) (plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M)), and#(tt(), X) -> activate#(X)) (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, s(M)) -> isNat#(M)) (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M))) (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(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, 0()) -> U31#(and(isNat(N), n__isNatKind(N)), N)) (activate#(n__plus(X1, X2)) -> plus#(activate(X1), activate(X2)), plus#(N, 0()) -> and#(isNat(N), n__isNatKind(N))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> activate#(V2)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (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)) -> activate#(V2)) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(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))) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> activate#(V1)) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (activate#(n__and(X1, X2)) -> and#(activate(X1), X2), and#(tt(), X) -> activate#(X)) } SCCS: Scc: { U12#(tt(), V2) -> isNat#(activate(V2)), U12#(tt(), V2) -> activate#(V2), isNat#(n__plus(V1, V2)) -> activate#(V1), isNat#(n__plus(V1, V2)) -> activate#(V2), isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1)), activate#(n__isNatKind(X)) -> isNatKind#(X), 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__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2), activate#(n__isNat(X)) -> isNat#(X), U11#(tt(), V1, V2) -> U12#(isNat(activate(V1)), activate(V2)), U11#(tt(), V1, V2) -> isNat#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> activate#(V2), U21#(tt(), V1) -> isNat#(activate(V1)), U21#(tt(), V1) -> activate#(V1), U31#(tt(), N) -> activate#(N), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M)), plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U31#(and(isNat(N), n__isNatKind(N)), N), plus#(N, 0()) -> and#(isNat(N), n__isNatKind(N)), U41#(tt(), M, N) -> activate#(N), U41#(tt(), M, N) -> activate#(M), U41#(tt(), M, N) -> plus#(activate(N), activate(M)), and#(tt(), X) -> activate#(X), isNatKind#(n__plus(V1, V2)) -> activate#(V1), isNatKind#(n__plus(V1, V2)) -> activate#(V2), isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))} SCC: Strict: { U12#(tt(), V2) -> isNat#(activate(V2)), U12#(tt(), V2) -> activate#(V2), isNat#(n__plus(V1, V2)) -> activate#(V1), isNat#(n__plus(V1, V2)) -> activate#(V2), isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1)), activate#(n__isNatKind(X)) -> isNatKind#(X), 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__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2), activate#(n__isNat(X)) -> isNat#(X), U11#(tt(), V1, V2) -> U12#(isNat(activate(V1)), activate(V2)), U11#(tt(), V1, V2) -> isNat#(activate(V1)), U11#(tt(), V1, V2) -> activate#(V1), U11#(tt(), V1, V2) -> activate#(V2), U21#(tt(), V1) -> isNat#(activate(V1)), U21#(tt(), V1) -> activate#(V1), U31#(tt(), N) -> activate#(N), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M)), plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), plus#(N, 0()) -> isNat#(N), plus#(N, 0()) -> U31#(and(isNat(N), n__isNatKind(N)), N), plus#(N, 0()) -> and#(isNat(N), n__isNatKind(N)), U41#(tt(), M, N) -> activate#(N), U41#(tt(), M, N) -> activate#(M), U41#(tt(), M, N) -> plus#(activate(N), activate(M)), and#(tt(), X) -> activate#(X), isNatKind#(n__plus(V1, V2)) -> activate#(V1), isNatKind#(n__plus(V1, V2)) -> activate#(V2), isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), isNatKind#(n__plus(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__plus(V1, V2)) -> U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)), isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)), activate(X) -> X, activate(n__0()) -> 0(), activate(n__isNatKind(X)) -> isNatKind(X), activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)), activate(n__s(X)) -> s(activate(X)), activate(n__and(X1, X2)) -> and(activate(X1), X2), activate(n__isNat(X)) -> isNat(X), U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)), U13(tt()) -> tt(), U22(tt()) -> tt(), U21(tt(), V1) -> U22(isNat(activate(V1))), U31(tt(), N) -> activate(N), s(X) -> n__s(X), plus(N, s(M)) -> U41(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N), plus(N, 0()) -> U31(and(isNat(N), n__isNatKind(N)), N), plus(X1, X2) -> n__plus(X1, X2), U41(tt(), M, N) -> s(plus(activate(N), activate(M))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNatKind(X) -> n__isNatKind(X), isNatKind(n__0()) -> tt(), isNatKind(n__plus(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), isNatKind(n__s(V1)) -> isNatKind(activate(V1)), 0() -> n__0()} Fail