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