YES(O(1),O(n^3)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^3)). Strict Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , shuffle(nil()) -> nil() , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) , less_leaves(x, leaf()) -> false() , less_leaves(leaf(), cons(w, z)) -> true() , less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^3)) We add the following dependency tuples: Strict DPs: { minus^#(x, 0()) -> c_1() , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(0(), s(y)) -> c_3() , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , app^#(nil(), y) -> c_5() , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(nil()) -> c_7() , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(nil()) -> c_9() , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) , concat^#(leaf(), y) -> c_11() , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) , less_leaves^#(x, leaf()) -> c_13() , less_leaves^#(leaf(), cons(w, z)) -> c_14() , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^3)). Strict DPs: { minus^#(x, 0()) -> c_1() , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(0(), s(y)) -> c_3() , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , app^#(nil(), y) -> c_5() , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(nil()) -> c_7() , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(nil()) -> c_9() , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) , concat^#(leaf(), y) -> c_11() , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) , less_leaves^#(x, leaf()) -> c_13() , less_leaves^#(leaf(), cons(w, z)) -> c_14() , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , shuffle(nil()) -> nil() , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) , less_leaves(x, leaf()) -> false() , less_leaves(leaf(), cons(w, z)) -> true() , less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^3)) We estimate the number of application of {1,3,5,7,9,11,13,14} by applications of Pre({1,3,5,7,9,11,13,14}) = {2,4,6,8,10,12,15}. Here rules are labeled as follows: DPs: { 1: minus^#(x, 0()) -> c_1() , 2: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , 3: quot^#(0(), s(y)) -> c_3() , 4: quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , 5: app^#(nil(), y) -> c_5() , 6: app^#(add(n, x), y) -> c_6(app^#(x, y)) , 7: reverse^#(nil()) -> c_7() , 8: reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , 9: shuffle^#(nil()) -> c_9() , 10: shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) , 11: concat^#(leaf(), y) -> c_11() , 12: concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) , 13: less_leaves^#(x, leaf()) -> c_13() , 14: less_leaves^#(leaf(), cons(w, z)) -> c_14() , 15: less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^3)). Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z)) } Weak DPs: { minus^#(x, 0()) -> c_1() , quot^#(0(), s(y)) -> c_3() , app^#(nil(), y) -> c_5() , reverse^#(nil()) -> c_7() , shuffle^#(nil()) -> c_9() , concat^#(leaf(), y) -> c_11() , less_leaves^#(x, leaf()) -> c_13() , less_leaves^#(leaf(), cons(w, z)) -> c_14() } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , shuffle(nil()) -> nil() , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) , less_leaves(x, leaf()) -> false() , less_leaves(leaf(), cons(w, z)) -> true() , less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^3)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { minus^#(x, 0()) -> c_1() , quot^#(0(), s(y)) -> c_3() , app^#(nil(), y) -> c_5() , reverse^#(nil()) -> c_7() , shuffle^#(nil()) -> c_9() , concat^#(leaf(), y) -> c_11() , less_leaves^#(x, leaf()) -> c_13() , less_leaves^#(leaf(), cons(w, z)) -> c_14() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^3)). Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , shuffle(nil()) -> nil() , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) , less_leaves(x, leaf()) -> false() , less_leaves(leaf(), cons(w, z)) -> true() , less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^3)) We replace rewrite rules by usable rules: Weak Usable Rules: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^3)). Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^3)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. DPs: { 6: concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) , 7: less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z)) } Trs: { minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_2) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_8) = {1, 2}, Uargs(c_10) = {1, 2}, Uargs(c_12) = {1}, Uargs(c_15) = {1, 2, 3} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [minus](x1, x2) = [1 1] x1 + [0 0] x2 + [0] [2 2] [0 4] [0] [0] = [0] [0] [s](x1) = [0 0] x1 + [4] [1 1] [0] [quot](x1, x2) = [7 7] x1 + [7 7] x2 + [0] [0 0] [0 0] [0] [app](x1, x2) = [2 0] x2 + [1] [0 1] [0] [nil] = [0] [0] [add](x1, x2) = [1] [0] [reverse](x1) = [4] [0] [shuffle](x1) = [7 7] x1 + [0] [0 0] [0] [concat](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [2 0] [0 4] [4] [leaf] = [0] [0] [cons](x1, x2) = [1 1] x1 + [1 0] x2 + [2] [0 0] [0 1] [4] [less_leaves](x1, x2) = [7 7] x1 + [7 7] x2 + [0] [0 0] [0 0] [0] [false] = [0] [0] [true] = [0] [0] [minus^#](x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 4] [0 4] [4] [c_1] = [0] [0] [c_2](x1) = [4 0] x1 + [0] [0 0] [3] [quot^#](x1, x2) = [0 0] x1 + [0] [2 4] [0] [c_3] = [0] [0] [c_4](x1, x2) = [2 0] x1 + [4 0] x2 + [0] [0 0] [0 0] [7] [app^#](x1, x2) = [0 0] x1 + [0] [2 0] [6] [c_5] = [0] [0] [c_6](x1) = [4 0] x1 + [0] [0 0] [7] [reverse^#](x1) = [0 0] x1 + [0] [6 0] [2] [c_7] = [0] [0] [c_8](x1, x2) = [1 0] x1 + [4 0] x2 + [0] [0 0] [0 0] [3] [shuffle^#](x1) = [0] [4] [c_9] = [0] [0] [c_10](x1, x2) = [4 0] x1 + [4 0] x2 + [0] [0 0] [0 0] [3] [concat^#](x1, x2) = [0 1] x1 + [0 0] x2 + [0] [0 0] [0 4] [0] [c_11] = [0] [0] [c_12](x1) = [1 0] x1 + [1] [0 0] [0] [less_leaves^#](x1, x2) = [4 0] x1 + [2 0] x2 + [0] [0 0] [0 0] [4] [c_13] = [0] [0] [c_14] = [0] [0] [c_15](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [2 0] x3 + [3] [0 0] [0 0] [0 0] [3] The following symbols are considered usable {minus, app, reverse, concat, minus^#, quot^#, app^#, reverse^#, shuffle^#, concat^#, less_leaves^#} The order satisfies the following ordering constraints: [minus(x, 0())] = [1 1] x + [0] [2 2] [0] >= [1 0] x + [0] [0 1] [0] = [x] [minus(s(x), s(y))] = [1 1] x + [0 0] y + [4] [2 2] [4 4] [8] > [1 1] x + [0 0] y + [0] [2 2] [0 4] [0] = [minus(x, y)] [app(nil(), y)] = [2 0] y + [1] [0 1] [0] > [1 0] y + [0] [0 1] [0] = [y] [app(add(n, x), y)] = [2 0] y + [1] [0 1] [0] >= [1] [0] = [add(n, app(x, y))] [reverse(nil())] = [4] [0] > [0] [0] = [nil()] [reverse(add(n, x))] = [4] [0] > [3] [0] = [app(reverse(x), add(n, nil()))] [concat(leaf(), y)] = [1 0] y + [0] [0 4] [4] >= [1 0] y + [0] [0 1] [0] = [y] [concat(cons(u, v), y)] = [1 0] y + [1 1] u + [1 0] v + [2] [0 4] [2 2] [2 0] [8] >= [1 0] y + [1 1] u + [1 0] v + [2] [0 4] [0 0] [2 0] [8] = [cons(u, concat(v, y))] [minus^#(s(x), s(y))] = [0 0] x + [0 0] y + [0] [4 4] [4 4] [4] >= [0] [3] = [c_2(minus^#(x, y))] [quot^#(s(x), s(y))] = [0 0] x + [0] [4 4] [8] >= [0] [7] = [c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))] [app^#(add(n, x), y)] = [0] [8] >= [0] [7] = [c_6(app^#(x, y))] [reverse^#(add(n, x))] = [0] [8] >= [0] [3] = [c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))] [shuffle^#(add(n, x))] = [0] [4] >= [0] [3] = [c_10(shuffle^#(reverse(x)), reverse^#(x))] [concat^#(cons(u, v), y)] = [0 0] y + [0 1] v + [4] [0 4] [0 0] [0] > [0 1] v + [1] [0 0] [0] = [c_12(concat^#(v, y))] [less_leaves^#(cons(u, v), cons(w, z))] = [4 4] u + [4 0] v + [2 2] w + [2 0] z + [12] [0 0] [0 0] [0 0] [0 0] [4] > [4 1] u + [4 0] v + [2 2] w + [2 0] z + [3] [0 0] [0 0] [0 0] [0 0] [3] = [c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z))] 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^3)). Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) } Weak DPs: { concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^3)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z)), concat^#(u, v), concat^#(w, z)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^3)). Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^3)) We replace rewrite rules by usable rules: Weak Usable Rules: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^3)). Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^3)) We decompose the input problem according to the dependency graph into the upper component { quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) } and lower component { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) } Further, following extension rules are added to the lower component. { quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 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: { quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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: quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_4) = {1}, Uargs(c_10) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [minus](x1, x2) = [1] x1 + [1] [0] = [7] [s](x1) = [1] x1 + [4] [quot](x1, x2) = [7] x1 + [7] x2 + [0] [app](x1, x2) = [1] x2 + [1] [nil] = [0] [add](x1, x2) = [1] [reverse](x1) = [4] x1 + [4] [shuffle](x1) = [7] x1 + [0] [concat](x1, x2) = [7] x1 + [7] x2 + [0] [leaf] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0] [false] = [0] [true] = [0] [minus^#](x1, x2) = [7] x1 + [7] x2 + [7] [c_1] = [0] [c_2](x1) = [7] x1 + [0] [quot^#](x1, x2) = [1] x1 + [0] [c_3] = [0] [c_4](x1, x2) = [1] x1 + [1] [app^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_5] = [0] [c_6](x1) = [7] x1 + [0] [reverse^#](x1) = [7] x1 + [7] [c_7] = [0] [c_8](x1, x2) = [7] x1 + [7] x2 + [0] [shuffle^#](x1) = [0] [c_9] = [0] [c_10](x1, x2) = [1] x1 + [0] [concat^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_11] = [0] [c_12](x1) = [7] x1 + [0] [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_13] = [0] [c_14] = [0] [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] The following symbols are considered usable {minus, app, reverse, quot^#, shuffle^#} The order satisfies the following ordering constraints: [minus(x, 0())] = [1] x + [1] > [1] x + [0] = [x] [minus(s(x), s(y))] = [1] x + [5] > [1] x + [1] = [minus(x, y)] [app(nil(), y)] = [1] y + [1] > [1] y + [0] = [y] [app(add(n, x), y)] = [1] y + [1] >= [1] = [add(n, app(x, y))] [reverse(nil())] = [4] > [0] = [nil()] [reverse(add(n, x))] = [8] > [2] = [app(reverse(x), add(n, nil()))] [quot^#(s(x), s(y))] = [1] x + [4] > [1] x + [2] = [c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))] [shuffle^#(add(n, x))] = [0] >= [0] = [c_10(shuffle^#(reverse(x)), reverse^#(x))] 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: { shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) } Weak DPs: { quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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. { quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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: { shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We replace rewrite rules by usable rules: Weak Usable Rules: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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: shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [minus](x1, x2) = [7] x1 + [7] x2 + [0] [0] = [0] [s](x1) = [1] x1 + [0] [quot](x1, x2) = [7] x1 + [7] x2 + [0] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [add](x1, x2) = [1] x1 + [1] x2 + [1] [reverse](x1) = [1] x1 + [0] [shuffle](x1) = [7] x1 + [0] [concat](x1, x2) = [7] x1 + [7] x2 + [0] [leaf] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0] [false] = [0] [true] = [0] [minus^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_1] = [0] [c_2](x1) = [7] x1 + [0] [quot^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_3] = [0] [c_4](x1, x2) = [7] x1 + [7] x2 + [0] [app^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_5] = [0] [c_6](x1) = [7] x1 + [0] [reverse^#](x1) = [7] x1 + [0] [c_7] = [0] [c_8](x1, x2) = [7] x1 + [7] x2 + [0] [shuffle^#](x1) = [1] x1 + [0] [c_9] = [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [concat^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_11] = [0] [c_12](x1) = [7] x1 + [0] [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_13] = [0] [c_14] = [0] [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c] = [0] [c_1](x1) = [1] x1 + [0] The following symbols are considered usable {app, reverse, shuffle^#} The order satisfies the following ordering constraints: [app(nil(), y)] = [1] y + [0] >= [1] y + [0] = [y] [app(add(n, x), y)] = [1] x + [1] y + [1] n + [1] >= [1] x + [1] y + [1] n + [1] = [add(n, app(x, y))] [reverse(nil())] = [0] >= [0] = [nil()] [reverse(add(n, x))] = [1] x + [1] n + [1] >= [1] x + [1] n + [1] = [app(reverse(x), add(n, nil()))] [shuffle^#(add(n, x))] = [1] x + [1] n + [1] > [1] x + [0] = [c_1(shuffle^#(reverse(x)))] 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: { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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. { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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^2)). Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) } Weak DPs: { quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , 4: quot^#(s(x), s(y)) -> minus^#(x, y) , 5: quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } Trs: { minus(s(x), s(y)) -> minus(x, y) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_2) = {1}, Uargs(c_6) = {1}, Uargs(c_8) = {1, 2} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [minus](x1, x2) = [1] x1 + [0] [0] = [7] [s](x1) = [1] x1 + [2] [quot](x1, x2) = [7] x1 + [7] x2 + [0] [app](x1, x2) = [4] x2 + [0] [nil] = [0] [add](x1, x2) = [0] [reverse](x1) = [0] [shuffle](x1) = [7] x1 + [0] [concat](x1, x2) = [7] x1 + [7] x2 + [0] [leaf] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0] [false] = [0] [true] = [0] [minus^#](x1, x2) = [4] x1 + [0] [c_1] = [0] [c_2](x1) = [1] x1 + [5] [quot^#](x1, x2) = [4] x1 + [0] [c_3] = [0] [c_4](x1, x2) = [7] x1 + [7] x2 + [0] [app^#](x1, x2) = [0] [c_5] = [0] [c_6](x1) = [2] x1 + [0] [reverse^#](x1) = [0] [c_7] = [0] [c_8](x1, x2) = [4] x1 + [1] x2 + [0] [shuffle^#](x1) = [0] [c_9] = [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [concat^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_11] = [0] [c_12](x1) = [7] x1 + [0] [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_13] = [0] [c_14] = [0] [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] The following symbols are considered usable {minus, app, reverse, minus^#, quot^#, app^#, reverse^#, shuffle^#} The order satisfies the following ordering constraints: [minus(x, 0())] = [1] x + [0] >= [1] x + [0] = [x] [minus(s(x), s(y))] = [1] x + [2] > [1] x + [0] = [minus(x, y)] [app(nil(), y)] = [4] y + [0] >= [1] y + [0] = [y] [app(add(n, x), y)] = [4] y + [0] >= [0] = [add(n, app(x, y))] [reverse(nil())] = [0] >= [0] = [nil()] [reverse(add(n, x))] = [0] >= [0] = [app(reverse(x), add(n, nil()))] [minus^#(s(x), s(y))] = [4] x + [8] > [4] x + [5] = [c_2(minus^#(x, y))] [quot^#(s(x), s(y))] = [4] x + [8] > [4] x + [0] = [minus^#(x, y)] [quot^#(s(x), s(y))] = [4] x + [8] > [4] x + [0] = [quot^#(minus(x, y), s(y))] [app^#(add(n, x), y)] = [0] >= [0] = [c_6(app^#(x, y))] [reverse^#(add(n, x))] = [0] >= [0] = [c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))] [shuffle^#(add(n, x))] = [0] >= [0] = [reverse^#(x)] [shuffle^#(add(n, x))] = [0] >= [0] = [shuffle^#(reverse(x))] 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^2)). Strict DPs: { app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) } Weak DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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. { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(s(x), s(y)) -> minus^#(x, y) , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) } Weak DPs: { shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Weak Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) } Weak DPs: { shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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 { reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } and lower component { app^#(add(n, x), y) -> c_6(app^#(x, y)) } Further, following extension rules are added to the lower component. { reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil())) , reverse^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 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: { reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) } Weak DPs: { shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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: reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , 2: shuffle^#(add(n, x)) -> reverse^#(x) , 3: shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_8) = {1, 2} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [minus](x1, x2) = [7] x1 + [7] x2 + [0] [0] = [0] [s](x1) = [1] x1 + [0] [quot](x1, x2) = [7] x1 + [7] x2 + [0] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [add](x1, x2) = [1] x1 + [1] x2 + [1] [reverse](x1) = [1] x1 + [0] [shuffle](x1) = [7] x1 + [0] [concat](x1, x2) = [7] x1 + [7] x2 + [0] [leaf] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0] [false] = [0] [true] = [0] [minus^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_1] = [0] [c_2](x1) = [7] x1 + [0] [quot^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_3] = [0] [c_4](x1, x2) = [7] x1 + [7] x2 + [0] [app^#](x1, x2) = [0] [c_5] = [0] [c_6](x1) = [7] x1 + [0] [reverse^#](x1) = [1] x1 + [0] [c_7] = [0] [c_8](x1, x2) = [4] x1 + [1] x2 + [0] [shuffle^#](x1) = [1] x1 + [7] [c_9] = [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [concat^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_11] = [0] [c_12](x1) = [7] x1 + [0] [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_13] = [0] [c_14] = [0] [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] The following symbols are considered usable {app, reverse, reverse^#, shuffle^#} The order satisfies the following ordering constraints: [app(nil(), y)] = [1] y + [0] >= [1] y + [0] = [y] [app(add(n, x), y)] = [1] x + [1] y + [1] n + [1] >= [1] x + [1] y + [1] n + [1] = [add(n, app(x, y))] [reverse(nil())] = [0] >= [0] = [nil()] [reverse(add(n, x))] = [1] x + [1] n + [1] >= [1] x + [1] n + [1] = [app(reverse(x), add(n, nil()))] [reverse^#(add(n, x))] = [1] x + [1] n + [1] > [1] x + [0] = [c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))] [shuffle^#(add(n, x))] = [1] x + [1] n + [8] > [1] x + [0] = [reverse^#(x)] [shuffle^#(add(n, x))] = [1] x + [1] n + [8] > [1] x + [7] = [shuffle^#(reverse(x))] 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: { reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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. { reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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: { app^#(add(n, x), y) -> c_6(app^#(x, y)) } Weak DPs: { reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil())) , reverse^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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: app^#(add(n, x), y) -> c_6(app^#(x, y)) , 2: reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil())) , 3: reverse^#(add(n, x)) -> reverse^#(x) , 4: shuffle^#(add(n, x)) -> reverse^#(x) , 5: shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_6) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [minus](x1, x2) = [7] x1 + [7] x2 + [0] [0] = [0] [s](x1) = [1] x1 + [0] [quot](x1, x2) = [7] x1 + [7] x2 + [0] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [add](x1, x2) = [1] x1 + [1] x2 + [1] [reverse](x1) = [1] x1 + [0] [shuffle](x1) = [7] x1 + [0] [concat](x1, x2) = [7] x1 + [7] x2 + [0] [leaf] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0] [false] = [0] [true] = [0] [minus^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_1] = [0] [c_2](x1) = [7] x1 + [0] [quot^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_3] = [0] [c_4](x1, x2) = [7] x1 + [7] x2 + [0] [app^#](x1, x2) = [1] x1 + [0] [c_5] = [0] [c_6](x1) = [1] x1 + [0] [reverse^#](x1) = [1] x1 + [0] [c_7] = [0] [c_8](x1, x2) = [7] x1 + [7] x2 + [0] [shuffle^#](x1) = [1] x1 + [7] [c_9] = [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [concat^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_11] = [0] [c_12](x1) = [7] x1 + [0] [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_13] = [0] [c_14] = [0] [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] The following symbols are considered usable {app, reverse, app^#, reverse^#, shuffle^#} The order satisfies the following ordering constraints: [app(nil(), y)] = [1] y + [0] >= [1] y + [0] = [y] [app(add(n, x), y)] = [1] x + [1] y + [1] n + [1] >= [1] x + [1] y + [1] n + [1] = [add(n, app(x, y))] [reverse(nil())] = [0] >= [0] = [nil()] [reverse(add(n, x))] = [1] x + [1] n + [1] >= [1] x + [1] n + [1] = [app(reverse(x), add(n, nil()))] [app^#(add(n, x), y)] = [1] x + [1] n + [1] > [1] x + [0] = [c_6(app^#(x, y))] [reverse^#(add(n, x))] = [1] x + [1] n + [1] > [1] x + [0] = [app^#(reverse(x), add(n, nil()))] [reverse^#(add(n, x))] = [1] x + [1] n + [1] > [1] x + [0] = [reverse^#(x)] [shuffle^#(add(n, x))] = [1] x + [1] n + [8] > [1] x + [0] = [reverse^#(x)] [shuffle^#(add(n, x))] = [1] x + [1] n + [8] > [1] x + [7] = [shuffle^#(reverse(x))] 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: { app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil())) , reverse^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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. { app^#(add(n, x), y) -> c_6(app^#(x, y)) , reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil())) , reverse^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> reverse^#(x) , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 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^3))