MAYBE 1046.89/297.03 MAYBE 1046.89/297.03 1046.89/297.03 We are left with following problem, upon which TcT provides the 1046.89/297.03 certificate MAYBE. 1046.89/297.03 1046.89/297.03 Strict Trs: 1046.89/297.03 { active(terms(X)) -> terms(active(X)) 1046.89/297.03 , active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))) 1046.89/297.03 , active(cons(X1, X2)) -> cons(active(X1), X2) 1046.89/297.03 , active(recip(X)) -> recip(active(X)) 1046.89/297.03 , active(sqr(X)) -> sqr(active(X)) 1046.89/297.03 , active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))) 1046.89/297.03 , active(sqr(0())) -> mark(0()) 1046.89/297.03 , active(add(X1, X2)) -> add(X1, active(X2)) 1046.89/297.03 , active(add(X1, X2)) -> add(active(X1), X2) 1046.89/297.03 , active(add(s(X), Y)) -> mark(s(add(X, Y))) 1046.89/297.03 , active(add(0(), X)) -> mark(X) 1046.89/297.03 , active(dbl(X)) -> dbl(active(X)) 1046.89/297.03 , active(dbl(s(X))) -> mark(s(s(dbl(X)))) 1046.89/297.03 , active(dbl(0())) -> mark(0()) 1046.89/297.03 , active(first(X1, X2)) -> first(X1, active(X2)) 1046.89/297.03 , active(first(X1, X2)) -> first(active(X1), X2) 1046.89/297.03 , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) 1046.89/297.03 , active(first(0(), X)) -> mark(nil()) 1046.89/297.03 , terms(mark(X)) -> mark(terms(X)) 1046.89/297.03 , terms(ok(X)) -> ok(terms(X)) 1046.89/297.03 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1046.89/297.03 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1046.89/297.03 , recip(mark(X)) -> mark(recip(X)) 1046.89/297.03 , recip(ok(X)) -> ok(recip(X)) 1046.89/297.03 , sqr(mark(X)) -> mark(sqr(X)) 1046.89/297.03 , sqr(ok(X)) -> ok(sqr(X)) 1046.89/297.03 , s(ok(X)) -> ok(s(X)) 1046.89/297.03 , add(X1, mark(X2)) -> mark(add(X1, X2)) 1046.89/297.03 , add(mark(X1), X2) -> mark(add(X1, X2)) 1046.89/297.03 , add(ok(X1), ok(X2)) -> ok(add(X1, X2)) 1046.89/297.03 , dbl(mark(X)) -> mark(dbl(X)) 1046.89/297.03 , dbl(ok(X)) -> ok(dbl(X)) 1046.89/297.03 , first(X1, mark(X2)) -> mark(first(X1, X2)) 1046.89/297.03 , first(mark(X1), X2) -> mark(first(X1, X2)) 1046.89/297.03 , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) 1046.89/297.03 , proper(terms(X)) -> terms(proper(X)) 1046.89/297.03 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1046.89/297.03 , proper(recip(X)) -> recip(proper(X)) 1046.89/297.03 , proper(sqr(X)) -> sqr(proper(X)) 1046.89/297.03 , proper(s(X)) -> s(proper(X)) 1046.89/297.03 , proper(0()) -> ok(0()) 1046.89/297.03 , proper(add(X1, X2)) -> add(proper(X1), proper(X2)) 1046.89/297.03 , proper(dbl(X)) -> dbl(proper(X)) 1046.89/297.03 , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) 1046.89/297.03 , proper(nil()) -> ok(nil()) 1046.89/297.03 , top(mark(X)) -> top(proper(X)) 1046.89/297.03 , top(ok(X)) -> top(active(X)) } 1046.89/297.03 Obligation: 1046.89/297.03 runtime complexity 1046.89/297.03 Answer: 1046.89/297.03 MAYBE 1046.89/297.03 1046.89/297.03 None of the processors succeeded. 1046.89/297.03 1046.89/297.03 Details of failed attempt(s): 1046.89/297.03 ----------------------------- 1046.89/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1046.89/297.03 following reason: 1046.89/297.03 1046.89/297.03 Computation stopped due to timeout after 297.0 seconds. 1046.89/297.03 1046.89/297.03 2) 'Best' failed due to the following reason: 1046.89/297.03 1046.89/297.03 None of the processors succeeded. 1046.89/297.03 1046.89/297.03 Details of failed attempt(s): 1046.89/297.03 ----------------------------- 1046.89/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1046.89/297.03 seconds)' failed due to the following reason: 1046.89/297.03 1046.89/297.03 Computation stopped due to timeout after 148.0 seconds. 1046.89/297.03 1046.89/297.03 2) 'Best' failed due to the following reason: 1046.89/297.03 1046.89/297.03 None of the processors succeeded. 1046.89/297.03 1046.89/297.03 Details of failed attempt(s): 1046.89/297.03 ----------------------------- 1046.89/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1046.89/297.03 following reason: 1046.89/297.03 1046.89/297.03 The processor is inapplicable, reason: 1046.89/297.03 Processor only applicable for innermost runtime complexity analysis 1046.89/297.03 1046.89/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1046.89/297.03 to the following reason: 1046.89/297.03 1046.89/297.03 The processor is inapplicable, reason: 1046.89/297.03 Processor only applicable for innermost runtime complexity analysis 1046.89/297.03 1046.89/297.03 1046.89/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1046.89/297.03 failed due to the following reason: 1046.89/297.03 1046.89/297.03 None of the processors succeeded. 1046.89/297.03 1046.89/297.03 Details of failed attempt(s): 1046.89/297.03 ----------------------------- 1046.89/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1046.89/297.03 failed due to the following reason: 1046.89/297.03 1046.89/297.03 match-boundness of the problem could not be verified. 1046.89/297.03 1046.89/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1046.89/297.03 failed due to the following reason: 1046.89/297.03 1046.89/297.03 match-boundness of the problem could not be verified. 1046.89/297.03 1046.89/297.03 1046.89/297.03 1046.89/297.03 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1046.89/297.03 the following reason: 1046.89/297.03 1046.89/297.03 We add the following weak dependency pairs: 1046.89/297.03 1046.89/297.03 Strict DPs: 1046.89/297.03 { active^#(terms(X)) -> c_1(terms^#(active(X))) 1046.89/297.03 , active^#(terms(N)) -> c_2(cons^#(recip(sqr(N)), terms(s(N)))) 1046.89/297.03 , active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1046.89/297.03 , active^#(recip(X)) -> c_4(recip^#(active(X))) 1046.89/297.03 , active^#(sqr(X)) -> c_5(sqr^#(active(X))) 1046.89/297.03 , active^#(sqr(s(X))) -> c_6(s^#(add(sqr(X), dbl(X)))) 1046.89/297.03 , active^#(sqr(0())) -> c_7() 1046.89/297.03 , active^#(add(X1, X2)) -> c_8(add^#(X1, active(X2))) 1046.89/297.03 , active^#(add(X1, X2)) -> c_9(add^#(active(X1), X2)) 1046.89/297.03 , active^#(add(s(X), Y)) -> c_10(s^#(add(X, Y))) 1046.89/297.03 , active^#(add(0(), X)) -> c_11(X) 1046.89/297.03 , active^#(dbl(X)) -> c_12(dbl^#(active(X))) 1046.89/297.03 , active^#(dbl(s(X))) -> c_13(s^#(s(dbl(X)))) 1046.89/297.03 , active^#(dbl(0())) -> c_14() 1046.89/297.03 , active^#(first(X1, X2)) -> c_15(first^#(X1, active(X2))) 1046.89/297.03 , active^#(first(X1, X2)) -> c_16(first^#(active(X1), X2)) 1046.89/297.03 , active^#(first(s(X), cons(Y, Z))) -> c_17(cons^#(Y, first(X, Z))) 1046.89/297.03 , active^#(first(0(), X)) -> c_18() 1046.89/297.03 , terms^#(mark(X)) -> c_19(terms^#(X)) 1046.89/297.03 , terms^#(ok(X)) -> c_20(terms^#(X)) 1046.89/297.03 , cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 1046.89/297.03 , cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 1046.89/297.03 , recip^#(mark(X)) -> c_23(recip^#(X)) 1046.89/297.03 , recip^#(ok(X)) -> c_24(recip^#(X)) 1046.89/297.03 , sqr^#(mark(X)) -> c_25(sqr^#(X)) 1046.89/297.03 , sqr^#(ok(X)) -> c_26(sqr^#(X)) 1046.89/297.03 , s^#(ok(X)) -> c_27(s^#(X)) 1046.89/297.03 , add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) 1046.89/297.03 , add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) 1046.89/297.03 , add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) 1046.89/297.03 , dbl^#(mark(X)) -> c_31(dbl^#(X)) 1046.89/297.03 , dbl^#(ok(X)) -> c_32(dbl^#(X)) 1046.89/297.03 , first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) 1046.89/297.03 , first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) 1046.89/297.03 , first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) 1046.89/297.03 , proper^#(terms(X)) -> c_36(terms^#(proper(X))) 1046.89/297.03 , proper^#(cons(X1, X2)) -> c_37(cons^#(proper(X1), proper(X2))) 1046.89/297.03 , proper^#(recip(X)) -> c_38(recip^#(proper(X))) 1046.89/297.03 , proper^#(sqr(X)) -> c_39(sqr^#(proper(X))) 1046.89/297.03 , proper^#(s(X)) -> c_40(s^#(proper(X))) 1046.89/297.03 , proper^#(0()) -> c_41() 1046.89/297.03 , proper^#(add(X1, X2)) -> c_42(add^#(proper(X1), proper(X2))) 1046.89/297.03 , proper^#(dbl(X)) -> c_43(dbl^#(proper(X))) 1046.89/297.03 , proper^#(first(X1, X2)) -> c_44(first^#(proper(X1), proper(X2))) 1046.89/297.03 , proper^#(nil()) -> c_45() 1046.89/297.03 , top^#(mark(X)) -> c_46(top^#(proper(X))) 1046.89/297.03 , top^#(ok(X)) -> c_47(top^#(active(X))) } 1046.89/297.03 1046.89/297.03 and mark the set of starting terms. 1046.89/297.03 1046.89/297.03 We are left with following problem, upon which TcT provides the 1046.89/297.03 certificate MAYBE. 1046.89/297.03 1046.89/297.03 Strict DPs: 1046.89/297.03 { active^#(terms(X)) -> c_1(terms^#(active(X))) 1046.89/297.03 , active^#(terms(N)) -> c_2(cons^#(recip(sqr(N)), terms(s(N)))) 1046.89/297.03 , active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1046.89/297.03 , active^#(recip(X)) -> c_4(recip^#(active(X))) 1046.89/297.03 , active^#(sqr(X)) -> c_5(sqr^#(active(X))) 1046.89/297.03 , active^#(sqr(s(X))) -> c_6(s^#(add(sqr(X), dbl(X)))) 1046.89/297.03 , active^#(sqr(0())) -> c_7() 1046.89/297.03 , active^#(add(X1, X2)) -> c_8(add^#(X1, active(X2))) 1046.89/297.03 , active^#(add(X1, X2)) -> c_9(add^#(active(X1), X2)) 1046.89/297.03 , active^#(add(s(X), Y)) -> c_10(s^#(add(X, Y))) 1046.89/297.03 , active^#(add(0(), X)) -> c_11(X) 1046.89/297.03 , active^#(dbl(X)) -> c_12(dbl^#(active(X))) 1046.89/297.03 , active^#(dbl(s(X))) -> c_13(s^#(s(dbl(X)))) 1046.89/297.03 , active^#(dbl(0())) -> c_14() 1046.89/297.03 , active^#(first(X1, X2)) -> c_15(first^#(X1, active(X2))) 1046.89/297.03 , active^#(first(X1, X2)) -> c_16(first^#(active(X1), X2)) 1046.89/297.03 , active^#(first(s(X), cons(Y, Z))) -> c_17(cons^#(Y, first(X, Z))) 1046.89/297.03 , active^#(first(0(), X)) -> c_18() 1046.89/297.03 , terms^#(mark(X)) -> c_19(terms^#(X)) 1046.89/297.03 , terms^#(ok(X)) -> c_20(terms^#(X)) 1046.89/297.03 , cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 1046.89/297.03 , cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 1046.89/297.03 , recip^#(mark(X)) -> c_23(recip^#(X)) 1046.89/297.03 , recip^#(ok(X)) -> c_24(recip^#(X)) 1046.89/297.03 , sqr^#(mark(X)) -> c_25(sqr^#(X)) 1046.89/297.03 , sqr^#(ok(X)) -> c_26(sqr^#(X)) 1046.89/297.03 , s^#(ok(X)) -> c_27(s^#(X)) 1046.89/297.03 , add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) 1046.89/297.04 , add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) 1046.89/297.04 , add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) 1046.89/297.04 , dbl^#(mark(X)) -> c_31(dbl^#(X)) 1046.89/297.04 , dbl^#(ok(X)) -> c_32(dbl^#(X)) 1046.89/297.04 , first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) 1046.89/297.04 , first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) 1046.89/297.04 , first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) 1046.89/297.04 , proper^#(terms(X)) -> c_36(terms^#(proper(X))) 1046.89/297.04 , proper^#(cons(X1, X2)) -> c_37(cons^#(proper(X1), proper(X2))) 1046.89/297.04 , proper^#(recip(X)) -> c_38(recip^#(proper(X))) 1046.89/297.04 , proper^#(sqr(X)) -> c_39(sqr^#(proper(X))) 1046.89/297.04 , proper^#(s(X)) -> c_40(s^#(proper(X))) 1046.89/297.04 , proper^#(0()) -> c_41() 1046.89/297.04 , proper^#(add(X1, X2)) -> c_42(add^#(proper(X1), proper(X2))) 1046.89/297.04 , proper^#(dbl(X)) -> c_43(dbl^#(proper(X))) 1046.89/297.04 , proper^#(first(X1, X2)) -> c_44(first^#(proper(X1), proper(X2))) 1046.89/297.04 , proper^#(nil()) -> c_45() 1046.89/297.04 , top^#(mark(X)) -> c_46(top^#(proper(X))) 1046.89/297.04 , top^#(ok(X)) -> c_47(top^#(active(X))) } 1046.89/297.04 Strict Trs: 1046.89/297.04 { active(terms(X)) -> terms(active(X)) 1046.89/297.04 , active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))) 1046.89/297.04 , active(cons(X1, X2)) -> cons(active(X1), X2) 1046.89/297.04 , active(recip(X)) -> recip(active(X)) 1046.89/297.04 , active(sqr(X)) -> sqr(active(X)) 1046.89/297.04 , active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))) 1046.89/297.04 , active(sqr(0())) -> mark(0()) 1046.89/297.04 , active(add(X1, X2)) -> add(X1, active(X2)) 1046.89/297.04 , active(add(X1, X2)) -> add(active(X1), X2) 1046.89/297.04 , active(add(s(X), Y)) -> mark(s(add(X, Y))) 1046.89/297.04 , active(add(0(), X)) -> mark(X) 1046.89/297.04 , active(dbl(X)) -> dbl(active(X)) 1046.89/297.04 , active(dbl(s(X))) -> mark(s(s(dbl(X)))) 1046.89/297.04 , active(dbl(0())) -> mark(0()) 1046.89/297.04 , active(first(X1, X2)) -> first(X1, active(X2)) 1046.89/297.04 , active(first(X1, X2)) -> first(active(X1), X2) 1046.89/297.04 , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) 1046.89/297.04 , active(first(0(), X)) -> mark(nil()) 1046.89/297.04 , terms(mark(X)) -> mark(terms(X)) 1046.89/297.04 , terms(ok(X)) -> ok(terms(X)) 1046.89/297.04 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1046.89/297.04 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1046.89/297.04 , recip(mark(X)) -> mark(recip(X)) 1046.89/297.04 , recip(ok(X)) -> ok(recip(X)) 1046.89/297.04 , sqr(mark(X)) -> mark(sqr(X)) 1046.89/297.04 , sqr(ok(X)) -> ok(sqr(X)) 1046.89/297.04 , s(ok(X)) -> ok(s(X)) 1046.89/297.04 , add(X1, mark(X2)) -> mark(add(X1, X2)) 1046.89/297.04 , add(mark(X1), X2) -> mark(add(X1, X2)) 1046.89/297.04 , add(ok(X1), ok(X2)) -> ok(add(X1, X2)) 1046.89/297.04 , dbl(mark(X)) -> mark(dbl(X)) 1046.89/297.04 , dbl(ok(X)) -> ok(dbl(X)) 1046.89/297.04 , first(X1, mark(X2)) -> mark(first(X1, X2)) 1046.89/297.04 , first(mark(X1), X2) -> mark(first(X1, X2)) 1046.89/297.04 , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) 1046.89/297.04 , proper(terms(X)) -> terms(proper(X)) 1046.89/297.04 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1046.89/297.04 , proper(recip(X)) -> recip(proper(X)) 1046.89/297.04 , proper(sqr(X)) -> sqr(proper(X)) 1046.89/297.04 , proper(s(X)) -> s(proper(X)) 1046.89/297.04 , proper(0()) -> ok(0()) 1046.89/297.04 , proper(add(X1, X2)) -> add(proper(X1), proper(X2)) 1046.89/297.04 , proper(dbl(X)) -> dbl(proper(X)) 1046.89/297.04 , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) 1046.89/297.04 , proper(nil()) -> ok(nil()) 1046.89/297.04 , top(mark(X)) -> top(proper(X)) 1046.89/297.04 , top(ok(X)) -> top(active(X)) } 1046.89/297.04 Obligation: 1046.89/297.04 runtime complexity 1046.89/297.04 Answer: 1046.89/297.04 MAYBE 1046.89/297.04 1046.89/297.04 Consider the dependency graph: 1046.89/297.04 1046.89/297.04 1: active^#(terms(X)) -> c_1(terms^#(active(X))) 1046.89/297.04 -->_1 terms^#(ok(X)) -> c_20(terms^#(X)) :20 1046.89/297.04 -->_1 terms^#(mark(X)) -> c_19(terms^#(X)) :19 1046.89/297.04 1046.89/297.04 2: active^#(terms(N)) -> c_2(cons^#(recip(sqr(N)), terms(s(N)))) 1046.89/297.04 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 1046.89/297.04 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 1046.89/297.04 1046.89/297.04 3: active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1046.89/297.04 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 1046.89/297.04 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 1046.89/297.04 1046.89/297.04 4: active^#(recip(X)) -> c_4(recip^#(active(X))) 1046.89/297.04 -->_1 recip^#(ok(X)) -> c_24(recip^#(X)) :24 1046.89/297.04 -->_1 recip^#(mark(X)) -> c_23(recip^#(X)) :23 1046.89/297.04 1046.89/297.04 5: active^#(sqr(X)) -> c_5(sqr^#(active(X))) 1046.89/297.04 -->_1 sqr^#(ok(X)) -> c_26(sqr^#(X)) :26 1046.89/297.04 -->_1 sqr^#(mark(X)) -> c_25(sqr^#(X)) :25 1046.89/297.04 1046.89/297.04 6: active^#(sqr(s(X))) -> c_6(s^#(add(sqr(X), dbl(X)))) 1046.89/297.04 -->_1 s^#(ok(X)) -> c_27(s^#(X)) :27 1046.89/297.04 1046.89/297.04 7: active^#(sqr(0())) -> c_7() 1046.89/297.04 1046.89/297.04 8: active^#(add(X1, X2)) -> c_8(add^#(X1, active(X2))) 1046.89/297.04 -->_1 add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) :30 1046.89/297.04 -->_1 add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) :29 1046.89/297.04 -->_1 add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) :28 1046.89/297.04 1046.89/297.04 9: active^#(add(X1, X2)) -> c_9(add^#(active(X1), X2)) 1046.89/297.04 -->_1 add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) :30 1046.89/297.04 -->_1 add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) :29 1046.89/297.04 -->_1 add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) :28 1046.89/297.04 1046.89/297.04 10: active^#(add(s(X), Y)) -> c_10(s^#(add(X, Y))) 1046.89/297.04 -->_1 s^#(ok(X)) -> c_27(s^#(X)) :27 1046.89/297.04 1046.89/297.04 11: active^#(add(0(), X)) -> c_11(X) 1046.89/297.04 -->_1 top^#(ok(X)) -> c_47(top^#(active(X))) :47 1046.89/297.04 -->_1 top^#(mark(X)) -> c_46(top^#(proper(X))) :46 1046.89/297.04 -->_1 proper^#(first(X1, X2)) -> 1046.89/297.04 c_44(first^#(proper(X1), proper(X2))) :44 1046.89/297.04 -->_1 proper^#(dbl(X)) -> c_43(dbl^#(proper(X))) :43 1046.89/297.04 -->_1 proper^#(add(X1, X2)) -> 1046.89/297.04 c_42(add^#(proper(X1), proper(X2))) :42 1046.89/297.04 -->_1 proper^#(s(X)) -> c_40(s^#(proper(X))) :40 1046.89/297.04 -->_1 proper^#(sqr(X)) -> c_39(sqr^#(proper(X))) :39 1046.89/297.04 -->_1 proper^#(recip(X)) -> c_38(recip^#(proper(X))) :38 1046.89/297.04 -->_1 proper^#(cons(X1, X2)) -> 1046.89/297.04 c_37(cons^#(proper(X1), proper(X2))) :37 1046.89/297.04 -->_1 proper^#(terms(X)) -> c_36(terms^#(proper(X))) :36 1046.89/297.04 -->_1 first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) :35 1046.89/297.04 -->_1 first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) :34 1046.89/297.04 -->_1 first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) :33 1046.89/297.04 -->_1 dbl^#(ok(X)) -> c_32(dbl^#(X)) :32 1046.89/297.04 -->_1 dbl^#(mark(X)) -> c_31(dbl^#(X)) :31 1046.89/297.04 -->_1 add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) :30 1046.89/297.04 -->_1 add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) :29 1046.89/297.04 -->_1 add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) :28 1046.89/297.04 -->_1 s^#(ok(X)) -> c_27(s^#(X)) :27 1046.89/297.04 -->_1 sqr^#(ok(X)) -> c_26(sqr^#(X)) :26 1046.89/297.04 -->_1 sqr^#(mark(X)) -> c_25(sqr^#(X)) :25 1046.89/297.04 -->_1 recip^#(ok(X)) -> c_24(recip^#(X)) :24 1046.89/297.04 -->_1 recip^#(mark(X)) -> c_23(recip^#(X)) :23 1046.89/297.04 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 1046.89/297.04 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 1046.89/297.04 -->_1 terms^#(ok(X)) -> c_20(terms^#(X)) :20 1046.89/297.04 -->_1 terms^#(mark(X)) -> c_19(terms^#(X)) :19 1046.89/297.04 -->_1 active^#(first(s(X), cons(Y, Z))) -> 1046.89/297.04 c_17(cons^#(Y, first(X, Z))) :17 1046.89/297.04 -->_1 active^#(first(X1, X2)) -> c_16(first^#(active(X1), X2)) :16 1046.89/297.04 -->_1 active^#(first(X1, X2)) -> c_15(first^#(X1, active(X2))) :15 1046.89/297.04 -->_1 active^#(dbl(s(X))) -> c_13(s^#(s(dbl(X)))) :13 1046.89/297.04 -->_1 active^#(dbl(X)) -> c_12(dbl^#(active(X))) :12 1046.89/297.04 -->_1 proper^#(nil()) -> c_45() :45 1046.89/297.04 -->_1 proper^#(0()) -> c_41() :41 1046.89/297.04 -->_1 active^#(first(0(), X)) -> c_18() :18 1046.89/297.04 -->_1 active^#(dbl(0())) -> c_14() :14 1046.89/297.04 -->_1 active^#(add(0(), X)) -> c_11(X) :11 1046.89/297.04 -->_1 active^#(add(s(X), Y)) -> c_10(s^#(add(X, Y))) :10 1046.89/297.04 -->_1 active^#(add(X1, X2)) -> c_9(add^#(active(X1), X2)) :9 1046.89/297.04 -->_1 active^#(add(X1, X2)) -> c_8(add^#(X1, active(X2))) :8 1046.89/297.04 -->_1 active^#(sqr(0())) -> c_7() :7 1046.89/297.04 -->_1 active^#(sqr(s(X))) -> c_6(s^#(add(sqr(X), dbl(X)))) :6 1046.89/297.04 -->_1 active^#(sqr(X)) -> c_5(sqr^#(active(X))) :5 1046.89/297.04 -->_1 active^#(recip(X)) -> c_4(recip^#(active(X))) :4 1046.89/297.04 -->_1 active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) :3 1046.89/297.04 -->_1 active^#(terms(N)) -> 1046.89/297.04 c_2(cons^#(recip(sqr(N)), terms(s(N)))) :2 1046.89/297.04 -->_1 active^#(terms(X)) -> c_1(terms^#(active(X))) :1 1046.89/297.04 1046.89/297.04 12: active^#(dbl(X)) -> c_12(dbl^#(active(X))) 1046.89/297.04 -->_1 dbl^#(ok(X)) -> c_32(dbl^#(X)) :32 1046.89/297.04 -->_1 dbl^#(mark(X)) -> c_31(dbl^#(X)) :31 1046.89/297.04 1046.89/297.04 13: active^#(dbl(s(X))) -> c_13(s^#(s(dbl(X)))) 1046.89/297.04 -->_1 s^#(ok(X)) -> c_27(s^#(X)) :27 1046.89/297.04 1046.89/297.04 14: active^#(dbl(0())) -> c_14() 1046.89/297.04 1046.89/297.04 15: active^#(first(X1, X2)) -> c_15(first^#(X1, active(X2))) 1046.89/297.04 -->_1 first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) :35 1046.89/297.04 -->_1 first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) :34 1046.89/297.04 -->_1 first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) :33 1046.89/297.04 1046.89/297.04 16: active^#(first(X1, X2)) -> c_16(first^#(active(X1), X2)) 1046.89/297.04 -->_1 first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) :35 1046.89/297.04 -->_1 first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) :34 1046.89/297.04 -->_1 first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) :33 1046.89/297.04 1046.89/297.04 17: active^#(first(s(X), cons(Y, Z))) -> 1046.89/297.04 c_17(cons^#(Y, first(X, Z))) 1046.89/297.04 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 1046.89/297.04 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 1046.89/297.04 1046.89/297.04 18: active^#(first(0(), X)) -> c_18() 1046.89/297.04 1046.89/297.04 19: terms^#(mark(X)) -> c_19(terms^#(X)) 1046.89/297.04 -->_1 terms^#(ok(X)) -> c_20(terms^#(X)) :20 1046.89/297.04 -->_1 terms^#(mark(X)) -> c_19(terms^#(X)) :19 1046.89/297.04 1046.89/297.04 20: terms^#(ok(X)) -> c_20(terms^#(X)) 1046.89/297.04 -->_1 terms^#(ok(X)) -> c_20(terms^#(X)) :20 1046.89/297.04 -->_1 terms^#(mark(X)) -> c_19(terms^#(X)) :19 1046.89/297.04 1046.89/297.04 21: cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 1046.89/297.04 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 1046.89/297.04 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 1046.89/297.04 1046.89/297.04 22: cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 1046.89/297.04 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 1046.89/297.04 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 1046.89/297.04 1046.89/297.04 23: recip^#(mark(X)) -> c_23(recip^#(X)) 1046.89/297.04 -->_1 recip^#(ok(X)) -> c_24(recip^#(X)) :24 1046.89/297.04 -->_1 recip^#(mark(X)) -> c_23(recip^#(X)) :23 1046.89/297.04 1046.89/297.04 24: recip^#(ok(X)) -> c_24(recip^#(X)) 1046.89/297.04 -->_1 recip^#(ok(X)) -> c_24(recip^#(X)) :24 1046.89/297.04 -->_1 recip^#(mark(X)) -> c_23(recip^#(X)) :23 1046.89/297.04 1046.89/297.04 25: sqr^#(mark(X)) -> c_25(sqr^#(X)) 1046.89/297.04 -->_1 sqr^#(ok(X)) -> c_26(sqr^#(X)) :26 1046.89/297.04 -->_1 sqr^#(mark(X)) -> c_25(sqr^#(X)) :25 1046.89/297.04 1046.89/297.04 26: sqr^#(ok(X)) -> c_26(sqr^#(X)) 1046.89/297.04 -->_1 sqr^#(ok(X)) -> c_26(sqr^#(X)) :26 1046.89/297.04 -->_1 sqr^#(mark(X)) -> c_25(sqr^#(X)) :25 1046.89/297.04 1046.89/297.04 27: s^#(ok(X)) -> c_27(s^#(X)) -->_1 s^#(ok(X)) -> c_27(s^#(X)) :27 1046.89/297.04 1046.89/297.04 28: add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) 1046.89/297.04 -->_1 add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) :30 1046.89/297.04 -->_1 add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) :29 1046.89/297.04 -->_1 add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) :28 1046.89/297.04 1046.89/297.04 29: add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) 1046.89/297.04 -->_1 add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) :30 1046.89/297.04 -->_1 add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) :29 1046.89/297.04 -->_1 add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) :28 1046.89/297.04 1046.89/297.04 30: add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) 1046.89/297.04 -->_1 add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) :30 1046.89/297.04 -->_1 add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) :29 1046.89/297.04 -->_1 add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) :28 1046.89/297.04 1046.89/297.04 31: dbl^#(mark(X)) -> c_31(dbl^#(X)) 1046.89/297.04 -->_1 dbl^#(ok(X)) -> c_32(dbl^#(X)) :32 1046.89/297.04 -->_1 dbl^#(mark(X)) -> c_31(dbl^#(X)) :31 1046.89/297.04 1046.89/297.04 32: dbl^#(ok(X)) -> c_32(dbl^#(X)) 1046.89/297.04 -->_1 dbl^#(ok(X)) -> c_32(dbl^#(X)) :32 1046.89/297.04 -->_1 dbl^#(mark(X)) -> c_31(dbl^#(X)) :31 1046.89/297.04 1046.89/297.04 33: first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) 1046.89/297.04 -->_1 first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) :35 1046.89/297.04 -->_1 first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) :34 1046.89/297.04 -->_1 first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) :33 1046.89/297.04 1046.89/297.04 34: first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) 1046.89/297.04 -->_1 first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) :35 1046.89/297.04 -->_1 first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) :34 1046.89/297.04 -->_1 first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) :33 1046.89/297.04 1046.89/297.04 35: first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) 1046.89/297.04 -->_1 first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) :35 1046.89/297.04 -->_1 first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) :34 1046.89/297.04 -->_1 first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) :33 1046.89/297.04 1046.89/297.04 36: proper^#(terms(X)) -> c_36(terms^#(proper(X))) 1046.89/297.04 -->_1 terms^#(ok(X)) -> c_20(terms^#(X)) :20 1046.89/297.04 -->_1 terms^#(mark(X)) -> c_19(terms^#(X)) :19 1046.89/297.04 1046.89/297.04 37: proper^#(cons(X1, X2)) -> c_37(cons^#(proper(X1), proper(X2))) 1046.89/297.04 -->_1 cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) :22 1046.89/297.04 -->_1 cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) :21 1046.89/297.04 1046.89/297.04 38: proper^#(recip(X)) -> c_38(recip^#(proper(X))) 1046.89/297.04 -->_1 recip^#(ok(X)) -> c_24(recip^#(X)) :24 1046.89/297.04 -->_1 recip^#(mark(X)) -> c_23(recip^#(X)) :23 1046.89/297.04 1046.89/297.04 39: proper^#(sqr(X)) -> c_39(sqr^#(proper(X))) 1046.89/297.04 -->_1 sqr^#(ok(X)) -> c_26(sqr^#(X)) :26 1046.89/297.04 -->_1 sqr^#(mark(X)) -> c_25(sqr^#(X)) :25 1046.89/297.04 1046.89/297.04 40: proper^#(s(X)) -> c_40(s^#(proper(X))) 1046.89/297.04 -->_1 s^#(ok(X)) -> c_27(s^#(X)) :27 1046.89/297.04 1046.89/297.04 41: proper^#(0()) -> c_41() 1046.89/297.04 1046.89/297.04 42: proper^#(add(X1, X2)) -> c_42(add^#(proper(X1), proper(X2))) 1046.89/297.04 -->_1 add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) :30 1046.89/297.04 -->_1 add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) :29 1046.89/297.04 -->_1 add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) :28 1046.89/297.04 1046.89/297.04 43: proper^#(dbl(X)) -> c_43(dbl^#(proper(X))) 1046.89/297.04 -->_1 dbl^#(ok(X)) -> c_32(dbl^#(X)) :32 1046.89/297.04 -->_1 dbl^#(mark(X)) -> c_31(dbl^#(X)) :31 1046.89/297.04 1046.89/297.04 44: proper^#(first(X1, X2)) -> 1046.89/297.04 c_44(first^#(proper(X1), proper(X2))) 1046.89/297.04 -->_1 first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) :35 1046.89/297.04 -->_1 first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) :34 1046.89/297.04 -->_1 first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) :33 1046.89/297.04 1046.89/297.04 45: proper^#(nil()) -> c_45() 1046.89/297.04 1046.89/297.04 46: top^#(mark(X)) -> c_46(top^#(proper(X))) 1046.89/297.04 -->_1 top^#(ok(X)) -> c_47(top^#(active(X))) :47 1046.89/297.04 -->_1 top^#(mark(X)) -> c_46(top^#(proper(X))) :46 1046.89/297.04 1046.89/297.04 47: top^#(ok(X)) -> c_47(top^#(active(X))) 1046.89/297.04 -->_1 top^#(ok(X)) -> c_47(top^#(active(X))) :47 1046.89/297.04 -->_1 top^#(mark(X)) -> c_46(top^#(proper(X))) :46 1046.89/297.04 1046.89/297.04 1046.89/297.04 Only the nodes 1046.89/297.04 {19,20,21,22,23,24,25,26,27,28,30,29,31,32,33,35,34,41,45,46,47} 1046.89/297.04 are reachable from nodes 1046.89/297.04 {19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,41,45,46,47} 1046.89/297.04 that start derivation from marked basic terms. The nodes not 1046.89/297.04 reachable are removed from the problem. 1046.89/297.04 1046.89/297.04 We are left with following problem, upon which TcT provides the 1046.89/297.04 certificate MAYBE. 1046.89/297.04 1046.89/297.04 Strict DPs: 1046.89/297.04 { terms^#(mark(X)) -> c_19(terms^#(X)) 1046.89/297.04 , terms^#(ok(X)) -> c_20(terms^#(X)) 1046.89/297.04 , cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 1046.89/297.04 , cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 1046.89/297.04 , recip^#(mark(X)) -> c_23(recip^#(X)) 1046.89/297.04 , recip^#(ok(X)) -> c_24(recip^#(X)) 1046.89/297.04 , sqr^#(mark(X)) -> c_25(sqr^#(X)) 1046.89/297.04 , sqr^#(ok(X)) -> c_26(sqr^#(X)) 1046.89/297.04 , s^#(ok(X)) -> c_27(s^#(X)) 1046.89/297.04 , add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) 1046.89/297.04 , add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) 1046.89/297.04 , add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) 1046.89/297.04 , dbl^#(mark(X)) -> c_31(dbl^#(X)) 1046.89/297.04 , dbl^#(ok(X)) -> c_32(dbl^#(X)) 1046.89/297.04 , first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) 1046.89/297.04 , first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) 1046.89/297.04 , first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) 1046.89/297.04 , proper^#(0()) -> c_41() 1046.89/297.04 , proper^#(nil()) -> c_45() 1046.89/297.04 , top^#(mark(X)) -> c_46(top^#(proper(X))) 1046.89/297.04 , top^#(ok(X)) -> c_47(top^#(active(X))) } 1046.89/297.04 Strict Trs: 1046.89/297.04 { active(terms(X)) -> terms(active(X)) 1046.89/297.04 , active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))) 1046.89/297.04 , active(cons(X1, X2)) -> cons(active(X1), X2) 1046.89/297.04 , active(recip(X)) -> recip(active(X)) 1046.89/297.04 , active(sqr(X)) -> sqr(active(X)) 1046.89/297.04 , active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))) 1046.89/297.04 , active(sqr(0())) -> mark(0()) 1046.89/297.04 , active(add(X1, X2)) -> add(X1, active(X2)) 1046.89/297.04 , active(add(X1, X2)) -> add(active(X1), X2) 1046.89/297.04 , active(add(s(X), Y)) -> mark(s(add(X, Y))) 1046.89/297.04 , active(add(0(), X)) -> mark(X) 1046.89/297.04 , active(dbl(X)) -> dbl(active(X)) 1046.89/297.04 , active(dbl(s(X))) -> mark(s(s(dbl(X)))) 1046.89/297.04 , active(dbl(0())) -> mark(0()) 1046.89/297.04 , active(first(X1, X2)) -> first(X1, active(X2)) 1046.89/297.04 , active(first(X1, X2)) -> first(active(X1), X2) 1046.89/297.05 , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) 1046.89/297.05 , active(first(0(), X)) -> mark(nil()) 1046.89/297.05 , terms(mark(X)) -> mark(terms(X)) 1046.89/297.05 , terms(ok(X)) -> ok(terms(X)) 1046.89/297.05 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1046.89/297.05 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1046.89/297.05 , recip(mark(X)) -> mark(recip(X)) 1046.89/297.05 , recip(ok(X)) -> ok(recip(X)) 1046.89/297.05 , sqr(mark(X)) -> mark(sqr(X)) 1046.89/297.05 , sqr(ok(X)) -> ok(sqr(X)) 1046.89/297.05 , s(ok(X)) -> ok(s(X)) 1046.89/297.05 , add(X1, mark(X2)) -> mark(add(X1, X2)) 1046.89/297.05 , add(mark(X1), X2) -> mark(add(X1, X2)) 1046.89/297.05 , add(ok(X1), ok(X2)) -> ok(add(X1, X2)) 1046.89/297.05 , dbl(mark(X)) -> mark(dbl(X)) 1046.89/297.05 , dbl(ok(X)) -> ok(dbl(X)) 1046.89/297.05 , first(X1, mark(X2)) -> mark(first(X1, X2)) 1046.89/297.05 , first(mark(X1), X2) -> mark(first(X1, X2)) 1046.89/297.05 , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) 1046.89/297.05 , proper(terms(X)) -> terms(proper(X)) 1046.89/297.05 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1046.89/297.05 , proper(recip(X)) -> recip(proper(X)) 1046.89/297.05 , proper(sqr(X)) -> sqr(proper(X)) 1046.89/297.05 , proper(s(X)) -> s(proper(X)) 1046.89/297.05 , proper(0()) -> ok(0()) 1046.89/297.05 , proper(add(X1, X2)) -> add(proper(X1), proper(X2)) 1046.89/297.05 , proper(dbl(X)) -> dbl(proper(X)) 1046.89/297.05 , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) 1046.89/297.05 , proper(nil()) -> ok(nil()) 1046.89/297.05 , top(mark(X)) -> top(proper(X)) 1046.89/297.05 , top(ok(X)) -> top(active(X)) } 1046.89/297.05 Obligation: 1046.89/297.05 runtime complexity 1046.89/297.05 Answer: 1046.89/297.05 MAYBE 1046.89/297.05 1046.89/297.05 We estimate the number of application of {18,19} by applications of 1046.89/297.05 Pre({18,19}) = {}. Here rules are labeled as follows: 1046.89/297.05 1046.89/297.05 DPs: 1046.89/297.05 { 1: terms^#(mark(X)) -> c_19(terms^#(X)) 1046.89/297.05 , 2: terms^#(ok(X)) -> c_20(terms^#(X)) 1046.89/297.05 , 3: cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 1046.89/297.05 , 4: cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 1046.89/297.05 , 5: recip^#(mark(X)) -> c_23(recip^#(X)) 1046.89/297.05 , 6: recip^#(ok(X)) -> c_24(recip^#(X)) 1046.89/297.05 , 7: sqr^#(mark(X)) -> c_25(sqr^#(X)) 1046.89/297.05 , 8: sqr^#(ok(X)) -> c_26(sqr^#(X)) 1046.89/297.05 , 9: s^#(ok(X)) -> c_27(s^#(X)) 1046.89/297.05 , 10: add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) 1046.89/297.05 , 11: add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) 1046.89/297.05 , 12: add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) 1046.89/297.05 , 13: dbl^#(mark(X)) -> c_31(dbl^#(X)) 1046.89/297.05 , 14: dbl^#(ok(X)) -> c_32(dbl^#(X)) 1046.89/297.05 , 15: first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) 1046.89/297.05 , 16: first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) 1046.89/297.05 , 17: first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) 1046.89/297.05 , 18: proper^#(0()) -> c_41() 1046.89/297.05 , 19: proper^#(nil()) -> c_45() 1046.89/297.05 , 20: top^#(mark(X)) -> c_46(top^#(proper(X))) 1046.89/297.05 , 21: top^#(ok(X)) -> c_47(top^#(active(X))) } 1046.89/297.05 1046.89/297.05 We are left with following problem, upon which TcT provides the 1046.89/297.05 certificate MAYBE. 1046.89/297.05 1046.89/297.05 Strict DPs: 1046.89/297.05 { terms^#(mark(X)) -> c_19(terms^#(X)) 1046.89/297.05 , terms^#(ok(X)) -> c_20(terms^#(X)) 1046.89/297.05 , cons^#(mark(X1), X2) -> c_21(cons^#(X1, X2)) 1046.89/297.05 , cons^#(ok(X1), ok(X2)) -> c_22(cons^#(X1, X2)) 1046.89/297.05 , recip^#(mark(X)) -> c_23(recip^#(X)) 1046.89/297.05 , recip^#(ok(X)) -> c_24(recip^#(X)) 1046.89/297.05 , sqr^#(mark(X)) -> c_25(sqr^#(X)) 1046.89/297.05 , sqr^#(ok(X)) -> c_26(sqr^#(X)) 1046.89/297.05 , s^#(ok(X)) -> c_27(s^#(X)) 1046.89/297.05 , add^#(X1, mark(X2)) -> c_28(add^#(X1, X2)) 1046.89/297.05 , add^#(mark(X1), X2) -> c_29(add^#(X1, X2)) 1046.89/297.05 , add^#(ok(X1), ok(X2)) -> c_30(add^#(X1, X2)) 1046.89/297.05 , dbl^#(mark(X)) -> c_31(dbl^#(X)) 1046.89/297.05 , dbl^#(ok(X)) -> c_32(dbl^#(X)) 1046.89/297.05 , first^#(X1, mark(X2)) -> c_33(first^#(X1, X2)) 1046.89/297.05 , first^#(mark(X1), X2) -> c_34(first^#(X1, X2)) 1046.89/297.05 , first^#(ok(X1), ok(X2)) -> c_35(first^#(X1, X2)) 1046.89/297.05 , top^#(mark(X)) -> c_46(top^#(proper(X))) 1046.89/297.05 , top^#(ok(X)) -> c_47(top^#(active(X))) } 1046.89/297.05 Strict Trs: 1046.89/297.05 { active(terms(X)) -> terms(active(X)) 1046.89/297.05 , active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))) 1046.89/297.05 , active(cons(X1, X2)) -> cons(active(X1), X2) 1046.89/297.05 , active(recip(X)) -> recip(active(X)) 1046.89/297.05 , active(sqr(X)) -> sqr(active(X)) 1046.89/297.05 , active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))) 1046.89/297.05 , active(sqr(0())) -> mark(0()) 1046.89/297.05 , active(add(X1, X2)) -> add(X1, active(X2)) 1046.89/297.05 , active(add(X1, X2)) -> add(active(X1), X2) 1046.89/297.05 , active(add(s(X), Y)) -> mark(s(add(X, Y))) 1046.89/297.05 , active(add(0(), X)) -> mark(X) 1046.89/297.05 , active(dbl(X)) -> dbl(active(X)) 1046.89/297.05 , active(dbl(s(X))) -> mark(s(s(dbl(X)))) 1046.89/297.05 , active(dbl(0())) -> mark(0()) 1046.89/297.05 , active(first(X1, X2)) -> first(X1, active(X2)) 1046.89/297.05 , active(first(X1, X2)) -> first(active(X1), X2) 1046.89/297.05 , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) 1046.89/297.05 , active(first(0(), X)) -> mark(nil()) 1046.89/297.05 , terms(mark(X)) -> mark(terms(X)) 1046.89/297.05 , terms(ok(X)) -> ok(terms(X)) 1046.89/297.05 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1046.89/297.05 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1046.89/297.05 , recip(mark(X)) -> mark(recip(X)) 1046.89/297.05 , recip(ok(X)) -> ok(recip(X)) 1046.89/297.05 , sqr(mark(X)) -> mark(sqr(X)) 1046.89/297.05 , sqr(ok(X)) -> ok(sqr(X)) 1046.89/297.05 , s(ok(X)) -> ok(s(X)) 1046.89/297.05 , add(X1, mark(X2)) -> mark(add(X1, X2)) 1046.89/297.05 , add(mark(X1), X2) -> mark(add(X1, X2)) 1046.89/297.05 , add(ok(X1), ok(X2)) -> ok(add(X1, X2)) 1046.89/297.05 , dbl(mark(X)) -> mark(dbl(X)) 1046.89/297.05 , dbl(ok(X)) -> ok(dbl(X)) 1046.89/297.05 , first(X1, mark(X2)) -> mark(first(X1, X2)) 1046.89/297.05 , first(mark(X1), X2) -> mark(first(X1, X2)) 1046.89/297.05 , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) 1046.89/297.05 , proper(terms(X)) -> terms(proper(X)) 1046.89/297.05 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1046.89/297.05 , proper(recip(X)) -> recip(proper(X)) 1046.89/297.05 , proper(sqr(X)) -> sqr(proper(X)) 1046.89/297.05 , proper(s(X)) -> s(proper(X)) 1046.89/297.05 , proper(0()) -> ok(0()) 1046.89/297.05 , proper(add(X1, X2)) -> add(proper(X1), proper(X2)) 1046.89/297.05 , proper(dbl(X)) -> dbl(proper(X)) 1046.89/297.05 , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) 1046.89/297.05 , proper(nil()) -> ok(nil()) 1046.89/297.05 , top(mark(X)) -> top(proper(X)) 1046.89/297.05 , top(ok(X)) -> top(active(X)) } 1046.89/297.05 Weak DPs: 1046.89/297.05 { proper^#(0()) -> c_41() 1046.89/297.05 , proper^#(nil()) -> c_45() } 1046.89/297.05 Obligation: 1046.89/297.05 runtime complexity 1046.89/297.05 Answer: 1046.89/297.05 MAYBE 1046.89/297.05 1046.89/297.05 Empty strict component of the problem is NOT empty. 1046.89/297.05 1046.89/297.05 1046.89/297.05 Arrrr.. 1047.24/297.34 EOF