MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) , 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)) , isNat(n__x(V1, V2)) -> U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) , activate(n__isNatKind(X)) -> isNatKind(X) , activate(n__s(X)) -> s(activate(X)) , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNat(X)) -> isNat(X) , U13(tt()) -> tt() , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) , U32(tt(), V2) -> U33(isNat(activate(V2))) , U33(tt()) -> tt() , U41(tt(), N) -> activate(N) , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , plus(N, s(M)) -> U51(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) , U61(tt()) -> 0() , 0() -> n__0() , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) , x(X1, X2) -> n__x(X1, X2) , x(N, s(M)) -> U71(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) , 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)) , isNatKind(n__x(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , U13^#(tt()) -> c_16() , isNat^#(X) -> c_3(X) , isNat^#(n__0()) -> c_4() , isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__0()) -> c_9(0^#()) , activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , activate^#(n__s(X)) -> c_12(s^#(activate(X))) , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , 0^#() -> c_29() , plus^#(X1, X2) -> c_25(X1, X2) , plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , isNatKind^#(X) -> c_36(X) , isNatKind^#(n__0()) -> c_37() , isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , s^#(X) -> c_24(X) , x^#(X1, X2) -> c_31(X1, X2) , x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , and^#(X1, X2) -> c_34(X1, X2) , and^#(tt(), X) -> c_35(activate^#(X)) , U22^#(tt()) -> c_18() , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , U33^#(tt()) -> c_21() , U41^#(tt(), N) -> c_22(activate^#(N)) , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , U61^#(tt()) -> c_28(0^#()) , U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , U13^#(tt()) -> c_16() , isNat^#(X) -> c_3(X) , isNat^#(n__0()) -> c_4() , isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__0()) -> c_9(0^#()) , activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , activate^#(n__s(X)) -> c_12(s^#(activate(X))) , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , 0^#() -> c_29() , plus^#(X1, X2) -> c_25(X1, X2) , plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , isNatKind^#(X) -> c_36(X) , isNatKind^#(n__0()) -> c_37() , isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , s^#(X) -> c_24(X) , x^#(X1, X2) -> c_31(X1, X2) , x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , and^#(X1, X2) -> c_34(X1, X2) , and^#(tt(), X) -> c_35(activate^#(X)) , U22^#(tt()) -> c_18() , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , U33^#(tt()) -> c_21() , U41^#(tt(), N) -> c_22(activate^#(N)) , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , U61^#(tt()) -> c_28(0^#()) , U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) } Strict Trs: { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) , 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)) , isNat(n__x(V1, V2)) -> U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) , activate(n__isNatKind(X)) -> isNatKind(X) , activate(n__s(X)) -> s(activate(X)) , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNat(X)) -> isNat(X) , U13(tt()) -> tt() , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) , U32(tt(), V2) -> U33(isNat(activate(V2))) , U33(tt()) -> tt() , U41(tt(), N) -> activate(N) , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , plus(N, s(M)) -> U51(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) , U61(tt()) -> 0() , 0() -> n__0() , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) , x(X1, X2) -> n__x(X1, X2) , x(N, s(M)) -> U71(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) , 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)) , isNatKind(n__x(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {3,5,19,24,34,36} by applications of Pre({3,5,19,24,34,36}) = {2,4,9,11,12,14,18,20,23,26,28,29,32,35,39}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , 2: U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , 3: U13^#(tt()) -> c_16() , 4: isNat^#(X) -> c_3(X) , 5: isNat^#(n__0()) -> c_4() , 6: isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , 7: isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , 8: isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , 9: U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , 10: U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , 11: activate^#(X) -> c_8(X) , 12: activate^#(n__0()) -> c_9(0^#()) , 13: activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , 14: activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , 15: activate^#(n__s(X)) -> c_12(s^#(activate(X))) , 16: activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , 17: activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , 18: activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , 19: 0^#() -> c_29() , 20: plus^#(X1, X2) -> c_25(X1, X2) , 21: plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , 22: plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , 23: isNatKind^#(X) -> c_36(X) , 24: isNatKind^#(n__0()) -> c_37() , 25: isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , 26: isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , 27: isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , 28: s^#(X) -> c_24(X) , 29: x^#(X1, X2) -> c_31(X1, X2) , 30: x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , 31: x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , 32: and^#(X1, X2) -> c_34(X1, X2) , 33: and^#(tt(), X) -> c_35(activate^#(X)) , 34: U22^#(tt()) -> c_18() , 35: U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , 36: U33^#(tt()) -> c_21() , 37: U41^#(tt(), N) -> c_22(activate^#(N)) , 38: U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , 39: U61^#(tt()) -> c_28(0^#()) , 40: U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , isNat^#(X) -> c_3(X) , isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__0()) -> c_9(0^#()) , activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , activate^#(n__s(X)) -> c_12(s^#(activate(X))) , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , plus^#(X1, X2) -> c_25(X1, X2) , plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , isNatKind^#(X) -> c_36(X) , isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , s^#(X) -> c_24(X) , x^#(X1, X2) -> c_31(X1, X2) , x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , and^#(X1, X2) -> c_34(X1, X2) , and^#(tt(), X) -> c_35(activate^#(X)) , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , U41^#(tt(), N) -> c_22(activate^#(N)) , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , U61^#(tt()) -> c_28(0^#()) , U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) } Strict Trs: { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) , 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)) , isNat(n__x(V1, V2)) -> U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) , activate(n__isNatKind(X)) -> isNatKind(X) , activate(n__s(X)) -> s(activate(X)) , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNat(X)) -> isNat(X) , U13(tt()) -> tt() , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) , U32(tt(), V2) -> U33(isNat(activate(V2))) , U33(tt()) -> tt() , U41(tt(), N) -> activate(N) , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , plus(N, s(M)) -> U51(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) , U61(tt()) -> 0() , 0() -> n__0() , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) , x(X1, X2) -> n__x(X1, X2) , x(N, s(M)) -> U71(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) , 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)) , isNatKind(n__x(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } Weak DPs: { U13^#(tt()) -> c_16() , isNat^#(n__0()) -> c_4() , 0^#() -> c_29() , isNatKind^#(n__0()) -> c_37() , U22^#(tt()) -> c_18() , U33^#(tt()) -> c_21() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,7,10,30,33} by applications of Pre({2,7,10,30,33}) = {1,3,5,8,9,17,20,24,25,27,28,29,31}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , 2: U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , 3: isNat^#(X) -> c_3(X) , 4: isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , 5: isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , 6: isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , 7: U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , 8: U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , 9: activate^#(X) -> c_8(X) , 10: activate^#(n__0()) -> c_9(0^#()) , 11: activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , 12: activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , 13: activate^#(n__s(X)) -> c_12(s^#(activate(X))) , 14: activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , 15: activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , 16: activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , 17: plus^#(X1, X2) -> c_25(X1, X2) , 18: plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , 19: plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , 20: isNatKind^#(X) -> c_36(X) , 21: isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , 22: isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , 23: isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , 24: s^#(X) -> c_24(X) , 25: x^#(X1, X2) -> c_31(X1, X2) , 26: x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , 27: x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , 28: and^#(X1, X2) -> c_34(X1, X2) , 29: and^#(tt(), X) -> c_35(activate^#(X)) , 30: U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , 31: U41^#(tt(), N) -> c_22(activate^#(N)) , 32: U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , 33: U61^#(tt()) -> c_28(0^#()) , 34: U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) , 35: U13^#(tt()) -> c_16() , 36: isNat^#(n__0()) -> c_4() , 37: 0^#() -> c_29() , 38: isNatKind^#(n__0()) -> c_37() , 39: U22^#(tt()) -> c_18() , 40: U33^#(tt()) -> c_21() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , isNat^#(X) -> c_3(X) , isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , activate^#(n__s(X)) -> c_12(s^#(activate(X))) , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , plus^#(X1, X2) -> c_25(X1, X2) , plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , isNatKind^#(X) -> c_36(X) , isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , s^#(X) -> c_24(X) , x^#(X1, X2) -> c_31(X1, X2) , x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , and^#(X1, X2) -> c_34(X1, X2) , and^#(tt(), X) -> c_35(activate^#(X)) , U41^#(tt(), N) -> c_22(activate^#(N)) , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) } Strict Trs: { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) , 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)) , isNat(n__x(V1, V2)) -> U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) , activate(n__isNatKind(X)) -> isNatKind(X) , activate(n__s(X)) -> s(activate(X)) , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNat(X)) -> isNat(X) , U13(tt()) -> tt() , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) , U32(tt(), V2) -> U33(isNat(activate(V2))) , U33(tt()) -> tt() , U41(tt(), N) -> activate(N) , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , plus(N, s(M)) -> U51(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) , U61(tt()) -> 0() , 0() -> n__0() , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) , x(X1, X2) -> n__x(X1, X2) , x(N, s(M)) -> U71(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) , 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)) , isNatKind(n__x(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } Weak DPs: { U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , U13^#(tt()) -> c_16() , isNat^#(n__0()) -> c_4() , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , activate^#(n__0()) -> c_9(0^#()) , 0^#() -> c_29() , isNatKind^#(n__0()) -> c_37() , U22^#(tt()) -> c_18() , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , U33^#(tt()) -> c_21() , U61^#(tt()) -> c_28(0^#()) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,4,6,24} by applications of Pre({1,4,6,24}) = {2,3,5,7,11,13,14,17,21,22,25}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , 2: isNat^#(X) -> c_3(X) , 3: isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , 4: isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , 5: isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , 6: U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , 7: activate^#(X) -> c_8(X) , 8: activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , 9: activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , 10: activate^#(n__s(X)) -> c_12(s^#(activate(X))) , 11: activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , 12: activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , 13: activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , 14: plus^#(X1, X2) -> c_25(X1, X2) , 15: plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , 16: plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , 17: isNatKind^#(X) -> c_36(X) , 18: isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , 19: isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , 20: isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , 21: s^#(X) -> c_24(X) , 22: x^#(X1, X2) -> c_31(X1, X2) , 23: x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , 24: x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , 25: and^#(X1, X2) -> c_34(X1, X2) , 26: and^#(tt(), X) -> c_35(activate^#(X)) , 27: U41^#(tt(), N) -> c_22(activate^#(N)) , 28: U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , 29: U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) , 30: U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , 31: U13^#(tt()) -> c_16() , 32: isNat^#(n__0()) -> c_4() , 33: U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , 34: activate^#(n__0()) -> c_9(0^#()) , 35: 0^#() -> c_29() , 36: isNatKind^#(n__0()) -> c_37() , 37: U22^#(tt()) -> c_18() , 38: U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , 39: U33^#(tt()) -> c_21() , 40: U61^#(tt()) -> c_28(0^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isNat^#(X) -> c_3(X) , isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , activate^#(n__s(X)) -> c_12(s^#(activate(X))) , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , plus^#(X1, X2) -> c_25(X1, X2) , plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , isNatKind^#(X) -> c_36(X) , isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , s^#(X) -> c_24(X) , x^#(X1, X2) -> c_31(X1, X2) , x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , and^#(X1, X2) -> c_34(X1, X2) , and^#(tt(), X) -> c_35(activate^#(X)) , U41^#(tt(), N) -> c_22(activate^#(N)) , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) } Strict Trs: { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) , 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)) , isNat(n__x(V1, V2)) -> U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) , activate(n__isNatKind(X)) -> isNatKind(X) , activate(n__s(X)) -> s(activate(X)) , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNat(X)) -> isNat(X) , U13(tt()) -> tt() , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) , U32(tt(), V2) -> U33(isNat(activate(V2))) , U33(tt()) -> tt() , U41(tt(), N) -> activate(N) , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , plus(N, s(M)) -> U51(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) , U61(tt()) -> 0() , 0() -> n__0() , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) , x(X1, X2) -> n__x(X1, X2) , x(N, s(M)) -> U71(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) , 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)) , isNatKind(n__x(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , U13^#(tt()) -> c_16() , isNat^#(n__0()) -> c_4() , isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , activate^#(n__0()) -> c_9(0^#()) , 0^#() -> c_29() , isNatKind^#(n__0()) -> c_37() , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , U22^#(tt()) -> c_18() , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , U33^#(tt()) -> c_21() , U61^#(tt()) -> c_28(0^#()) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,3} by applications of Pre({2,3}) = {1,4,10,11,14,18,19,21}. Here rules are labeled as follows: DPs: { 1: isNat^#(X) -> c_3(X) , 2: isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , 3: isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , 4: activate^#(X) -> c_8(X) , 5: activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , 6: activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , 7: activate^#(n__s(X)) -> c_12(s^#(activate(X))) , 8: activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , 9: activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , 10: activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , 11: plus^#(X1, X2) -> c_25(X1, X2) , 12: plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , 13: plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , 14: isNatKind^#(X) -> c_36(X) , 15: isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , 16: isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , 17: isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , 18: s^#(X) -> c_24(X) , 19: x^#(X1, X2) -> c_31(X1, X2) , 20: x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , 21: and^#(X1, X2) -> c_34(X1, X2) , 22: and^#(tt(), X) -> c_35(activate^#(X)) , 23: U41^#(tt(), N) -> c_22(activate^#(N)) , 24: U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , 25: U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) , 26: U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , 27: U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , 28: U13^#(tt()) -> c_16() , 29: isNat^#(n__0()) -> c_4() , 30: isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , 31: U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , 32: U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , 33: activate^#(n__0()) -> c_9(0^#()) , 34: 0^#() -> c_29() , 35: isNatKind^#(n__0()) -> c_37() , 36: x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , 37: U22^#(tt()) -> c_18() , 38: U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , 39: U33^#(tt()) -> c_21() , 40: U61^#(tt()) -> c_28(0^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isNat^#(X) -> c_3(X) , activate^#(X) -> c_8(X) , activate^#(n__plus(X1, X2)) -> c_10(plus^#(activate(X1), activate(X2))) , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) , activate^#(n__s(X)) -> c_12(s^#(activate(X))) , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) , plus^#(X1, X2) -> c_25(X1, X2) , plus^#(N, s(M)) -> c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) , isNatKind^#(X) -> c_36(X) , isNatKind^#(n__plus(V1, V2)) -> c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) , isNatKind^#(n__x(V1, V2)) -> c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) , s^#(X) -> c_24(X) , x^#(X1, X2) -> c_31(X1, X2) , x^#(N, s(M)) -> c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)) , and^#(X1, X2) -> c_34(X1, X2) , and^#(tt(), X) -> c_35(activate^#(X)) , U41^#(tt(), N) -> c_22(activate^#(N)) , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) , U71^#(tt(), M, N) -> c_30(plus^#(x(activate(N), activate(M)), activate(N))) } Strict Trs: { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) , 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)) , isNat(n__x(V1, V2)) -> U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) , activate(n__isNatKind(X)) -> isNatKind(X) , activate(n__s(X)) -> s(activate(X)) , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNat(X)) -> isNat(X) , U13(tt()) -> tt() , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) , U32(tt(), V2) -> U33(isNat(activate(V2))) , U33(tt()) -> tt() , U41(tt(), N) -> activate(N) , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , plus(N, s(M)) -> U51(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) , U61(tt()) -> 0() , 0() -> n__0() , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) , x(X1, X2) -> n__x(X1, X2) , x(N, s(M)) -> U71(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N) , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) , 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)) , isNatKind(n__x(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNat(activate(V1)), activate(V2))) , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) , U13^#(tt()) -> c_16() , isNat^#(n__0()) -> c_4() , isNat^#(n__plus(V1, V2)) -> c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_6(U21^#(isNatKind(activate(V1)), activate(V1))) , isNat^#(n__x(V1, V2)) -> c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))) , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) , U31^#(tt(), V1, V2) -> c_19(U32^#(isNat(activate(V1)), activate(V2))) , activate^#(n__0()) -> c_9(0^#()) , 0^#() -> c_29() , isNatKind^#(n__0()) -> c_37() , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) , U22^#(tt()) -> c_18() , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) , U33^#(tt()) -> c_21() , U61^#(tt()) -> c_28(0^#()) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..