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