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