MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { lessElements(l, t) -> lessE(l, t, 0()) , lessE(l, t, n) -> if(le(length(l), n), le(length(toList(t)), n), l, t, n) , if(true(), b, l, t, n) -> l , if(false(), true(), l, t, n) -> t , if(false(), false(), l, t, n) -> lessE(l, t, s(n)) , le(0(), m) -> true() , le(s(n), 0()) -> false() , le(s(n), s(m)) -> le(n, m) , length(nil()) -> 0() , length(cons(n, l)) -> s(length(l)) , toList(leaf()) -> nil() , toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2))) , append(nil(), l2) -> l2 , append(cons(n, l1), l2) -> cons(n, append(l1, l2)) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { lessElements^#(l, t) -> c_1(lessE^#(l, t, 0())) , lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) , if^#(true(), b, l, t, n) -> c_3() , if^#(false(), true(), l, t, n) -> c_4() , if^#(false(), false(), l, t, n) -> c_5(lessE^#(l, t, s(n))) , le^#(0(), m) -> c_6() , le^#(s(n), 0()) -> c_7() , le^#(s(n), s(m)) -> c_8(le^#(n, m)) , length^#(nil()) -> c_9() , length^#(cons(n, l)) -> c_10(length^#(l)) , toList^#(leaf()) -> c_11() , toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) , append^#(nil(), l2) -> c_13() , append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) , a^#() -> c_15() , a^#() -> c_16() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { lessElements^#(l, t) -> c_1(lessE^#(l, t, 0())) , lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) , if^#(true(), b, l, t, n) -> c_3() , if^#(false(), true(), l, t, n) -> c_4() , if^#(false(), false(), l, t, n) -> c_5(lessE^#(l, t, s(n))) , le^#(0(), m) -> c_6() , le^#(s(n), 0()) -> c_7() , le^#(s(n), s(m)) -> c_8(le^#(n, m)) , length^#(nil()) -> c_9() , length^#(cons(n, l)) -> c_10(length^#(l)) , toList^#(leaf()) -> c_11() , toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) , append^#(nil(), l2) -> c_13() , append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) , a^#() -> c_15() , a^#() -> c_16() } Weak Trs: { lessElements(l, t) -> lessE(l, t, 0()) , lessE(l, t, n) -> if(le(length(l), n), le(length(toList(t)), n), l, t, n) , if(true(), b, l, t, n) -> l , if(false(), true(), l, t, n) -> t , if(false(), false(), l, t, n) -> lessE(l, t, s(n)) , le(0(), m) -> true() , le(s(n), 0()) -> false() , le(s(n), s(m)) -> le(n, m) , length(nil()) -> 0() , length(cons(n, l)) -> s(length(l)) , toList(leaf()) -> nil() , toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2))) , append(nil(), l2) -> l2 , append(cons(n, l1), l2) -> cons(n, append(l1, l2)) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,4,6,7,9,11,13,15,16} by applications of Pre({3,4,6,7,9,11,13,15,16}) = {2,8,10,12,14}. Here rules are labeled as follows: DPs: { 1: lessElements^#(l, t) -> c_1(lessE^#(l, t, 0())) , 2: lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) , 3: if^#(true(), b, l, t, n) -> c_3() , 4: if^#(false(), true(), l, t, n) -> c_4() , 5: if^#(false(), false(), l, t, n) -> c_5(lessE^#(l, t, s(n))) , 6: le^#(0(), m) -> c_6() , 7: le^#(s(n), 0()) -> c_7() , 8: le^#(s(n), s(m)) -> c_8(le^#(n, m)) , 9: length^#(nil()) -> c_9() , 10: length^#(cons(n, l)) -> c_10(length^#(l)) , 11: toList^#(leaf()) -> c_11() , 12: toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) , 13: append^#(nil(), l2) -> c_13() , 14: append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) , 15: a^#() -> c_15() , 16: a^#() -> c_16() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { lessElements^#(l, t) -> c_1(lessE^#(l, t, 0())) , lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) , if^#(false(), false(), l, t, n) -> c_5(lessE^#(l, t, s(n))) , le^#(s(n), s(m)) -> c_8(le^#(n, m)) , length^#(cons(n, l)) -> c_10(length^#(l)) , toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) , append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) } Weak DPs: { if^#(true(), b, l, t, n) -> c_3() , if^#(false(), true(), l, t, n) -> c_4() , le^#(0(), m) -> c_6() , le^#(s(n), 0()) -> c_7() , length^#(nil()) -> c_9() , toList^#(leaf()) -> c_11() , append^#(nil(), l2) -> c_13() , a^#() -> c_15() , a^#() -> c_16() } Weak Trs: { lessElements(l, t) -> lessE(l, t, 0()) , lessE(l, t, n) -> if(le(length(l), n), le(length(toList(t)), n), l, t, n) , if(true(), b, l, t, n) -> l , if(false(), true(), l, t, n) -> t , if(false(), false(), l, t, n) -> lessE(l, t, s(n)) , le(0(), m) -> true() , le(s(n), 0()) -> false() , le(s(n), s(m)) -> le(n, m) , length(nil()) -> 0() , length(cons(n, l)) -> s(length(l)) , toList(leaf()) -> nil() , toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2))) , append(nil(), l2) -> l2 , append(cons(n, l1), l2) -> cons(n, append(l1, l2)) , a() -> c() , a() -> d() } 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. { if^#(true(), b, l, t, n) -> c_3() , if^#(false(), true(), l, t, n) -> c_4() , le^#(0(), m) -> c_6() , le^#(s(n), 0()) -> c_7() , length^#(nil()) -> c_9() , toList^#(leaf()) -> c_11() , append^#(nil(), l2) -> c_13() , a^#() -> c_15() , a^#() -> c_16() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { lessElements^#(l, t) -> c_1(lessE^#(l, t, 0())) , lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) , if^#(false(), false(), l, t, n) -> c_5(lessE^#(l, t, s(n))) , le^#(s(n), s(m)) -> c_8(le^#(n, m)) , length^#(cons(n, l)) -> c_10(length^#(l)) , toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) , append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) } Weak Trs: { lessElements(l, t) -> lessE(l, t, 0()) , lessE(l, t, n) -> if(le(length(l), n), le(length(toList(t)), n), l, t, n) , if(true(), b, l, t, n) -> l , if(false(), true(), l, t, n) -> t , if(false(), false(), l, t, n) -> lessE(l, t, s(n)) , le(0(), m) -> true() , le(s(n), 0()) -> false() , le(s(n), s(m)) -> le(n, m) , length(nil()) -> 0() , length(cons(n, l)) -> s(length(l)) , toList(leaf()) -> nil() , toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2))) , append(nil(), l2) -> l2 , append(cons(n, l1), l2) -> cons(n, append(l1, l2)) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: lessElements^#(l, t) -> c_1(lessE^#(l, t, 0())) -->_1 lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) :2 2: lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) -->_6 toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) :6 -->_5 length^#(cons(n, l)) -> c_10(length^#(l)) :5 -->_3 length^#(cons(n, l)) -> c_10(length^#(l)) :5 -->_4 le^#(s(n), s(m)) -> c_8(le^#(n, m)) :4 -->_2 le^#(s(n), s(m)) -> c_8(le^#(n, m)) :4 -->_1 if^#(false(), false(), l, t, n) -> c_5(lessE^#(l, t, s(n))) :3 3: if^#(false(), false(), l, t, n) -> c_5(lessE^#(l, t, s(n))) -->_1 lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) :2 4: le^#(s(n), s(m)) -> c_8(le^#(n, m)) -->_1 le^#(s(n), s(m)) -> c_8(le^#(n, m)) :4 5: length^#(cons(n, l)) -> c_10(length^#(l)) -->_1 length^#(cons(n, l)) -> c_10(length^#(l)) :5 6: toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) -->_1 append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) :7 -->_3 toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) :6 -->_2 toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) :6 7: append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) -->_1 append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) :7 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). { lessElements^#(l, t) -> c_1(lessE^#(l, t, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) , if^#(false(), false(), l, t, n) -> c_5(lessE^#(l, t, s(n))) , le^#(s(n), s(m)) -> c_8(le^#(n, m)) , length^#(cons(n, l)) -> c_10(length^#(l)) , toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) , append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) } Weak Trs: { lessElements(l, t) -> lessE(l, t, 0()) , lessE(l, t, n) -> if(le(length(l), n), le(length(toList(t)), n), l, t, n) , if(true(), b, l, t, n) -> l , if(false(), true(), l, t, n) -> t , if(false(), false(), l, t, n) -> lessE(l, t, s(n)) , le(0(), m) -> true() , le(s(n), 0()) -> false() , le(s(n), s(m)) -> le(n, m) , length(nil()) -> 0() , length(cons(n, l)) -> s(length(l)) , toList(leaf()) -> nil() , toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2))) , append(nil(), l2) -> l2 , append(cons(n, l1), l2) -> cons(n, append(l1, l2)) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { le(0(), m) -> true() , le(s(n), 0()) -> false() , le(s(n), s(m)) -> le(n, m) , length(nil()) -> 0() , length(cons(n, l)) -> s(length(l)) , toList(leaf()) -> nil() , toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2))) , append(nil(), l2) -> l2 , append(cons(n, l1), l2) -> cons(n, append(l1, l2)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { lessE^#(l, t, n) -> c_2(if^#(le(length(l), n), le(length(toList(t)), n), l, t, n), le^#(length(l), n), length^#(l), le^#(length(toList(t)), n), length^#(toList(t)), toList^#(t)) , if^#(false(), false(), l, t, n) -> c_5(lessE^#(l, t, s(n))) , le^#(s(n), s(m)) -> c_8(le^#(n, m)) , length^#(cons(n, l)) -> c_10(length^#(l)) , toList^#(node(t1, n, t2)) -> c_12(append^#(toList(t1), cons(n, toList(t2))), toList^#(t1), toList^#(t2)) , append^#(cons(n, l1), l2) -> c_14(append^#(l1, l2)) } Weak Trs: { le(0(), m) -> true() , le(s(n), 0()) -> false() , le(s(n), s(m)) -> le(n, m) , length(nil()) -> 0() , length(cons(n, l)) -> s(length(l)) , toList(leaf()) -> nil() , toList(node(t1, n, t2)) -> append(toList(t1), cons(n, toList(t2))) , append(nil(), l2) -> l2 , append(cons(n, l1), l2) -> cons(n, append(l1, l2)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..