MAYBE 1059.17/297.15 MAYBE 1059.17/297.15 1059.17/297.15 We are left with following problem, upon which TcT provides the 1059.17/297.15 certificate MAYBE. 1059.17/297.15 1059.17/297.15 Strict Trs: 1059.17/297.15 { active(from(X)) -> from(active(X)) 1059.17/297.15 , active(from(X)) -> mark(cons(X, from(s(X)))) 1059.17/297.15 , active(cons(X1, X2)) -> cons(active(X1), X2) 1059.17/297.15 , active(s(X)) -> s(active(X)) 1059.17/297.15 , active(sel(X1, X2)) -> sel(X1, active(X2)) 1059.17/297.15 , active(sel(X1, X2)) -> sel(active(X1), X2) 1059.17/297.15 , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)) 1059.17/297.15 , active(sel(0(), cons(X, Y))) -> mark(X) 1059.17/297.15 , from(mark(X)) -> mark(from(X)) 1059.17/297.15 , from(ok(X)) -> ok(from(X)) 1059.17/297.15 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1059.17/297.15 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1059.17/297.15 , s(mark(X)) -> mark(s(X)) 1059.17/297.15 , s(ok(X)) -> ok(s(X)) 1059.17/297.15 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 1059.17/297.15 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 1059.17/297.15 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 1059.17/297.15 , proper(from(X)) -> from(proper(X)) 1059.17/297.15 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1059.17/297.15 , proper(s(X)) -> s(proper(X)) 1059.17/297.15 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 1059.17/297.15 , proper(0()) -> ok(0()) 1059.17/297.15 , top(mark(X)) -> top(proper(X)) 1059.17/297.15 , top(ok(X)) -> top(active(X)) } 1059.17/297.15 Obligation: 1059.17/297.15 runtime complexity 1059.17/297.15 Answer: 1059.17/297.15 MAYBE 1059.17/297.15 1059.17/297.15 None of the processors succeeded. 1059.17/297.15 1059.17/297.15 Details of failed attempt(s): 1059.17/297.15 ----------------------------- 1059.17/297.15 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1059.17/297.15 following reason: 1059.17/297.15 1059.17/297.15 Computation stopped due to timeout after 297.0 seconds. 1059.17/297.15 1059.17/297.15 2) 'Best' failed due to the following reason: 1059.17/297.15 1059.17/297.15 None of the processors succeeded. 1059.17/297.15 1059.17/297.15 Details of failed attempt(s): 1059.17/297.15 ----------------------------- 1059.17/297.15 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1059.17/297.15 seconds)' failed due to the following reason: 1059.17/297.15 1059.17/297.15 Computation stopped due to timeout after 148.0 seconds. 1059.17/297.15 1059.17/297.15 2) 'Best' failed due to the following reason: 1059.17/297.15 1059.17/297.15 None of the processors succeeded. 1059.17/297.15 1059.17/297.15 Details of failed attempt(s): 1059.17/297.15 ----------------------------- 1059.17/297.15 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1059.17/297.15 to the following reason: 1059.17/297.15 1059.17/297.15 The processor is inapplicable, reason: 1059.17/297.15 Processor only applicable for innermost runtime complexity analysis 1059.17/297.15 1059.17/297.15 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1059.17/297.15 following reason: 1059.17/297.15 1059.17/297.15 The processor is inapplicable, reason: 1059.17/297.15 Processor only applicable for innermost runtime complexity analysis 1059.17/297.15 1059.17/297.15 1059.17/297.15 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1059.17/297.15 failed due to the following reason: 1059.17/297.15 1059.17/297.15 None of the processors succeeded. 1059.17/297.15 1059.17/297.15 Details of failed attempt(s): 1059.17/297.15 ----------------------------- 1059.17/297.15 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1059.17/297.15 failed due to the following reason: 1059.17/297.15 1059.17/297.15 match-boundness of the problem could not be verified. 1059.17/297.15 1059.17/297.15 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1059.17/297.15 failed due to the following reason: 1059.17/297.15 1059.17/297.15 match-boundness of the problem could not be verified. 1059.17/297.15 1059.17/297.15 1059.17/297.15 1059.17/297.15 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1059.17/297.15 the following reason: 1059.17/297.15 1059.17/297.15 We add the following weak dependency pairs: 1059.17/297.15 1059.17/297.15 Strict DPs: 1059.17/297.15 { active^#(from(X)) -> c_1(from^#(active(X))) 1059.17/297.15 , active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) 1059.17/297.15 , active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1059.17/297.15 , active^#(s(X)) -> c_4(s^#(active(X))) 1059.17/297.15 , active^#(sel(X1, X2)) -> c_5(sel^#(X1, active(X2))) 1059.17/297.15 , active^#(sel(X1, X2)) -> c_6(sel^#(active(X1), X2)) 1059.17/297.15 , active^#(sel(s(X), cons(Y, Z))) -> c_7(sel^#(X, Z)) 1059.17/297.15 , active^#(sel(0(), cons(X, Y))) -> c_8(X) 1059.17/297.15 , from^#(mark(X)) -> c_9(from^#(X)) 1059.17/297.15 , from^#(ok(X)) -> c_10(from^#(X)) 1059.17/297.15 , cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) 1059.17/297.15 , cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) 1059.17/297.15 , s^#(mark(X)) -> c_13(s^#(X)) 1059.17/297.15 , s^#(ok(X)) -> c_14(s^#(X)) 1059.17/297.15 , sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) 1059.17/297.15 , sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) 1059.17/297.15 , sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) 1059.17/297.15 , proper^#(from(X)) -> c_18(from^#(proper(X))) 1059.17/297.15 , proper^#(cons(X1, X2)) -> c_19(cons^#(proper(X1), proper(X2))) 1059.17/297.15 , proper^#(s(X)) -> c_20(s^#(proper(X))) 1059.17/297.15 , proper^#(sel(X1, X2)) -> c_21(sel^#(proper(X1), proper(X2))) 1059.17/297.15 , proper^#(0()) -> c_22() 1059.17/297.15 , top^#(mark(X)) -> c_23(top^#(proper(X))) 1059.17/297.15 , top^#(ok(X)) -> c_24(top^#(active(X))) } 1059.17/297.15 1059.17/297.15 and mark the set of starting terms. 1059.17/297.15 1059.17/297.15 We are left with following problem, upon which TcT provides the 1059.17/297.15 certificate MAYBE. 1059.17/297.15 1059.17/297.15 Strict DPs: 1059.17/297.15 { active^#(from(X)) -> c_1(from^#(active(X))) 1059.17/297.15 , active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) 1059.17/297.15 , active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1059.17/297.15 , active^#(s(X)) -> c_4(s^#(active(X))) 1059.17/297.15 , active^#(sel(X1, X2)) -> c_5(sel^#(X1, active(X2))) 1059.17/297.15 , active^#(sel(X1, X2)) -> c_6(sel^#(active(X1), X2)) 1059.17/297.15 , active^#(sel(s(X), cons(Y, Z))) -> c_7(sel^#(X, Z)) 1059.17/297.15 , active^#(sel(0(), cons(X, Y))) -> c_8(X) 1059.17/297.15 , from^#(mark(X)) -> c_9(from^#(X)) 1059.17/297.15 , from^#(ok(X)) -> c_10(from^#(X)) 1059.17/297.15 , cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) 1059.17/297.15 , cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) 1059.17/297.15 , s^#(mark(X)) -> c_13(s^#(X)) 1059.17/297.15 , s^#(ok(X)) -> c_14(s^#(X)) 1059.17/297.15 , sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) 1059.17/297.15 , sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) 1059.17/297.15 , sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) 1059.17/297.15 , proper^#(from(X)) -> c_18(from^#(proper(X))) 1059.17/297.15 , proper^#(cons(X1, X2)) -> c_19(cons^#(proper(X1), proper(X2))) 1059.17/297.15 , proper^#(s(X)) -> c_20(s^#(proper(X))) 1059.17/297.15 , proper^#(sel(X1, X2)) -> c_21(sel^#(proper(X1), proper(X2))) 1059.17/297.15 , proper^#(0()) -> c_22() 1059.17/297.15 , top^#(mark(X)) -> c_23(top^#(proper(X))) 1059.17/297.15 , top^#(ok(X)) -> c_24(top^#(active(X))) } 1059.17/297.15 Strict Trs: 1059.17/297.15 { active(from(X)) -> from(active(X)) 1059.17/297.15 , active(from(X)) -> mark(cons(X, from(s(X)))) 1059.17/297.15 , active(cons(X1, X2)) -> cons(active(X1), X2) 1059.17/297.15 , active(s(X)) -> s(active(X)) 1059.17/297.15 , active(sel(X1, X2)) -> sel(X1, active(X2)) 1059.17/297.15 , active(sel(X1, X2)) -> sel(active(X1), X2) 1059.17/297.15 , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)) 1059.17/297.15 , active(sel(0(), cons(X, Y))) -> mark(X) 1059.17/297.15 , from(mark(X)) -> mark(from(X)) 1059.17/297.15 , from(ok(X)) -> ok(from(X)) 1059.17/297.15 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1059.17/297.15 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1059.17/297.15 , s(mark(X)) -> mark(s(X)) 1059.17/297.15 , s(ok(X)) -> ok(s(X)) 1059.17/297.15 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 1059.17/297.15 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 1059.17/297.15 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 1059.17/297.15 , proper(from(X)) -> from(proper(X)) 1059.17/297.15 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1059.17/297.15 , proper(s(X)) -> s(proper(X)) 1059.17/297.15 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 1059.17/297.15 , proper(0()) -> ok(0()) 1059.17/297.15 , top(mark(X)) -> top(proper(X)) 1059.17/297.15 , top(ok(X)) -> top(active(X)) } 1059.17/297.15 Obligation: 1059.17/297.15 runtime complexity 1059.17/297.15 Answer: 1059.17/297.15 MAYBE 1059.17/297.15 1059.17/297.15 Consider the dependency graph: 1059.17/297.15 1059.17/297.15 1: active^#(from(X)) -> c_1(from^#(active(X))) 1059.17/297.15 -->_1 from^#(ok(X)) -> c_10(from^#(X)) :10 1059.17/297.15 -->_1 from^#(mark(X)) -> c_9(from^#(X)) :9 1059.17/297.15 1059.17/297.15 2: active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) 1059.17/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) :12 1059.17/297.15 -->_1 cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) :11 1059.17/297.15 1059.17/297.15 3: active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1059.17/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) :12 1059.17/297.15 -->_1 cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) :11 1059.17/297.15 1059.17/297.15 4: active^#(s(X)) -> c_4(s^#(active(X))) 1059.17/297.15 -->_1 s^#(ok(X)) -> c_14(s^#(X)) :14 1059.17/297.15 -->_1 s^#(mark(X)) -> c_13(s^#(X)) :13 1059.17/297.15 1059.17/297.15 5: active^#(sel(X1, X2)) -> c_5(sel^#(X1, active(X2))) 1059.17/297.15 -->_1 sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) :17 1059.17/297.15 -->_1 sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) :16 1059.17/297.15 -->_1 sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) :15 1059.17/297.15 1059.17/297.15 6: active^#(sel(X1, X2)) -> c_6(sel^#(active(X1), X2)) 1059.17/297.15 -->_1 sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) :17 1059.17/297.15 -->_1 sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) :16 1059.17/297.15 -->_1 sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) :15 1059.17/297.16 1059.17/297.16 7: active^#(sel(s(X), cons(Y, Z))) -> c_7(sel^#(X, Z)) 1059.17/297.16 -->_1 sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) :17 1059.17/297.16 -->_1 sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) :16 1059.17/297.16 -->_1 sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) :15 1059.17/297.16 1059.17/297.16 8: active^#(sel(0(), cons(X, Y))) -> c_8(X) 1059.17/297.16 -->_1 top^#(ok(X)) -> c_24(top^#(active(X))) :24 1059.17/297.16 -->_1 top^#(mark(X)) -> c_23(top^#(proper(X))) :23 1059.17/297.16 -->_1 proper^#(sel(X1, X2)) -> 1059.17/297.16 c_21(sel^#(proper(X1), proper(X2))) :21 1059.17/297.16 -->_1 proper^#(s(X)) -> c_20(s^#(proper(X))) :20 1059.17/297.16 -->_1 proper^#(cons(X1, X2)) -> 1059.17/297.16 c_19(cons^#(proper(X1), proper(X2))) :19 1059.17/297.16 -->_1 proper^#(from(X)) -> c_18(from^#(proper(X))) :18 1059.17/297.16 -->_1 sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) :17 1059.17/297.16 -->_1 sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) :16 1059.17/297.16 -->_1 sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) :15 1059.17/297.16 -->_1 s^#(ok(X)) -> c_14(s^#(X)) :14 1059.17/297.16 -->_1 s^#(mark(X)) -> c_13(s^#(X)) :13 1059.17/297.16 -->_1 cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) :12 1059.17/297.16 -->_1 cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) :11 1059.17/297.16 -->_1 from^#(ok(X)) -> c_10(from^#(X)) :10 1059.17/297.16 -->_1 from^#(mark(X)) -> c_9(from^#(X)) :9 1059.17/297.16 -->_1 proper^#(0()) -> c_22() :22 1059.17/297.16 -->_1 active^#(sel(0(), cons(X, Y))) -> c_8(X) :8 1059.17/297.16 -->_1 active^#(sel(s(X), cons(Y, Z))) -> c_7(sel^#(X, Z)) :7 1059.17/297.16 -->_1 active^#(sel(X1, X2)) -> c_6(sel^#(active(X1), X2)) :6 1059.17/297.16 -->_1 active^#(sel(X1, X2)) -> c_5(sel^#(X1, active(X2))) :5 1059.17/297.16 -->_1 active^#(s(X)) -> c_4(s^#(active(X))) :4 1059.17/297.16 -->_1 active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) :3 1059.17/297.16 -->_1 active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) :2 1059.17/297.16 -->_1 active^#(from(X)) -> c_1(from^#(active(X))) :1 1059.17/297.16 1059.17/297.16 9: from^#(mark(X)) -> c_9(from^#(X)) 1059.17/297.16 -->_1 from^#(ok(X)) -> c_10(from^#(X)) :10 1059.17/297.16 -->_1 from^#(mark(X)) -> c_9(from^#(X)) :9 1059.17/297.16 1059.17/297.16 10: from^#(ok(X)) -> c_10(from^#(X)) 1059.17/297.16 -->_1 from^#(ok(X)) -> c_10(from^#(X)) :10 1059.17/297.16 -->_1 from^#(mark(X)) -> c_9(from^#(X)) :9 1059.17/297.16 1059.17/297.16 11: cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) 1059.17/297.16 -->_1 cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) :12 1059.17/297.16 -->_1 cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) :11 1059.17/297.16 1059.17/297.16 12: cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) 1059.17/297.16 -->_1 cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) :12 1059.17/297.16 -->_1 cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) :11 1059.17/297.16 1059.17/297.16 13: s^#(mark(X)) -> c_13(s^#(X)) 1059.17/297.16 -->_1 s^#(ok(X)) -> c_14(s^#(X)) :14 1059.17/297.16 -->_1 s^#(mark(X)) -> c_13(s^#(X)) :13 1059.17/297.16 1059.17/297.16 14: s^#(ok(X)) -> c_14(s^#(X)) 1059.17/297.16 -->_1 s^#(ok(X)) -> c_14(s^#(X)) :14 1059.17/297.16 -->_1 s^#(mark(X)) -> c_13(s^#(X)) :13 1059.17/297.16 1059.17/297.16 15: sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) 1059.17/297.16 -->_1 sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) :17 1059.17/297.16 -->_1 sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) :16 1059.17/297.16 -->_1 sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) :15 1059.17/297.16 1059.17/297.16 16: sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) 1059.17/297.16 -->_1 sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) :17 1059.17/297.16 -->_1 sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) :16 1059.17/297.16 -->_1 sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) :15 1059.17/297.16 1059.17/297.16 17: sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) 1059.17/297.16 -->_1 sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) :17 1059.17/297.16 -->_1 sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) :16 1059.17/297.16 -->_1 sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) :15 1059.17/297.16 1059.17/297.16 18: proper^#(from(X)) -> c_18(from^#(proper(X))) 1059.17/297.16 -->_1 from^#(ok(X)) -> c_10(from^#(X)) :10 1059.17/297.16 -->_1 from^#(mark(X)) -> c_9(from^#(X)) :9 1059.17/297.16 1059.17/297.16 19: proper^#(cons(X1, X2)) -> c_19(cons^#(proper(X1), proper(X2))) 1059.17/297.16 -->_1 cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) :12 1059.17/297.16 -->_1 cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) :11 1059.17/297.16 1059.17/297.16 20: proper^#(s(X)) -> c_20(s^#(proper(X))) 1059.17/297.16 -->_1 s^#(ok(X)) -> c_14(s^#(X)) :14 1059.17/297.16 -->_1 s^#(mark(X)) -> c_13(s^#(X)) :13 1059.17/297.16 1059.17/297.16 21: proper^#(sel(X1, X2)) -> c_21(sel^#(proper(X1), proper(X2))) 1059.17/297.16 -->_1 sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) :17 1059.17/297.16 -->_1 sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) :16 1059.17/297.16 -->_1 sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) :15 1059.17/297.16 1059.17/297.16 22: proper^#(0()) -> c_22() 1059.17/297.16 1059.17/297.16 23: top^#(mark(X)) -> c_23(top^#(proper(X))) 1059.17/297.16 -->_1 top^#(ok(X)) -> c_24(top^#(active(X))) :24 1059.17/297.16 -->_1 top^#(mark(X)) -> c_23(top^#(proper(X))) :23 1059.17/297.16 1059.17/297.16 24: top^#(ok(X)) -> c_24(top^#(active(X))) 1059.17/297.16 -->_1 top^#(ok(X)) -> c_24(top^#(active(X))) :24 1059.17/297.16 -->_1 top^#(mark(X)) -> c_23(top^#(proper(X))) :23 1059.17/297.16 1059.17/297.16 1059.17/297.16 Only the nodes {9,10,11,12,13,14,15,17,16,22,23,24} are reachable 1059.17/297.16 from nodes {9,10,11,12,13,14,15,16,17,22,23,24} that start 1059.17/297.16 derivation from marked basic terms. The nodes not reachable are 1059.17/297.16 removed from the problem. 1059.17/297.16 1059.17/297.16 We are left with following problem, upon which TcT provides the 1059.17/297.16 certificate MAYBE. 1059.17/297.16 1059.17/297.16 Strict DPs: 1059.17/297.16 { from^#(mark(X)) -> c_9(from^#(X)) 1059.17/297.16 , from^#(ok(X)) -> c_10(from^#(X)) 1059.17/297.16 , cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) 1059.17/297.16 , cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) 1059.17/297.16 , s^#(mark(X)) -> c_13(s^#(X)) 1059.17/297.16 , s^#(ok(X)) -> c_14(s^#(X)) 1059.17/297.16 , sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) 1059.17/297.16 , sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) 1059.17/297.16 , sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) 1059.17/297.16 , proper^#(0()) -> c_22() 1059.17/297.16 , top^#(mark(X)) -> c_23(top^#(proper(X))) 1059.17/297.16 , top^#(ok(X)) -> c_24(top^#(active(X))) } 1059.17/297.16 Strict Trs: 1059.17/297.16 { active(from(X)) -> from(active(X)) 1059.17/297.16 , active(from(X)) -> mark(cons(X, from(s(X)))) 1059.17/297.16 , active(cons(X1, X2)) -> cons(active(X1), X2) 1059.17/297.16 , active(s(X)) -> s(active(X)) 1059.17/297.16 , active(sel(X1, X2)) -> sel(X1, active(X2)) 1059.17/297.16 , active(sel(X1, X2)) -> sel(active(X1), X2) 1059.17/297.16 , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)) 1059.17/297.16 , active(sel(0(), cons(X, Y))) -> mark(X) 1059.17/297.16 , from(mark(X)) -> mark(from(X)) 1059.17/297.16 , from(ok(X)) -> ok(from(X)) 1059.17/297.16 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1059.17/297.16 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1059.17/297.16 , s(mark(X)) -> mark(s(X)) 1059.17/297.16 , s(ok(X)) -> ok(s(X)) 1059.17/297.16 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 1059.17/297.16 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 1059.17/297.16 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 1059.17/297.16 , proper(from(X)) -> from(proper(X)) 1059.17/297.16 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1059.17/297.16 , proper(s(X)) -> s(proper(X)) 1059.17/297.16 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 1059.17/297.16 , proper(0()) -> ok(0()) 1059.17/297.16 , top(mark(X)) -> top(proper(X)) 1059.17/297.16 , top(ok(X)) -> top(active(X)) } 1059.17/297.16 Obligation: 1059.17/297.16 runtime complexity 1059.17/297.16 Answer: 1059.17/297.16 MAYBE 1059.17/297.16 1059.17/297.16 We estimate the number of application of {10} by applications of 1059.17/297.16 Pre({10}) = {}. Here rules are labeled as follows: 1059.17/297.16 1059.17/297.16 DPs: 1059.17/297.16 { 1: from^#(mark(X)) -> c_9(from^#(X)) 1059.17/297.16 , 2: from^#(ok(X)) -> c_10(from^#(X)) 1059.17/297.16 , 3: cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) 1059.17/297.16 , 4: cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) 1059.17/297.16 , 5: s^#(mark(X)) -> c_13(s^#(X)) 1059.17/297.16 , 6: s^#(ok(X)) -> c_14(s^#(X)) 1059.17/297.16 , 7: sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) 1059.17/297.16 , 8: sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) 1059.17/297.16 , 9: sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) 1059.17/297.16 , 10: proper^#(0()) -> c_22() 1059.17/297.16 , 11: top^#(mark(X)) -> c_23(top^#(proper(X))) 1059.17/297.16 , 12: top^#(ok(X)) -> c_24(top^#(active(X))) } 1059.17/297.16 1059.17/297.16 We are left with following problem, upon which TcT provides the 1059.17/297.16 certificate MAYBE. 1059.17/297.16 1059.17/297.16 Strict DPs: 1059.17/297.16 { from^#(mark(X)) -> c_9(from^#(X)) 1059.17/297.16 , from^#(ok(X)) -> c_10(from^#(X)) 1059.17/297.16 , cons^#(mark(X1), X2) -> c_11(cons^#(X1, X2)) 1059.17/297.16 , cons^#(ok(X1), ok(X2)) -> c_12(cons^#(X1, X2)) 1059.17/297.16 , s^#(mark(X)) -> c_13(s^#(X)) 1059.17/297.16 , s^#(ok(X)) -> c_14(s^#(X)) 1059.17/297.16 , sel^#(X1, mark(X2)) -> c_15(sel^#(X1, X2)) 1059.17/297.16 , sel^#(mark(X1), X2) -> c_16(sel^#(X1, X2)) 1059.17/297.16 , sel^#(ok(X1), ok(X2)) -> c_17(sel^#(X1, X2)) 1059.17/297.16 , top^#(mark(X)) -> c_23(top^#(proper(X))) 1059.17/297.16 , top^#(ok(X)) -> c_24(top^#(active(X))) } 1059.17/297.16 Strict Trs: 1059.17/297.16 { active(from(X)) -> from(active(X)) 1059.17/297.16 , active(from(X)) -> mark(cons(X, from(s(X)))) 1059.17/297.16 , active(cons(X1, X2)) -> cons(active(X1), X2) 1059.17/297.16 , active(s(X)) -> s(active(X)) 1059.17/297.16 , active(sel(X1, X2)) -> sel(X1, active(X2)) 1059.17/297.16 , active(sel(X1, X2)) -> sel(active(X1), X2) 1059.17/297.16 , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)) 1059.17/297.16 , active(sel(0(), cons(X, Y))) -> mark(X) 1059.17/297.16 , from(mark(X)) -> mark(from(X)) 1059.17/297.16 , from(ok(X)) -> ok(from(X)) 1059.17/297.16 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1059.17/297.16 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1059.17/297.16 , s(mark(X)) -> mark(s(X)) 1059.17/297.16 , s(ok(X)) -> ok(s(X)) 1059.17/297.16 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 1059.17/297.16 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 1059.17/297.16 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 1059.17/297.16 , proper(from(X)) -> from(proper(X)) 1059.17/297.16 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1059.17/297.16 , proper(s(X)) -> s(proper(X)) 1059.17/297.16 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 1059.17/297.16 , proper(0()) -> ok(0()) 1059.17/297.16 , top(mark(X)) -> top(proper(X)) 1059.17/297.16 , top(ok(X)) -> top(active(X)) } 1059.17/297.16 Weak DPs: { proper^#(0()) -> c_22() } 1059.17/297.16 Obligation: 1059.17/297.16 runtime complexity 1059.17/297.16 Answer: 1059.17/297.16 MAYBE 1059.17/297.16 1059.17/297.16 Empty strict component of the problem is NOT empty. 1059.17/297.16 1059.17/297.16 1059.17/297.16 Arrrr.. 1059.55/297.34 EOF