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