MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { incr^#(nil()) -> c_1() , incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(nil()) -> c_3() , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) , head^#(cons(X, L)) -> c_7() , tail^#(cons(X, L)) -> c_8() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(nil()) -> c_1() , incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(nil()) -> c_3() , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) , head^#(cons(X, L)) -> c_7() , tail^#(cons(X, L)) -> c_8() } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,3,7,8} by applications of Pre({1,3,7,8}) = {2,4,5}. Here rules are labeled as follows: DPs: { 1: incr^#(nil()) -> c_1() , 2: incr^#(cons(X, L)) -> c_2(incr^#(L)) , 3: adx^#(nil()) -> c_3() , 4: adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , 5: nats^#() -> c_5(adx^#(zeros()), zeros^#()) , 6: zeros^#() -> c_6(zeros^#()) , 7: head^#(cons(X, L)) -> c_7() , 8: tail^#(cons(X, L)) -> c_8() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak DPs: { incr^#(nil()) -> c_1() , adx^#(nil()) -> c_3() , head^#(cons(X, L)) -> c_7() , tail^#(cons(X, L)) -> c_8() } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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. { incr^#(nil()) -> c_1() , adx^#(nil()) -> c_3() , head^#(cons(X, L)) -> c_7() , tail^#(cons(X, L)) -> c_8() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , zeros() -> cons(0(), zeros()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , zeros() -> cons(0(), zeros()) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..