YES TRS: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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)) -> plus#(X1, X2), activate#(n__s(X)) -> s#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), 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#(N), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(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(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(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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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: { (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(isNat(N), n__isNatKind(N))), and#(tt(), X) -> activate#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (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__isNatKind(X)) -> isNatKind#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (isNatKind#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), and#(tt(), X) -> activate#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (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__isNatKind(X)) -> isNatKind#(X)) (isNatKind#(n__plus(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> isNatKind#(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)) -> activate#(V1)) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V2)) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__plus(V1, V2)) -> activate#(V1)) (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__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))) (U41#(tt(), M, N) -> activate#(M), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U41#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U41#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U41#(tt(), M, N) -> activate#(M), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U41#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#()) (plus#(N, s(M)) -> isNat#(N), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (plus#(N, s(M)) -> isNat#(N), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (plus#(N, s(M)) -> isNat#(N), isNat#(n__s(V1)) -> activate#(V1)) (plus#(N, s(M)) -> isNat#(N), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (plus#(N, s(M)) -> isNat#(N), isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (plus#(N, s(M)) -> isNat#(N), isNat#(n__plus(V1, V2)) -> U11#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) (plus#(N, s(M)) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V2)) (plus#(N, s(M)) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V1)) (U41#(tt(), M, N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U41#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U41#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U41#(tt(), M, N) -> activate#(N), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U41#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#()) (plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(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(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(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(isNat(N), n__isNatKind(N))), M, N), U41#(tt(), M, N) -> plus#(activate(N), activate(M))) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V1)) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> 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)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) (plus#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> isNatKind#(activate(V1))) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> 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)) -> isNatKind#(activate(V1))) (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)) -> plus#(X1, X2)) (U31#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U31#(tt(), N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(X1, X2)) (plus#(N, 0()) -> U31#(and(isNat(N), n__isNatKind(N)), N), U31#(tt(), N) -> activate#(N)) (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))) (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))) (and#(tt(), X) -> activate#(X), activate#(n__0()) -> 0#()) (and#(tt(), X) -> activate#(X), activate#(n__isNatKind(X)) -> isNatKind#(X)) (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> s#(X)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (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))) (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)) -> plus#(X1, X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__0()) -> 0#()) (U21#(tt(), V1) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__plus(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), and#(tt(), X) -> activate#(X)) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, s(M)) -> isNat#(N)) (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)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M))) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(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()) -> U31#(and(isNat(N), n__isNatKind(N)), N)) (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, 0()) -> and#(isNat(N), n__isNatKind(N))) (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)) -> plus#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (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)) -> plus#(X1, X2)) (U12#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (U12#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> isNat#(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(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(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)) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> 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) -> U22#(isNat(activate(V1)))) } 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)) -> plus#(X1, X2), activate#(n__and(X1, X2)) -> and#(X1, X2), 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#(N), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(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(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)) -> plus#(X1, X2), activate#(n__and(X1, X2)) -> and#(X1, X2), 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#(N), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(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(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(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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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()} POLY: Argument Filtering: pi(n__and) = 1, pi(0) = [], pi(n__s) = 0, pi(n__plus) = [0,1], pi(n__isNatKind) = 0, pi(isNatKind#) = 0, pi(isNatKind) = 0, pi(n__0) = [], pi(and#) = 1, pi(and) = 1, pi(U41#) = [1,2], pi(U41) = [1,2], pi(plus#) = [0,1], pi(plus) = [0,1], pi(s) = 0, pi(U31#) = 1, pi(U31) = 1, pi(U21#) = 1, pi(U21) = [], pi(U22) = [], pi(U13) = [], pi(tt) = [], pi(U11#) = [1,2], pi(U11) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNat#) = 0, pi(isNat) = [], pi(U12#) = 1, pi(U12) = [] Usable Rules: {} Interpretation: [U41#](x0, x1) = x0 + x1, [U11#](x0, x1) = x0 + x1, [plus#](x0, x1) = x0 + x1, [n__plus](x0, x1) = x0 + x1 + 1, [0] = 0 Strict: { U12#(tt(), V2) -> isNat#(activate(V2)), U12#(tt(), V2) -> activate#(V2), 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__and(X1, X2)) -> and#(X1, X2), 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#(N), plus#(N, s(M)) -> isNat#(M), plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(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(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__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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: {(plus#(N, s(M)) -> isNat#(N), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (plus#(N, s(M)) -> isNat#(N), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (plus#(N, s(M)) -> isNat#(N), isNat#(n__s(V1)) -> activate#(V1)) (U41#(tt(), M, N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U41#(tt(), M, N) -> activate#(N), activate#(n__isNatKind(X)) -> isNatKind#(X)) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (U12#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U12#(tt(), V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U12#(tt(), V2) -> isNat#(activate(V2)), isNat#(n__s(V1)) -> isNatKind#(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)) -> 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)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (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))) (plus#(N, s(M)) -> and#(isNat(M), n__isNatKind(M)), and#(tt(), X) -> activate#(X)) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, 0()) -> and#(isNat(N), n__isNatKind(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()) -> isNat#(N)) (U41#(tt(), M, N) -> plus#(activate(N), activate(M)), plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(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)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, 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)) -> isNat#(N)) (U41#(tt(), M, N) -> activate#(M), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U41#(tt(), M, N) -> activate#(M), activate#(n__isNatKind(X)) -> isNatKind#(X)) (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))) (plus#(N, 0()) -> and#(isNat(N), n__isNatKind(N)), and#(tt(), X) -> activate#(X)) (U11#(tt(), V1, V2) -> U12#(isNat(activate(V1)), activate(V2)), U12#(tt(), V2) -> isNat#(activate(V2))) (U11#(tt(), V1, V2) -> U12#(isNat(activate(V1)), activate(V2)), U12#(tt(), V2) -> activate#(V2)) (plus#(N, 0()) -> U31#(and(isNat(N), n__isNatKind(N)), N), U31#(tt(), N) -> activate#(N)) (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__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U11#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n__isNatKind(X)) -> isNatKind#(X)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U11#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(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(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(isNat(N), n__isNatKind(N))), M, N), U41#(tt(), M, N) -> plus#(activate(N), activate(M))) (plus#(N, s(M)) -> and#(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), and#(tt(), X) -> activate#(X)) (plus#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> 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)) -> isNatKind#(activate(V1))) (U31#(tt(), N) -> activate#(N), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U31#(tt(), N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(X1, X2))} SCCS: Scc: { plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N), U41#(tt(), M, N) -> plus#(activate(N), activate(M))} Scc: {activate#(n__isNatKind(X)) -> isNatKind#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))} Scc: {isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> isNat#(activate(V1))} SCC: Strict: { plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N), U41#(tt(), M, N) -> plus#(activate(N), activate(M))} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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()} POLY: Argument Filtering: pi(n__and) = 1, pi(0) = [], pi(n__s) = [0], pi(n__plus) = [0,1], pi(n__isNatKind) = [], pi(isNatKind) = [], pi(n__0) = [], pi(and) = 1, pi(U41#) = [1], pi(U41) = [1,2], pi(plus#) = 1, pi(plus) = [0,1], pi(s) = [0], pi(U31) = [1], pi(U21) = [], pi(U22) = [], pi(U13) = [], pi(tt) = [], pi(U11) = [], pi(activate) = 0, pi(isNat) = [], pi(U12) = [] Usable Rules: {} Interpretation: [U41#](x0) = x0 + 1, [s](x0) = x0 + 1 Strict: {plus#(N, s(M)) -> U41#(and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))), M, N)} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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: {} SCCS: Qed SCC: Strict: {activate#(n__isNatKind(X)) -> isNatKind#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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()} POLY: Argument Filtering: pi(n__and) = [0,1], pi(0) = [], pi(n__s) = 0, pi(n__plus) = [0,1], pi(n__isNatKind) = [0], pi(isNatKind#) = 0, pi(isNatKind) = [0], pi(n__0) = [], pi(and#) = 1, pi(and) = [0,1], pi(U41) = [1,2], pi(plus) = [0,1], pi(s) = 0, pi(U31) = 1, pi(U21) = [], pi(U22) = [], pi(U13) = [], pi(tt) = [], pi(U11) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNat) = [0], pi(U12) = [] Usable Rules: {} Interpretation: [n__and](x0, x1) = x0 + x1, [n__isNatKind](x0) = x0 + 1 Strict: {activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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: {(activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2))} SCCS: Scc: {isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))} Scc: {activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)} SCC: Strict: {isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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()} POLY: Argument Filtering: pi(n__and) = 1, pi(0) = [], pi(n__s) = [0], pi(n__plus) = [0,1], pi(n__isNatKind) = [], pi(isNatKind#) = 0, pi(isNatKind) = [], pi(n__0) = [], pi(and) = 1, pi(U41) = [1,2], pi(plus) = [0,1], pi(s) = [0], pi(U31) = 1, pi(U21) = [], pi(U22) = [], pi(U13) = [], pi(tt) = [], pi(U11) = [], pi(activate) = 0, pi(isNat) = [], pi(U12) = [] Usable Rules: {} Interpretation: [n__s](x0) = x0 + 1 Strict: {} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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()} Qed SCC: Strict: {activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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()} SPSC: Simple Projection: pi(and#) = 1, pi(activate#) = 0 Strict: {and#(tt(), X) -> activate#(X)} EDG: {} SCCS: Qed SCC: Strict: {isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> isNat#(activate(V1))} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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()} POLY: Argument Filtering: pi(n__and) = 1, pi(0) = [], pi(n__s) = [0], pi(n__plus) = [0,1], pi(n__isNatKind) = [], pi(isNatKind) = [], pi(n__0) = [], pi(and) = 1, pi(U41) = [1,2], pi(plus) = [0,1], pi(s) = [0], pi(U31) = 1, pi(U21#) = 1, pi(U21) = [], pi(U22) = [], pi(U13) = [], pi(tt) = [], pi(U11) = [], pi(activate) = 0, pi(isNat#) = 0, pi(isNat) = [], pi(U12) = [] Usable Rules: {} Interpretation: [n__s](x0) = x0 + 1 Strict: {U21#(tt(), V1) -> isNat#(activate(V1))} Weak: { U12(tt(), V2) -> U13(isNat(activate(V2))), 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(X1, X2), activate(n__s(X)) -> s(X), activate(n__and(X1, X2)) -> and(X1, X2), 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(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: {} SCCS: Qed