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