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