MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { fib(0()) -> 0() , fib(s(0())) -> s(0()) , fib(s(s(x))) -> sp(g(x)) , fib(s(s(0()))) -> s(0()) , sp(pair(x, y)) -> +(x, y) , g(0()) -> pair(s(0()), 0()) , g(s(x)) -> np(g(x)) , g(s(0())) -> pair(s(0()), s(0())) , np(pair(x, y)) -> pair(+(x, y), x) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { fib^#(0()) -> c_1() , fib^#(s(0())) -> c_2() , fib^#(s(s(x))) -> c_3(sp^#(g(x)), g^#(x)) , fib^#(s(s(0()))) -> c_4() , sp^#(pair(x, y)) -> c_5(+^#(x, y)) , g^#(0()) -> c_6() , g^#(s(x)) -> c_7(np^#(g(x)), g^#(x)) , g^#(s(0())) -> c_8() , +^#(x, 0()) -> c_10() , +^#(x, s(y)) -> c_11(+^#(x, y)) , np^#(pair(x, y)) -> c_9(+^#(x, y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fib^#(0()) -> c_1() , fib^#(s(0())) -> c_2() , fib^#(s(s(x))) -> c_3(sp^#(g(x)), g^#(x)) , fib^#(s(s(0()))) -> c_4() , sp^#(pair(x, y)) -> c_5(+^#(x, y)) , g^#(0()) -> c_6() , g^#(s(x)) -> c_7(np^#(g(x)), g^#(x)) , g^#(s(0())) -> c_8() , +^#(x, 0()) -> c_10() , +^#(x, s(y)) -> c_11(+^#(x, y)) , np^#(pair(x, y)) -> c_9(+^#(x, y)) } Weak Trs: { fib(0()) -> 0() , fib(s(0())) -> s(0()) , fib(s(s(x))) -> sp(g(x)) , fib(s(s(0()))) -> s(0()) , sp(pair(x, y)) -> +(x, y) , g(0()) -> pair(s(0()), 0()) , g(s(x)) -> np(g(x)) , g(s(0())) -> pair(s(0()), s(0())) , np(pair(x, y)) -> pair(+(x, y), x) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,4,6,8,9} by applications of Pre({1,2,4,6,8,9}) = {3,5,7,10,11}. Here rules are labeled as follows: DPs: { 1: fib^#(0()) -> c_1() , 2: fib^#(s(0())) -> c_2() , 3: fib^#(s(s(x))) -> c_3(sp^#(g(x)), g^#(x)) , 4: fib^#(s(s(0()))) -> c_4() , 5: sp^#(pair(x, y)) -> c_5(+^#(x, y)) , 6: g^#(0()) -> c_6() , 7: g^#(s(x)) -> c_7(np^#(g(x)), g^#(x)) , 8: g^#(s(0())) -> c_8() , 9: +^#(x, 0()) -> c_10() , 10: +^#(x, s(y)) -> c_11(+^#(x, y)) , 11: np^#(pair(x, y)) -> c_9(+^#(x, y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fib^#(s(s(x))) -> c_3(sp^#(g(x)), g^#(x)) , sp^#(pair(x, y)) -> c_5(+^#(x, y)) , g^#(s(x)) -> c_7(np^#(g(x)), g^#(x)) , +^#(x, s(y)) -> c_11(+^#(x, y)) , np^#(pair(x, y)) -> c_9(+^#(x, y)) } Weak DPs: { fib^#(0()) -> c_1() , fib^#(s(0())) -> c_2() , fib^#(s(s(0()))) -> c_4() , g^#(0()) -> c_6() , g^#(s(0())) -> c_8() , +^#(x, 0()) -> c_10() } Weak Trs: { fib(0()) -> 0() , fib(s(0())) -> s(0()) , fib(s(s(x))) -> sp(g(x)) , fib(s(s(0()))) -> s(0()) , sp(pair(x, y)) -> +(x, y) , g(0()) -> pair(s(0()), 0()) , g(s(x)) -> np(g(x)) , g(s(0())) -> pair(s(0()), s(0())) , np(pair(x, y)) -> pair(+(x, y), x) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { fib^#(0()) -> c_1() , fib^#(s(0())) -> c_2() , fib^#(s(s(0()))) -> c_4() , g^#(0()) -> c_6() , g^#(s(0())) -> c_8() , +^#(x, 0()) -> c_10() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fib^#(s(s(x))) -> c_3(sp^#(g(x)), g^#(x)) , sp^#(pair(x, y)) -> c_5(+^#(x, y)) , g^#(s(x)) -> c_7(np^#(g(x)), g^#(x)) , +^#(x, s(y)) -> c_11(+^#(x, y)) , np^#(pair(x, y)) -> c_9(+^#(x, y)) } Weak Trs: { fib(0()) -> 0() , fib(s(0())) -> s(0()) , fib(s(s(x))) -> sp(g(x)) , fib(s(s(0()))) -> s(0()) , sp(pair(x, y)) -> +(x, y) , g(0()) -> pair(s(0()), 0()) , g(s(x)) -> np(g(x)) , g(s(0())) -> pair(s(0()), s(0())) , np(pair(x, y)) -> pair(+(x, y), x) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { g(0()) -> pair(s(0()), 0()) , g(s(x)) -> np(g(x)) , g(s(0())) -> pair(s(0()), s(0())) , np(pair(x, y)) -> pair(+(x, y), x) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fib^#(s(s(x))) -> c_3(sp^#(g(x)), g^#(x)) , sp^#(pair(x, y)) -> c_5(+^#(x, y)) , g^#(s(x)) -> c_7(np^#(g(x)), g^#(x)) , +^#(x, s(y)) -> c_11(+^#(x, y)) , np^#(pair(x, y)) -> c_9(+^#(x, y)) } Weak Trs: { g(0()) -> pair(s(0()), 0()) , g(s(x)) -> np(g(x)) , g(s(0())) -> pair(s(0()), s(0())) , np(pair(x, y)) -> pair(+(x, y), x) , +(x, 0()) -> x , +(x, s(y)) -> s(+(x, y)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..