MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { max(L(x)) -> x , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { max^#(L(x)) -> c_1() , max^#(N(L(x), N(y, z))) -> c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) , max^#(N(L(0()), L(y))) -> c_3() , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { max^#(L(x)) -> c_1() , max^#(N(L(x), N(y, z))) -> c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) , max^#(N(L(0()), L(y))) -> c_3() , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } Weak Trs: { max(L(x)) -> x , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,3} by applications of Pre({1,3}) = {2,4}. Here rules are labeled as follows: DPs: { 1: max^#(L(x)) -> c_1() , 2: max^#(N(L(x), N(y, z))) -> c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) , 3: max^#(N(L(0()), L(y))) -> c_3() , 4: max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { max^#(N(L(x), N(y, z))) -> c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } Weak DPs: { max^#(L(x)) -> c_1() , max^#(N(L(0()), L(y))) -> c_3() } Weak Trs: { max(L(x)) -> x , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(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. { max^#(L(x)) -> c_1() , max^#(N(L(0()), L(y))) -> c_3() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { max^#(N(L(x), N(y, z))) -> c_2(max^#(N(L(x), L(max(N(y, z))))), max^#(N(y, z))) , max^#(N(L(s(x)), L(s(y)))) -> c_4(max^#(N(L(x), L(y)))) } Weak Trs: { max(L(x)) -> x , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..