MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, x, r)) -> false() , left(empty()) -> empty() , left(node(l, x, r)) -> l , right(empty()) -> empty() , right(node(l, x, r)) -> r , elem(node(l, x, r)) -> x , append(nil(), x) -> cons(x, nil()) , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) , listify(n, xs) -> if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)) , if(true(), b, n, m, xs, ys) -> xs , if(false(), true(), n, m, xs, ys) -> listify(n, ys) , if(false(), false(), n, m, xs, ys) -> listify(m, xs) , toList(n) -> listify(n, nil()) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { isEmpty^#(empty()) -> c_1() , isEmpty^#(node(l, x, r)) -> c_2() , left^#(empty()) -> c_3() , left^#(node(l, x, r)) -> c_4() , right^#(empty()) -> c_5() , right^#(node(l, x, r)) -> c_6() , elem^#(node(l, x, r)) -> c_7() , append^#(nil(), x) -> c_8() , append^#(cons(y(), ys), x) -> c_9(append^#(ys, x)) , listify^#(n, xs) -> c_10(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), isEmpty^#(n), isEmpty^#(left(n)), left^#(n), right^#(n), left^#(left(n)), left^#(n), elem^#(left(n)), left^#(n), right^#(left(n)), left^#(n), elem^#(n), right^#(n), append^#(xs, n)) , if^#(true(), b, n, m, xs, ys) -> c_11() , if^#(false(), true(), n, m, xs, ys) -> c_12(listify^#(n, ys)) , if^#(false(), false(), n, m, xs, ys) -> c_13(listify^#(m, xs)) , toList^#(n) -> c_14(listify^#(n, nil())) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isEmpty^#(empty()) -> c_1() , isEmpty^#(node(l, x, r)) -> c_2() , left^#(empty()) -> c_3() , left^#(node(l, x, r)) -> c_4() , right^#(empty()) -> c_5() , right^#(node(l, x, r)) -> c_6() , elem^#(node(l, x, r)) -> c_7() , append^#(nil(), x) -> c_8() , append^#(cons(y(), ys), x) -> c_9(append^#(ys, x)) , listify^#(n, xs) -> c_10(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), isEmpty^#(n), isEmpty^#(left(n)), left^#(n), right^#(n), left^#(left(n)), left^#(n), elem^#(left(n)), left^#(n), right^#(left(n)), left^#(n), elem^#(n), right^#(n), append^#(xs, n)) , if^#(true(), b, n, m, xs, ys) -> c_11() , if^#(false(), true(), n, m, xs, ys) -> c_12(listify^#(n, ys)) , if^#(false(), false(), n, m, xs, ys) -> c_13(listify^#(m, xs)) , toList^#(n) -> c_14(listify^#(n, nil())) } Weak Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, x, r)) -> false() , left(empty()) -> empty() , left(node(l, x, r)) -> l , right(empty()) -> empty() , right(node(l, x, r)) -> r , elem(node(l, x, r)) -> x , append(nil(), x) -> cons(x, nil()) , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) , listify(n, xs) -> if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)) , if(true(), b, n, m, xs, ys) -> xs , if(false(), true(), n, m, xs, ys) -> listify(n, ys) , if(false(), false(), n, m, xs, ys) -> listify(m, xs) , toList(n) -> listify(n, nil()) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4,5,6,7,8,11} by applications of Pre({1,2,3,4,5,6,7,8,11}) = {9,10}. Here rules are labeled as follows: DPs: { 1: isEmpty^#(empty()) -> c_1() , 2: isEmpty^#(node(l, x, r)) -> c_2() , 3: left^#(empty()) -> c_3() , 4: left^#(node(l, x, r)) -> c_4() , 5: right^#(empty()) -> c_5() , 6: right^#(node(l, x, r)) -> c_6() , 7: elem^#(node(l, x, r)) -> c_7() , 8: append^#(nil(), x) -> c_8() , 9: append^#(cons(y(), ys), x) -> c_9(append^#(ys, x)) , 10: listify^#(n, xs) -> c_10(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), isEmpty^#(n), isEmpty^#(left(n)), left^#(n), right^#(n), left^#(left(n)), left^#(n), elem^#(left(n)), left^#(n), right^#(left(n)), left^#(n), elem^#(n), right^#(n), append^#(xs, n)) , 11: if^#(true(), b, n, m, xs, ys) -> c_11() , 12: if^#(false(), true(), n, m, xs, ys) -> c_12(listify^#(n, ys)) , 13: if^#(false(), false(), n, m, xs, ys) -> c_13(listify^#(m, xs)) , 14: toList^#(n) -> c_14(listify^#(n, nil())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(cons(y(), ys), x) -> c_9(append^#(ys, x)) , listify^#(n, xs) -> c_10(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), isEmpty^#(n), isEmpty^#(left(n)), left^#(n), right^#(n), left^#(left(n)), left^#(n), elem^#(left(n)), left^#(n), right^#(left(n)), left^#(n), elem^#(n), right^#(n), append^#(xs, n)) , if^#(false(), true(), n, m, xs, ys) -> c_12(listify^#(n, ys)) , if^#(false(), false(), n, m, xs, ys) -> c_13(listify^#(m, xs)) , toList^#(n) -> c_14(listify^#(n, nil())) } Weak DPs: { isEmpty^#(empty()) -> c_1() , isEmpty^#(node(l, x, r)) -> c_2() , left^#(empty()) -> c_3() , left^#(node(l, x, r)) -> c_4() , right^#(empty()) -> c_5() , right^#(node(l, x, r)) -> c_6() , elem^#(node(l, x, r)) -> c_7() , append^#(nil(), x) -> c_8() , if^#(true(), b, n, m, xs, ys) -> c_11() } Weak Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, x, r)) -> false() , left(empty()) -> empty() , left(node(l, x, r)) -> l , right(empty()) -> empty() , right(node(l, x, r)) -> r , elem(node(l, x, r)) -> x , append(nil(), x) -> cons(x, nil()) , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) , listify(n, xs) -> if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)) , if(true(), b, n, m, xs, ys) -> xs , if(false(), true(), n, m, xs, ys) -> listify(n, ys) , if(false(), false(), n, m, xs, ys) -> listify(m, xs) , toList(n) -> listify(n, nil()) } 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^#(empty()) -> c_1() , isEmpty^#(node(l, x, r)) -> c_2() , left^#(empty()) -> c_3() , left^#(node(l, x, r)) -> c_4() , right^#(empty()) -> c_5() , right^#(node(l, x, r)) -> c_6() , elem^#(node(l, x, r)) -> c_7() , append^#(nil(), x) -> c_8() , if^#(true(), b, n, m, xs, ys) -> c_11() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(cons(y(), ys), x) -> c_9(append^#(ys, x)) , listify^#(n, xs) -> c_10(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), isEmpty^#(n), isEmpty^#(left(n)), left^#(n), right^#(n), left^#(left(n)), left^#(n), elem^#(left(n)), left^#(n), right^#(left(n)), left^#(n), elem^#(n), right^#(n), append^#(xs, n)) , if^#(false(), true(), n, m, xs, ys) -> c_12(listify^#(n, ys)) , if^#(false(), false(), n, m, xs, ys) -> c_13(listify^#(m, xs)) , toList^#(n) -> c_14(listify^#(n, nil())) } Weak Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, x, r)) -> false() , left(empty()) -> empty() , left(node(l, x, r)) -> l , right(empty()) -> empty() , right(node(l, x, r)) -> r , elem(node(l, x, r)) -> x , append(nil(), x) -> cons(x, nil()) , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) , listify(n, xs) -> if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)) , if(true(), b, n, m, xs, ys) -> xs , if(false(), true(), n, m, xs, ys) -> listify(n, ys) , if(false(), false(), n, m, xs, ys) -> listify(m, xs) , toList(n) -> listify(n, nil()) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { listify^#(n, xs) -> c_10(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), isEmpty^#(n), isEmpty^#(left(n)), left^#(n), right^#(n), left^#(left(n)), left^#(n), elem^#(left(n)), left^#(n), right^#(left(n)), left^#(n), elem^#(n), right^#(n), append^#(xs, n)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(cons(y(), ys), x) -> c_1(append^#(ys, x)) , listify^#(n, xs) -> c_2(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), append^#(xs, n)) , if^#(false(), true(), n, m, xs, ys) -> c_3(listify^#(n, ys)) , if^#(false(), false(), n, m, xs, ys) -> c_4(listify^#(m, xs)) , toList^#(n) -> c_5(listify^#(n, nil())) } Weak Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, x, r)) -> false() , left(empty()) -> empty() , left(node(l, x, r)) -> l , right(empty()) -> empty() , right(node(l, x, r)) -> r , elem(node(l, x, r)) -> x , append(nil(), x) -> cons(x, nil()) , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) , listify(n, xs) -> if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)) , if(true(), b, n, m, xs, ys) -> xs , if(false(), true(), n, m, xs, ys) -> listify(n, ys) , if(false(), false(), n, m, xs, ys) -> listify(m, xs) , toList(n) -> listify(n, nil()) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { isEmpty(empty()) -> true() , isEmpty(node(l, x, r)) -> false() , left(empty()) -> empty() , left(node(l, x, r)) -> l , right(empty()) -> empty() , right(node(l, x, r)) -> r , elem(node(l, x, r)) -> x , append(nil(), x) -> cons(x, nil()) , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(cons(y(), ys), x) -> c_1(append^#(ys, x)) , listify^#(n, xs) -> c_2(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), append^#(xs, n)) , if^#(false(), true(), n, m, xs, ys) -> c_3(listify^#(n, ys)) , if^#(false(), false(), n, m, xs, ys) -> c_4(listify^#(m, xs)) , toList^#(n) -> c_5(listify^#(n, nil())) } Weak Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, x, r)) -> false() , left(empty()) -> empty() , left(node(l, x, r)) -> l , right(empty()) -> empty() , right(node(l, x, r)) -> r , elem(node(l, x, r)) -> x , append(nil(), x) -> cons(x, nil()) , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: append^#(cons(y(), ys), x) -> c_1(append^#(ys, x)) -->_1 append^#(cons(y(), ys), x) -> c_1(append^#(ys, x)) :1 2: listify^#(n, xs) -> c_2(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), append^#(xs, n)) -->_1 if^#(false(), false(), n, m, xs, ys) -> c_4(listify^#(m, xs)) :4 -->_1 if^#(false(), true(), n, m, xs, ys) -> c_3(listify^#(n, ys)) :3 -->_2 append^#(cons(y(), ys), x) -> c_1(append^#(ys, x)) :1 3: if^#(false(), true(), n, m, xs, ys) -> c_3(listify^#(n, ys)) -->_1 listify^#(n, xs) -> c_2(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), append^#(xs, n)) :2 4: if^#(false(), false(), n, m, xs, ys) -> c_4(listify^#(m, xs)) -->_1 listify^#(n, xs) -> c_2(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), append^#(xs, n)) :2 5: toList^#(n) -> c_5(listify^#(n, nil())) -->_1 listify^#(n, xs) -> c_2(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), append^#(xs, n)) :2 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). { toList^#(n) -> c_5(listify^#(n, nil())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(cons(y(), ys), x) -> c_1(append^#(ys, x)) , listify^#(n, xs) -> c_2(if^#(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)), append^#(xs, n)) , if^#(false(), true(), n, m, xs, ys) -> c_3(listify^#(n, ys)) , if^#(false(), false(), n, m, xs, ys) -> c_4(listify^#(m, xs)) } Weak Trs: { isEmpty(empty()) -> true() , isEmpty(node(l, x, r)) -> false() , left(empty()) -> empty() , left(node(l, x, r)) -> l , right(empty()) -> empty() , right(node(l, x, r)) -> r , elem(node(l, x, r)) -> x , append(nil(), x) -> cons(x, nil()) , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..