YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) , main(x7) -> rec[fold_0][3](x7) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add the following dependency tuples: Strict DPs: { rec[fold_0][3]^#(Nil()) -> c_1() , rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) , insert_ord[2]^#(x6, Nil()) -> c_3() , insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(True(), x7, x5, x3) -> c_5() , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) , rec[leq_0][2]^#(0(), x18) -> c_7() , rec[leq_0][2]^#(S(x26), 0()) -> c_8() , rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) , main^#(x7) -> c_10(rec[fold_0][3]^#(x7)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { rec[fold_0][3]^#(Nil()) -> c_1() , rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) , insert_ord[2]^#(x6, Nil()) -> c_3() , insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(True(), x7, x5, x3) -> c_5() , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) , rec[leq_0][2]^#(0(), x18) -> c_7() , rec[leq_0][2]^#(S(x26), 0()) -> c_8() , rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) , main^#(x7) -> c_10(rec[fold_0][3]^#(x7)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) , main(x7) -> rec[fold_0][3](x7) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {1,3,5,7,8} by applications of Pre({1,3,5,7,8}) = {2,4,6,9,10}. Here rules are labeled as follows: DPs: { 1: rec[fold_0][3]^#(Nil()) -> c_1() , 2: rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) , 3: insert_ord[2]^#(x6, Nil()) -> c_3() , 4: insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , 5: insert_cond_1^#(True(), x7, x5, x3) -> c_5() , 6: insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) , 7: rec[leq_0][2]^#(0(), x18) -> c_7() , 8: rec[leq_0][2]^#(S(x26), 0()) -> c_8() , 9: rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) , 10: main^#(x7) -> c_10(rec[fold_0][3]^#(x7)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) , insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) , rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) , main^#(x7) -> c_10(rec[fold_0][3]^#(x7)) } Weak DPs: { rec[fold_0][3]^#(Nil()) -> c_1() , insert_ord[2]^#(x6, Nil()) -> c_3() , insert_cond_1^#(True(), x7, x5, x3) -> c_5() , rec[leq_0][2]^#(0(), x18) -> c_7() , rec[leq_0][2]^#(S(x26), 0()) -> c_8() } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) , main(x7) -> rec[fold_0][3](x7) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { rec[fold_0][3]^#(Nil()) -> c_1() , insert_ord[2]^#(x6, Nil()) -> c_3() , insert_cond_1^#(True(), x7, x5, x3) -> c_5() , rec[leq_0][2]^#(0(), x18) -> c_7() , rec[leq_0][2]^#(S(x26), 0()) -> c_8() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) , insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) , rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) , main^#(x7) -> c_10(rec[fold_0][3]^#(x7)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) , main(x7) -> rec[fold_0][3](x7) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Consider the dependency graph 1: rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) -->_1 insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) :2 -->_2 rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) :1 2: insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) -->_2 rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) :4 -->_1 insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) :3 3: insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) -->_1 insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) :2 4: rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) -->_1 rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) :4 5: main^#(x7) -> c_10(rec[fold_0][3]^#(x7)) -->_1 rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) :1 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). { main^#(x7) -> c_10(rec[fold_0][3]^#(x7)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) , insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) , rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) , main(x7) -> rec[fold_0][3](x7) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) , insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) , rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We decompose the input problem according to the dependency graph into the upper component { rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) } and lower component { insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) , rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) } Further, following extension rules are added to the lower component. { rec[fold_0][3]^#(Cons(x2, x1)) -> rec[fold_0][3]^#(x1) , rec[fold_0][3]^#(Cons(x2, x1)) -> insert_ord[2]^#(x2, rec[fold_0][3](x1)) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. DPs: { 1: rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) } Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(Nil) = {}, safe(rec[fold_0][3]) = {}, safe(Cons) = {1, 2}, safe(insert_ord[2]) = {}, safe(True) = {}, safe(insert_cond_1) = {2, 3, 4}, safe(False) = {}, safe(rec[leq_0][2]) = {1}, safe(0) = {}, safe(S) = {1}, safe(main) = {}, safe(rec[fold_0][3]^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(insert_ord[2]^#) = {}, safe(c_3) = {}, safe(c_4) = {}, safe(insert_cond_1^#) = {}, safe(rec[leq_0][2]^#) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(c_7) = {}, safe(c_8) = {}, safe(c_9) = {}, safe(main^#) = {}, safe(c_10) = {} and precedence rec[fold_0][3] > rec[leq_0][2], insert_cond_1 > rec[leq_0][2], rec[fold_0][3]^# > insert_ord[2], rec[fold_0][3]^# > insert_cond_1, rec[fold_0][3]^# > rec[leq_0][2], rec[fold_0][3] ~ insert_cond_1, insert_ord[2] ~ rec[leq_0][2] . Following symbols are considered recursive: {rec[fold_0][3]^#} The recursion depth is 1. Further, following argument filtering is employed: pi(Nil) = [], pi(rec[fold_0][3]) = [], pi(Cons) = [2], pi(insert_ord[2]) = 1, pi(True) = [], pi(insert_cond_1) = [1, 2, 3, 4], pi(False) = [], pi(rec[leq_0][2]) = [1, 2], pi(0) = [], pi(S) = [], pi(main) = [], pi(rec[fold_0][3]^#) = [1], pi(c_1) = [], pi(c_2) = [1, 2], pi(insert_ord[2]^#) = [], pi(c_3) = [], pi(c_4) = [], pi(insert_cond_1^#) = [], pi(rec[leq_0][2]^#) = [], pi(c_5) = [], pi(c_6) = [], pi(c_7) = [], pi(c_8) = [], pi(c_9) = [], pi(main^#) = [], pi(c_10) = [] Usable defined function symbols are a subset of: {rec[fold_0][3]^#, insert_ord[2]^#, insert_cond_1^#, rec[leq_0][2]^#, main^#} For your convenience, here are the satisfied ordering constraints: pi(rec[fold_0][3]^#(Cons(x2, x1))) = rec[fold_0][3]^#(Cons(; x1);) > c_2(insert_ord[2]^#(), rec[fold_0][3]^#(x1;);) = pi(c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1))) The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { rec[fold_0][3]^#(Cons(x2, x1)) -> c_2(insert_ord[2]^#(x2, rec[fold_0][3](x1)), rec[fold_0][3]^#(x1)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) , rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) } Weak DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> rec[fold_0][3]^#(x1) , rec[fold_0][3]^#(Cons(x2, x1)) -> insert_ord[2]^#(x2, rec[fold_0][3](x1)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 3: rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) , 5: rec[fold_0][3]^#(Cons(x2, x1)) -> insert_ord[2]^#(x2, rec[fold_0][3](x1)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_4) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_9) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [Nil] = [0] [rec[fold_0][3]](x1) = [1] x1 + [0] [Cons](x1, x2) = [1] x1 + [1] x2 + [0] [insert_ord[2]](x1, x2) = [1] x1 + [1] x2 + [0] [True] = [0] [insert_cond_1](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] x4 + [0] [False] = [0] [rec[leq_0][2]](x1, x2) = [0] [0] = [0] [S](x1) = [1] x1 + [4] [main](x1) = [7] x1 + [0] [rec[fold_0][3]^#](x1) = [4] x1 + [5] [c_1] = [0] [c_2](x1, x2) = [7] x1 + [7] x2 + [0] [insert_ord[2]^#](x1, x2) = [4] x2 + [0] [c_3] = [0] [c_4](x1, x2) = [1] x1 + [2] x2 + [0] [insert_cond_1^#](x1, x2, x3, x4) = [4] x4 + [0] [rec[leq_0][2]^#](x1, x2) = [2] x2 + [0] [c_5] = [0] [c_6](x1) = [1] x1 + [0] [c_7] = [0] [c_8] = [0] [c_9](x1) = [1] x1 + [1] [main^#](x1) = [7] x1 + [0] [c_10](x1) = [7] x1 + [0] The following symbols are considered usable {rec[fold_0][3], insert_ord[2], insert_cond_1, rec[leq_0][2], rec[fold_0][3]^#, insert_ord[2]^#, insert_cond_1^#, rec[leq_0][2]^#} The order satisfies the following ordering constraints: [rec[fold_0][3](Nil())] = [0] >= [0] = [Nil()] [rec[fold_0][3](Cons(x2, x1))] = [1] x2 + [1] x1 + [0] >= [1] x2 + [1] x1 + [0] = [insert_ord[2](x2, rec[fold_0][3](x1))] [insert_ord[2](x6, Nil())] = [1] x6 + [0] >= [1] x6 + [0] = [Cons(x6, Nil())] [insert_ord[2](x14, Cons(x10, x6))] = [1] x6 + [1] x14 + [1] x10 + [0] >= [1] x6 + [1] x14 + [1] x10 + [0] = [insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6)] [insert_cond_1(True(), x7, x5, x3)] = [1] x7 + [1] x5 + [1] x3 + [0] >= [1] x7 + [1] x5 + [1] x3 + [0] = [Cons(x7, Cons(x5, x3))] [insert_cond_1(False(), x4, x11, x8)] = [1] x4 + [1] x11 + [1] x8 + [0] >= [1] x4 + [1] x11 + [1] x8 + [0] = [Cons(x11, insert_ord[2](x4, x8))] [rec[leq_0][2](0(), x18)] = [0] >= [0] = [True()] [rec[leq_0][2](S(x26), 0())] = [0] >= [0] = [False()] [rec[leq_0][2](S(x10), S(x6))] = [0] >= [0] = [rec[leq_0][2](x10, x6)] [rec[fold_0][3]^#(Cons(x2, x1))] = [4] x2 + [4] x1 + [5] >= [4] x1 + [5] = [rec[fold_0][3]^#(x1)] [rec[fold_0][3]^#(Cons(x2, x1))] = [4] x2 + [4] x1 + [5] > [4] x1 + [0] = [insert_ord[2]^#(x2, rec[fold_0][3](x1))] [insert_ord[2]^#(x14, Cons(x10, x6))] = [4] x6 + [4] x10 + [0] >= [4] x6 + [4] x10 + [0] = [c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10))] [insert_cond_1^#(False(), x4, x11, x8)] = [4] x8 + [0] >= [4] x8 + [0] = [c_6(insert_ord[2]^#(x4, x8))] [rec[leq_0][2]^#(S(x10), S(x6))] = [2] x6 + [8] > [2] x6 + [1] = [c_9(rec[leq_0][2]^#(x10, x6))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) } Weak DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> rec[fold_0][3]^#(x1) , rec[fold_0][3]^#(Cons(x2, x1)) -> insert_ord[2]^#(x2, rec[fold_0][3](x1)) , rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { rec[leq_0][2]^#(S(x10), S(x6)) -> c_9(rec[leq_0][2]^#(x10, x6)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) , insert_cond_1^#(False(), x4, x11, x8) -> c_6(insert_ord[2]^#(x4, x8)) } Weak DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> rec[fold_0][3]^#(x1) , rec[fold_0][3]^#(Cons(x2, x1)) -> insert_ord[2]^#(x2, rec[fold_0][3](x1)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { insert_ord[2]^#(x14, Cons(x10, x6)) -> c_4(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6), rec[leq_0][2]^#(x14, x10)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { insert_ord[2]^#(x14, Cons(x10, x6)) -> c_1(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6)) , insert_cond_1^#(False(), x4, x11, x8) -> c_2(insert_ord[2]^#(x4, x8)) } Weak DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> c_3(rec[fold_0][3]^#(x1)) , rec[fold_0][3]^#(Cons(x2, x1)) -> c_4(insert_ord[2]^#(x2, rec[fold_0][3](x1))) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: insert_cond_1^#(False(), x4, x11, x8) -> c_2(insert_ord[2]^#(x4, x8)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [Nil] = [0] [rec[fold_0][3]](x1) = [1] x1 + [0] [Cons](x1, x2) = [1] x1 + [1] x2 + [0] [insert_ord[2]](x1, x2) = [1] x1 + [1] x2 + [0] [True] = [0] [insert_cond_1](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] x4 + [0] [False] = [4] [rec[leq_0][2]](x1, x2) = [1] x2 + [0] [0] = [4] [S](x1) = [1] x1 + [0] [main](x1) = [7] x1 + [0] [rec[fold_0][3]^#](x1) = [4] x1 + [0] [c_1] = [0] [c_2](x1, x2) = [7] x1 + [7] x2 + [0] [insert_ord[2]^#](x1, x2) = [1] x2 + [0] [c_3] = [0] [c_4](x1, x2) = [7] x1 + [7] x2 + [0] [insert_cond_1^#](x1, x2, x3, x4) = [1] x1 + [1] x4 + [0] [rec[leq_0][2]^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_5] = [0] [c_6](x1) = [7] x1 + [0] [c_7] = [0] [c_8] = [0] [c_9](x1) = [7] x1 + [0] [main^#](x1) = [7] x1 + [0] [c_10](x1) = [7] x1 + [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [1] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [1] x1 + [0] The following symbols are considered usable {rec[fold_0][3], insert_ord[2], insert_cond_1, rec[leq_0][2], rec[fold_0][3]^#, insert_ord[2]^#, insert_cond_1^#} The order satisfies the following ordering constraints: [rec[fold_0][3](Nil())] = [0] >= [0] = [Nil()] [rec[fold_0][3](Cons(x2, x1))] = [1] x2 + [1] x1 + [0] >= [1] x2 + [1] x1 + [0] = [insert_ord[2](x2, rec[fold_0][3](x1))] [insert_ord[2](x6, Nil())] = [1] x6 + [0] >= [1] x6 + [0] = [Cons(x6, Nil())] [insert_ord[2](x14, Cons(x10, x6))] = [1] x6 + [1] x14 + [1] x10 + [0] >= [1] x6 + [1] x14 + [1] x10 + [0] = [insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6)] [insert_cond_1(True(), x7, x5, x3)] = [1] x7 + [1] x5 + [1] x3 + [0] >= [1] x7 + [1] x5 + [1] x3 + [0] = [Cons(x7, Cons(x5, x3))] [insert_cond_1(False(), x4, x11, x8)] = [1] x4 + [1] x11 + [1] x8 + [0] >= [1] x4 + [1] x11 + [1] x8 + [0] = [Cons(x11, insert_ord[2](x4, x8))] [rec[leq_0][2](0(), x18)] = [1] x18 + [0] >= [0] = [True()] [rec[leq_0][2](S(x26), 0())] = [4] >= [4] = [False()] [rec[leq_0][2](S(x10), S(x6))] = [1] x6 + [0] >= [1] x6 + [0] = [rec[leq_0][2](x10, x6)] [rec[fold_0][3]^#(Cons(x2, x1))] = [4] x2 + [4] x1 + [0] >= [4] x1 + [0] = [c_3(rec[fold_0][3]^#(x1))] [rec[fold_0][3]^#(Cons(x2, x1))] = [4] x2 + [4] x1 + [0] >= [1] x1 + [0] = [c_4(insert_ord[2]^#(x2, rec[fold_0][3](x1)))] [insert_ord[2]^#(x14, Cons(x10, x6))] = [1] x6 + [1] x10 + [0] >= [1] x6 + [1] x10 + [0] = [c_1(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6))] [insert_cond_1^#(False(), x4, x11, x8)] = [1] x8 + [4] > [1] x8 + [1] = [c_2(insert_ord[2]^#(x4, x8))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { insert_ord[2]^#(x14, Cons(x10, x6)) -> c_1(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6)) } Weak DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> c_3(rec[fold_0][3]^#(x1)) , rec[fold_0][3]^#(Cons(x2, x1)) -> c_4(insert_ord[2]^#(x2, rec[fold_0][3](x1))) , insert_cond_1^#(False(), x4, x11, x8) -> c_2(insert_ord[2]^#(x4, x8)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: insert_ord[2]^#(x14, Cons(x10, x6)) -> c_1(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6)) , 2: rec[fold_0][3]^#(Cons(x2, x1)) -> c_3(rec[fold_0][3]^#(x1)) , 3: rec[fold_0][3]^#(Cons(x2, x1)) -> c_4(insert_ord[2]^#(x2, rec[fold_0][3](x1))) , 4: insert_cond_1^#(False(), x4, x11, x8) -> c_2(insert_ord[2]^#(x4, x8)) } Trs: { rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [Nil] = [0] [rec[fold_0][3]](x1) = [1] x1 + [0] [Cons](x1, x2) = [1] x2 + [3] [insert_ord[2]](x1, x2) = [1] x2 + [3] [True] = [0] [insert_cond_1](x1, x2, x3, x4) = [1] x4 + [6] [False] = [3] [rec[leq_0][2]](x1, x2) = [4] [0] = [0] [S](x1) = [1] x1 + [0] [main](x1) = [7] x1 + [0] [rec[fold_0][3]^#](x1) = [4] x1 + [0] [c_1] = [0] [c_2](x1, x2) = [7] x1 + [7] x2 + [0] [insert_ord[2]^#](x1, x2) = [3] x2 + [0] [c_3] = [0] [c_4](x1, x2) = [7] x1 + [7] x2 + [0] [insert_cond_1^#](x1, x2, x3, x4) = [1] x1 + [3] x4 + [1] [rec[leq_0][2]^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_5] = [0] [c_6](x1) = [7] x1 + [0] [c_7] = [0] [c_8] = [0] [c_9](x1) = [7] x1 + [0] [main^#](x1) = [7] x1 + [0] [c_10](x1) = [7] x1 + [0] [c] = [0] [c_1](x1) = [1] x1 + [1] [c_2](x1) = [1] x1 + [3] [c_3](x1) = [1] x1 + [5] [c_4](x1) = [1] x1 + [3] The following symbols are considered usable {rec[fold_0][3], insert_ord[2], insert_cond_1, rec[leq_0][2], rec[fold_0][3]^#, insert_ord[2]^#, insert_cond_1^#} The order satisfies the following ordering constraints: [rec[fold_0][3](Nil())] = [0] >= [0] = [Nil()] [rec[fold_0][3](Cons(x2, x1))] = [1] x1 + [3] >= [1] x1 + [3] = [insert_ord[2](x2, rec[fold_0][3](x1))] [insert_ord[2](x6, Nil())] = [3] >= [3] = [Cons(x6, Nil())] [insert_ord[2](x14, Cons(x10, x6))] = [1] x6 + [6] >= [1] x6 + [6] = [insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6)] [insert_cond_1(True(), x7, x5, x3)] = [1] x3 + [6] >= [1] x3 + [6] = [Cons(x7, Cons(x5, x3))] [insert_cond_1(False(), x4, x11, x8)] = [1] x8 + [6] >= [1] x8 + [6] = [Cons(x11, insert_ord[2](x4, x8))] [rec[leq_0][2](0(), x18)] = [4] > [0] = [True()] [rec[leq_0][2](S(x26), 0())] = [4] > [3] = [False()] [rec[leq_0][2](S(x10), S(x6))] = [4] >= [4] = [rec[leq_0][2](x10, x6)] [rec[fold_0][3]^#(Cons(x2, x1))] = [4] x1 + [12] > [4] x1 + [5] = [c_3(rec[fold_0][3]^#(x1))] [rec[fold_0][3]^#(Cons(x2, x1))] = [4] x1 + [12] > [3] x1 + [3] = [c_4(insert_ord[2]^#(x2, rec[fold_0][3](x1)))] [insert_ord[2]^#(x14, Cons(x10, x6))] = [3] x6 + [9] > [3] x6 + [6] = [c_1(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6))] [insert_cond_1^#(False(), x4, x11, x8)] = [3] x8 + [4] > [3] x8 + [3] = [c_2(insert_ord[2]^#(x4, x8))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { rec[fold_0][3]^#(Cons(x2, x1)) -> c_3(rec[fold_0][3]^#(x1)) , rec[fold_0][3]^#(Cons(x2, x1)) -> c_4(insert_ord[2]^#(x2, rec[fold_0][3](x1))) , insert_ord[2]^#(x14, Cons(x10, x6)) -> c_1(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6)) , insert_cond_1^#(False(), x4, x11, x8) -> c_2(insert_ord[2]^#(x4, x8)) } Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { rec[fold_0][3]^#(Cons(x2, x1)) -> c_3(rec[fold_0][3]^#(x1)) , rec[fold_0][3]^#(Cons(x2, x1)) -> c_4(insert_ord[2]^#(x2, rec[fold_0][3](x1))) , insert_ord[2]^#(x14, Cons(x10, x6)) -> c_1(insert_cond_1^#(rec[leq_0][2](x14, x10), x14, x10, x6)) , insert_cond_1^#(False(), x4, x11, x8) -> c_2(insert_ord[2]^#(x4, x8)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { rec[fold_0][3](Nil()) -> Nil() , rec[fold_0][3](Cons(x2, x1)) -> insert_ord[2](x2, rec[fold_0][3](x1)) , insert_ord[2](x6, Nil()) -> Cons(x6, Nil()) , insert_ord[2](x14, Cons(x10, x6)) -> insert_cond_1(rec[leq_0][2](x14, x10), x14, x10, x6) , insert_cond_1(True(), x7, x5, x3) -> Cons(x7, Cons(x5, x3)) , insert_cond_1(False(), x4, x11, x8) -> Cons(x11, insert_ord[2](x4, x8)) , rec[leq_0][2](0(), x18) -> True() , rec[leq_0][2](S(x26), 0()) -> False() , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))