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