MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { isEmpty(nil()) -> true() , isEmpty(cons(x, xs)) -> false() , last(cons(x, nil())) -> x , last(cons(x, cons(y, ys))) -> last(cons(y, ys)) , dropLast(nil()) -> nil() , dropLast(cons(x, nil())) -> nil() , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys))) , append(nil(), ys) -> ys , append(cons(x, xs), ys) -> cons(x, append(xs, ys)) , reverse(xs) -> rev(xs, nil()) , rev(xs, ys) -> if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys) , if(true(), xs, ys, zs) -> zs , if(false(), xs, ys, zs) -> rev(xs, ys) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { isEmpty^#(nil()) -> c_1() , isEmpty^#(cons(x, xs)) -> c_2() , last^#(cons(x, nil())) -> c_3() , last^#(cons(x, cons(y, ys))) -> c_4(last^#(cons(y, ys))) , dropLast^#(nil()) -> c_5() , dropLast^#(cons(x, nil())) -> c_6() , dropLast^#(cons(x, cons(y, ys))) -> c_7(dropLast^#(cons(y, ys))) , append^#(nil(), ys) -> c_8() , append^#(cons(x, xs), ys) -> c_9(append^#(xs, ys)) , reverse^#(xs) -> c_10(rev^#(xs, nil())) , rev^#(xs, ys) -> c_11(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), isEmpty^#(xs), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) , if^#(true(), xs, ys, zs) -> c_12() , if^#(false(), xs, ys, zs) -> c_13(rev^#(xs, ys)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isEmpty^#(nil()) -> c_1() , isEmpty^#(cons(x, xs)) -> c_2() , last^#(cons(x, nil())) -> c_3() , last^#(cons(x, cons(y, ys))) -> c_4(last^#(cons(y, ys))) , dropLast^#(nil()) -> c_5() , dropLast^#(cons(x, nil())) -> c_6() , dropLast^#(cons(x, cons(y, ys))) -> c_7(dropLast^#(cons(y, ys))) , append^#(nil(), ys) -> c_8() , append^#(cons(x, xs), ys) -> c_9(append^#(xs, ys)) , reverse^#(xs) -> c_10(rev^#(xs, nil())) , rev^#(xs, ys) -> c_11(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), isEmpty^#(xs), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) , if^#(true(), xs, ys, zs) -> c_12() , if^#(false(), xs, ys, zs) -> c_13(rev^#(xs, ys)) } Weak Trs: { isEmpty(nil()) -> true() , isEmpty(cons(x, xs)) -> false() , last(cons(x, nil())) -> x , last(cons(x, cons(y, ys))) -> last(cons(y, ys)) , dropLast(nil()) -> nil() , dropLast(cons(x, nil())) -> nil() , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys))) , append(nil(), ys) -> ys , append(cons(x, xs), ys) -> cons(x, append(xs, ys)) , reverse(xs) -> rev(xs, nil()) , rev(xs, ys) -> if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys) , if(true(), xs, ys, zs) -> zs , if(false(), xs, ys, zs) -> rev(xs, ys) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,5,6,8,12} by applications of Pre({1,2,3,5,6,8,12}) = {4,7,9,11}. Here rules are labeled as follows: DPs: { 1: isEmpty^#(nil()) -> c_1() , 2: isEmpty^#(cons(x, xs)) -> c_2() , 3: last^#(cons(x, nil())) -> c_3() , 4: last^#(cons(x, cons(y, ys))) -> c_4(last^#(cons(y, ys))) , 5: dropLast^#(nil()) -> c_5() , 6: dropLast^#(cons(x, nil())) -> c_6() , 7: dropLast^#(cons(x, cons(y, ys))) -> c_7(dropLast^#(cons(y, ys))) , 8: append^#(nil(), ys) -> c_8() , 9: append^#(cons(x, xs), ys) -> c_9(append^#(xs, ys)) , 10: reverse^#(xs) -> c_10(rev^#(xs, nil())) , 11: rev^#(xs, ys) -> c_11(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), isEmpty^#(xs), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) , 12: if^#(true(), xs, ys, zs) -> c_12() , 13: if^#(false(), xs, ys, zs) -> c_13(rev^#(xs, ys)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { last^#(cons(x, cons(y, ys))) -> c_4(last^#(cons(y, ys))) , dropLast^#(cons(x, cons(y, ys))) -> c_7(dropLast^#(cons(y, ys))) , append^#(cons(x, xs), ys) -> c_9(append^#(xs, ys)) , reverse^#(xs) -> c_10(rev^#(xs, nil())) , rev^#(xs, ys) -> c_11(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), isEmpty^#(xs), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) , if^#(false(), xs, ys, zs) -> c_13(rev^#(xs, ys)) } Weak DPs: { isEmpty^#(nil()) -> c_1() , isEmpty^#(cons(x, xs)) -> c_2() , last^#(cons(x, nil())) -> c_3() , dropLast^#(nil()) -> c_5() , dropLast^#(cons(x, nil())) -> c_6() , append^#(nil(), ys) -> c_8() , if^#(true(), xs, ys, zs) -> c_12() } Weak Trs: { isEmpty(nil()) -> true() , isEmpty(cons(x, xs)) -> false() , last(cons(x, nil())) -> x , last(cons(x, cons(y, ys))) -> last(cons(y, ys)) , dropLast(nil()) -> nil() , dropLast(cons(x, nil())) -> nil() , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys))) , append(nil(), ys) -> ys , append(cons(x, xs), ys) -> cons(x, append(xs, ys)) , reverse(xs) -> rev(xs, nil()) , rev(xs, ys) -> if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys) , if(true(), xs, ys, zs) -> zs , if(false(), xs, ys, zs) -> rev(xs, ys) } 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. { isEmpty^#(nil()) -> c_1() , isEmpty^#(cons(x, xs)) -> c_2() , last^#(cons(x, nil())) -> c_3() , dropLast^#(nil()) -> c_5() , dropLast^#(cons(x, nil())) -> c_6() , append^#(nil(), ys) -> c_8() , if^#(true(), xs, ys, zs) -> c_12() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { last^#(cons(x, cons(y, ys))) -> c_4(last^#(cons(y, ys))) , dropLast^#(cons(x, cons(y, ys))) -> c_7(dropLast^#(cons(y, ys))) , append^#(cons(x, xs), ys) -> c_9(append^#(xs, ys)) , reverse^#(xs) -> c_10(rev^#(xs, nil())) , rev^#(xs, ys) -> c_11(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), isEmpty^#(xs), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) , if^#(false(), xs, ys, zs) -> c_13(rev^#(xs, ys)) } Weak Trs: { isEmpty(nil()) -> true() , isEmpty(cons(x, xs)) -> false() , last(cons(x, nil())) -> x , last(cons(x, cons(y, ys))) -> last(cons(y, ys)) , dropLast(nil()) -> nil() , dropLast(cons(x, nil())) -> nil() , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys))) , append(nil(), ys) -> ys , append(cons(x, xs), ys) -> cons(x, append(xs, ys)) , reverse(xs) -> rev(xs, nil()) , rev(xs, ys) -> if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys) , if(true(), xs, ys, zs) -> zs , if(false(), xs, ys, zs) -> rev(xs, ys) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { rev^#(xs, ys) -> c_11(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), isEmpty^#(xs), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { last^#(cons(x, cons(y, ys))) -> c_1(last^#(cons(y, ys))) , dropLast^#(cons(x, cons(y, ys))) -> c_2(dropLast^#(cons(y, ys))) , append^#(cons(x, xs), ys) -> c_3(append^#(xs, ys)) , reverse^#(xs) -> c_4(rev^#(xs, nil())) , rev^#(xs, ys) -> c_5(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) , if^#(false(), xs, ys, zs) -> c_6(rev^#(xs, ys)) } Weak Trs: { isEmpty(nil()) -> true() , isEmpty(cons(x, xs)) -> false() , last(cons(x, nil())) -> x , last(cons(x, cons(y, ys))) -> last(cons(y, ys)) , dropLast(nil()) -> nil() , dropLast(cons(x, nil())) -> nil() , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys))) , append(nil(), ys) -> ys , append(cons(x, xs), ys) -> cons(x, append(xs, ys)) , reverse(xs) -> rev(xs, nil()) , rev(xs, ys) -> if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys) , if(true(), xs, ys, zs) -> zs , if(false(), xs, ys, zs) -> rev(xs, ys) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { isEmpty(nil()) -> true() , isEmpty(cons(x, xs)) -> false() , last(cons(x, nil())) -> x , last(cons(x, cons(y, ys))) -> last(cons(y, ys)) , dropLast(nil()) -> nil() , dropLast(cons(x, nil())) -> nil() , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys))) , append(nil(), ys) -> ys , append(cons(x, xs), ys) -> cons(x, append(xs, ys)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { last^#(cons(x, cons(y, ys))) -> c_1(last^#(cons(y, ys))) , dropLast^#(cons(x, cons(y, ys))) -> c_2(dropLast^#(cons(y, ys))) , append^#(cons(x, xs), ys) -> c_3(append^#(xs, ys)) , reverse^#(xs) -> c_4(rev^#(xs, nil())) , rev^#(xs, ys) -> c_5(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) , if^#(false(), xs, ys, zs) -> c_6(rev^#(xs, ys)) } Weak Trs: { isEmpty(nil()) -> true() , isEmpty(cons(x, xs)) -> false() , last(cons(x, nil())) -> x , last(cons(x, cons(y, ys))) -> last(cons(y, ys)) , dropLast(nil()) -> nil() , dropLast(cons(x, nil())) -> nil() , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys))) , append(nil(), ys) -> ys , append(cons(x, xs), ys) -> cons(x, append(xs, ys)) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: last^#(cons(x, cons(y, ys))) -> c_1(last^#(cons(y, ys))) -->_1 last^#(cons(x, cons(y, ys))) -> c_1(last^#(cons(y, ys))) :1 2: dropLast^#(cons(x, cons(y, ys))) -> c_2(dropLast^#(cons(y, ys))) -->_1 dropLast^#(cons(x, cons(y, ys))) -> c_2(dropLast^#(cons(y, ys))) :2 3: append^#(cons(x, xs), ys) -> c_3(append^#(xs, ys)) -->_1 append^#(cons(x, xs), ys) -> c_3(append^#(xs, ys)) :3 4: reverse^#(xs) -> c_4(rev^#(xs, nil())) -->_1 rev^#(xs, ys) -> c_5(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) :5 5: rev^#(xs, ys) -> c_5(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) -->_1 if^#(false(), xs, ys, zs) -> c_6(rev^#(xs, ys)) :6 -->_3 append^#(cons(x, xs), ys) -> c_3(append^#(xs, ys)) :3 -->_2 dropLast^#(cons(x, cons(y, ys))) -> c_2(dropLast^#(cons(y, ys))) :2 -->_4 last^#(cons(x, cons(y, ys))) -> c_1(last^#(cons(y, ys))) :1 6: if^#(false(), xs, ys, zs) -> c_6(rev^#(xs, ys)) -->_1 rev^#(xs, ys) -> c_5(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) :5 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { reverse^#(xs) -> c_4(rev^#(xs, nil())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { last^#(cons(x, cons(y, ys))) -> c_1(last^#(cons(y, ys))) , dropLast^#(cons(x, cons(y, ys))) -> c_2(dropLast^#(cons(y, ys))) , append^#(cons(x, xs), ys) -> c_3(append^#(xs, ys)) , rev^#(xs, ys) -> c_5(if^#(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys), dropLast^#(xs), append^#(ys, last(xs)), last^#(xs)) , if^#(false(), xs, ys, zs) -> c_6(rev^#(xs, ys)) } Weak Trs: { isEmpty(nil()) -> true() , isEmpty(cons(x, xs)) -> false() , last(cons(x, nil())) -> x , last(cons(x, cons(y, ys))) -> last(cons(y, ys)) , dropLast(nil()) -> nil() , dropLast(cons(x, nil())) -> nil() , dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys))) , append(nil(), ys) -> ys , append(cons(x, xs), ys) -> cons(x, append(xs, ys)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..