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