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