YES(O(1),O(n^3)) 444.65/150.26 YES(O(1),O(n^3)) 444.65/150.26 444.65/150.26 We are left with following problem, upon which TcT provides the 444.65/150.26 certificate YES(O(1),O(n^3)). 444.65/150.26 444.65/150.26 Strict Trs: 444.65/150.26 { minus(x, 0()) -> x 444.65/150.26 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.26 , quot(0(), s(y)) -> 0() 444.65/150.26 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 444.65/150.26 , app(nil(), y) -> y 444.65/150.26 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.26 , reverse(nil()) -> nil() 444.65/150.26 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.26 , shuffle(nil()) -> nil() 444.65/150.26 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 444.65/150.26 , concat(leaf(), y) -> y 444.65/150.26 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 444.65/150.26 , less_leaves(x, leaf()) -> false() 444.65/150.26 , less_leaves(leaf(), cons(w, z)) -> true() 444.65/150.26 , less_leaves(cons(u, v), cons(w, z)) -> 444.65/150.26 less_leaves(concat(u, v), concat(w, z)) } 444.65/150.26 Obligation: 444.65/150.26 innermost runtime complexity 444.65/150.26 Answer: 444.65/150.26 YES(O(1),O(n^3)) 444.65/150.26 444.65/150.26 We add the following dependency tuples: 444.65/150.26 444.65/150.26 Strict DPs: 444.65/150.26 { minus^#(x, 0()) -> c_1() 444.65/150.26 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 444.65/150.26 , quot^#(0(), s(y)) -> c_3() 444.65/150.26 , quot^#(s(x), s(y)) -> 444.65/150.26 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(nil(), y) -> c_5() 444.65/150.27 , app^#(add(n, x), y) -> c_6(app^#(x, y)) 444.65/150.27 , reverse^#(nil()) -> c_7() 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(nil()) -> c_9() 444.65/150.27 , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) 444.65/150.27 , concat^#(leaf(), y) -> c_11() 444.65/150.27 , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) 444.65/150.27 , less_leaves^#(x, leaf()) -> c_13() 444.65/150.27 , less_leaves^#(leaf(), cons(w, z)) -> c_14() 444.65/150.27 , less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z)) } 444.65/150.27 444.65/150.27 and mark the set of starting terms. 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(x, 0()) -> c_1() 444.65/150.27 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 444.65/150.27 , quot^#(0(), s(y)) -> c_3() 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(nil(), y) -> c_5() 444.65/150.27 , app^#(add(n, x), y) -> c_6(app^#(x, y)) 444.65/150.27 , reverse^#(nil()) -> c_7() 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(nil()) -> c_9() 444.65/150.27 , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) 444.65/150.27 , concat^#(leaf(), y) -> c_11() 444.65/150.27 , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) 444.65/150.27 , less_leaves^#(x, leaf()) -> c_13() 444.65/150.27 , less_leaves^#(leaf(), cons(w, z)) -> c_14() 444.65/150.27 , less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z)) } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , quot(0(), s(y)) -> 0() 444.65/150.27 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , shuffle(nil()) -> nil() 444.65/150.27 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 444.65/150.27 , less_leaves(x, leaf()) -> false() 444.65/150.27 , less_leaves(leaf(), cons(w, z)) -> true() 444.65/150.27 , less_leaves(cons(u, v), cons(w, z)) -> 444.65/150.27 less_leaves(concat(u, v), concat(w, z)) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 We estimate the number of application of {1,3,5,7,9,11,13,14} by 444.65/150.27 applications of Pre({1,3,5,7,9,11,13,14}) = {2,4,6,8,10,12,15}. 444.65/150.27 Here rules are labeled as follows: 444.65/150.27 444.65/150.27 DPs: 444.65/150.27 { 1: minus^#(x, 0()) -> c_1() 444.65/150.27 , 2: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 444.65/150.27 , 3: quot^#(0(), s(y)) -> c_3() 444.65/150.27 , 4: quot^#(s(x), s(y)) -> 444.65/150.27 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , 5: app^#(nil(), y) -> c_5() 444.65/150.27 , 6: app^#(add(n, x), y) -> c_6(app^#(x, y)) 444.65/150.27 , 7: reverse^#(nil()) -> c_7() 444.65/150.27 , 8: reverse^#(add(n, x)) -> 444.65/150.27 c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , 9: shuffle^#(nil()) -> c_9() 444.65/150.27 , 10: shuffle^#(add(n, x)) -> 444.65/150.27 c_10(shuffle^#(reverse(x)), reverse^#(x)) 444.65/150.27 , 11: concat^#(leaf(), y) -> c_11() 444.65/150.27 , 12: concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) 444.65/150.27 , 13: less_leaves^#(x, leaf()) -> c_13() 444.65/150.27 , 14: less_leaves^#(leaf(), cons(w, z)) -> c_14() 444.65/150.27 , 15: less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z)) } 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_6(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) 444.65/150.27 , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) 444.65/150.27 , less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z)) } 444.65/150.27 Weak DPs: 444.65/150.27 { minus^#(x, 0()) -> c_1() 444.65/150.27 , quot^#(0(), s(y)) -> c_3() 444.65/150.27 , app^#(nil(), y) -> c_5() 444.65/150.27 , reverse^#(nil()) -> c_7() 444.65/150.27 , shuffle^#(nil()) -> c_9() 444.65/150.27 , concat^#(leaf(), y) -> c_11() 444.65/150.27 , less_leaves^#(x, leaf()) -> c_13() 444.65/150.27 , less_leaves^#(leaf(), cons(w, z)) -> c_14() } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , quot(0(), s(y)) -> 0() 444.65/150.27 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , shuffle(nil()) -> nil() 444.65/150.27 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 444.65/150.27 , less_leaves(x, leaf()) -> false() 444.65/150.27 , less_leaves(leaf(), cons(w, z)) -> true() 444.65/150.27 , less_leaves(cons(u, v), cons(w, z)) -> 444.65/150.27 less_leaves(concat(u, v), concat(w, z)) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 The following weak DPs constitute a sub-graph of the DG that is 444.65/150.27 closed under successors. The DPs are removed. 444.65/150.27 444.65/150.27 { minus^#(x, 0()) -> c_1() 444.65/150.27 , quot^#(0(), s(y)) -> c_3() 444.65/150.27 , app^#(nil(), y) -> c_5() 444.65/150.27 , reverse^#(nil()) -> c_7() 444.65/150.27 , shuffle^#(nil()) -> c_9() 444.65/150.27 , concat^#(leaf(), y) -> c_11() 444.65/150.27 , less_leaves^#(x, leaf()) -> c_13() 444.65/150.27 , less_leaves^#(leaf(), cons(w, z)) -> c_14() } 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_6(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) 444.65/150.27 , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) 444.65/150.27 , less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z)) } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , quot(0(), s(y)) -> 0() 444.65/150.27 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , shuffle(nil()) -> nil() 444.65/150.27 , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) 444.65/150.27 , less_leaves(x, leaf()) -> false() 444.65/150.27 , less_leaves(leaf(), cons(w, z)) -> true() 444.65/150.27 , less_leaves(cons(u, v), cons(w, z)) -> 444.65/150.27 less_leaves(concat(u, v), concat(w, z)) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 We replace rewrite rules by usable rules: 444.65/150.27 444.65/150.27 Weak Usable Rules: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_6(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) 444.65/150.27 , concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) 444.65/150.27 , less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z)) } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 We use the processor 'matrix interpretation of dimension 2' to 444.65/150.27 orient following rules strictly. 444.65/150.27 444.65/150.27 DPs: 444.65/150.27 { 6: concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) } 444.65/150.27 444.65/150.27 Sub-proof: 444.65/150.27 ---------- 444.65/150.27 The following argument positions are usable: 444.65/150.27 Uargs(c_2) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_6) = {1}, 444.65/150.27 Uargs(c_8) = {1, 2}, Uargs(c_10) = {1, 2}, Uargs(c_12) = {1}, 444.65/150.27 Uargs(c_15) = {1, 2, 3} 444.65/150.27 444.65/150.27 TcT has computed the following constructor-based matrix 444.65/150.27 interpretation satisfying not(EDA) and not(IDA(1)). 444.65/150.27 444.65/150.27 [minus](x1, x2) = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [0] = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [s](x1) = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [app](x1, x2) = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [nil] = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [add](x1, x2) = [0 0] x1 + [0] 444.65/150.27 [1 1] [0] 444.65/150.27 444.65/150.27 [reverse](x1) = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [concat](x1, x2) = [1 0] x1 + [2 0] x2 + [0] 444.65/150.27 [0 1] [0 1] [0] 444.65/150.27 444.65/150.27 [leaf] = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [cons](x1, x2) = [0 0] x1 + [1 0] x2 + [4] 444.65/150.27 [1 1] [0 1] [0] 444.65/150.27 444.65/150.27 [minus^#](x1, x2) = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [c_2](x1) = [2 0] x1 + [0] 444.65/150.27 [0 0] [0] 444.65/150.27 444.65/150.27 [quot^#](x1, x2) = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [c_4](x1, x2) = [2 0] x1 + [2 0] x2 + [0] 444.65/150.27 [0 0] [0 0] [0] 444.65/150.27 444.65/150.27 [app^#](x1, x2) = [0 0] x2 + [0] 444.65/150.27 [0 4] [4] 444.65/150.27 444.65/150.27 [c_6](x1) = [4 0] x1 + [0] 444.65/150.27 [0 0] [3] 444.65/150.27 444.65/150.27 [reverse^#](x1) = [0 0] x1 + [0] 444.65/150.27 [0 4] [0] 444.65/150.27 444.65/150.27 [c_8](x1, x2) = [4 0] x1 + [1 0] x2 + [0] 444.65/150.27 [0 0] [0 0] [0] 444.65/150.27 444.65/150.27 [shuffle^#](x1) = [0] 444.65/150.27 [0] 444.65/150.27 444.65/150.27 [c_10](x1, x2) = [2 0] x1 + [1 0] x2 + [0] 444.65/150.27 [0 0] [0 0] [0] 444.65/150.27 444.65/150.27 [concat^#](x1, x2) = [2 0] x1 + [0] 444.65/150.27 [1 0] [0] 444.65/150.27 444.65/150.27 [c_12](x1) = [1 0] x1 + [5] 444.65/150.27 [0 0] [3] 444.65/150.27 444.65/150.27 [less_leaves^#](x1, x2) = [0 2] x1 + [0 4] x2 + [0] 444.65/150.27 [0 0] [2 4] [0] 444.65/150.27 444.65/150.27 [c_15](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 2] x3 + [0] 444.65/150.27 [0 0] [0 0] [0 0] [7] 444.65/150.27 444.65/150.27 The order satisfies the following ordering constraints: 444.65/150.27 444.65/150.27 [minus(x, 0())] = [0] 444.65/150.27 [0] 444.65/150.27 ? [1 0] x + [0] 444.65/150.27 [0 1] [0] 444.65/150.27 = [x] 444.65/150.27 444.65/150.27 [minus(s(x), s(y))] = [0] 444.65/150.27 [0] 444.65/150.27 >= [0] 444.65/150.27 [0] 444.65/150.27 = [minus(x, y)] 444.65/150.27 444.65/150.27 [app(nil(), y)] = [0] 444.65/150.27 [0] 444.65/150.27 ? [1 0] y + [0] 444.65/150.27 [0 1] [0] 444.65/150.27 = [y] 444.65/150.27 444.65/150.27 [app(add(n, x), y)] = [0] 444.65/150.27 [0] 444.65/150.27 ? [0 0] n + [0] 444.65/150.27 [1 1] [0] 444.65/150.27 = [add(n, app(x, y))] 444.65/150.27 444.65/150.27 [reverse(nil())] = [0] 444.65/150.27 [0] 444.65/150.27 >= [0] 444.65/150.27 [0] 444.65/150.27 = [nil()] 444.65/150.27 444.65/150.27 [reverse(add(n, x))] = [0] 444.65/150.27 [0] 444.65/150.27 >= [0] 444.65/150.27 [0] 444.65/150.27 = [app(reverse(x), add(n, nil()))] 444.65/150.27 444.65/150.27 [concat(leaf(), y)] = [2 0] y + [0] 444.65/150.27 [0 1] [0] 444.65/150.27 >= [1 0] y + [0] 444.65/150.27 [0 1] [0] 444.65/150.27 = [y] 444.65/150.27 444.65/150.27 [concat(cons(u, v), y)] = [2 0] y + [0 0] u + [1 0] v + [4] 444.65/150.27 [0 1] [1 1] [0 1] [0] 444.65/150.27 >= [2 0] y + [0 0] u + [1 0] v + [4] 444.65/150.27 [0 1] [1 1] [0 1] [0] 444.65/150.27 = [cons(u, concat(v, y))] 444.65/150.27 444.65/150.27 [minus^#(s(x), s(y))] = [0] 444.65/150.27 [0] 444.65/150.27 >= [0] 444.65/150.27 [0] 444.65/150.27 = [c_2(minus^#(x, y))] 444.65/150.27 444.65/150.27 [quot^#(s(x), s(y))] = [0] 444.65/150.27 [0] 444.65/150.27 >= [0] 444.65/150.27 [0] 444.65/150.27 = [c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))] 444.65/150.27 444.65/150.27 [app^#(add(n, x), y)] = [0 0] y + [0] 444.65/150.27 [0 4] [4] 444.65/150.27 >= [0] 444.65/150.27 [3] 444.65/150.27 = [c_6(app^#(x, y))] 444.65/150.27 444.65/150.27 [reverse^#(add(n, x))] = [0 0] n + [0] 444.65/150.27 [4 4] [0] 444.65/150.27 >= [0] 444.65/150.27 [0] 444.65/150.27 = [c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))] 444.65/150.27 444.65/150.27 [shuffle^#(add(n, x))] = [0] 444.65/150.27 [0] 444.65/150.27 >= [0] 444.65/150.27 [0] 444.65/150.27 = [c_10(shuffle^#(reverse(x)), reverse^#(x))] 444.65/150.27 444.65/150.27 [concat^#(cons(u, v), y)] = [2 0] v + [8] 444.65/150.27 [1 0] [4] 444.65/150.27 > [2 0] v + [5] 444.65/150.27 [0 0] [3] 444.65/150.27 = [c_12(concat^#(v, y))] 444.65/150.27 444.65/150.27 [less_leaves^#(cons(u, v), cons(w, z))] = [2 2] u + [0 2] v + [4 4] w + [0 4] z + [0] 444.65/150.27 [0 0] [0 0] [4 4] [2 4] [8] 444.65/150.27 >= [2 2] u + [0 2] v + [4 4] w + [0 4] z + [0] 444.65/150.27 [0 0] [0 0] [0 0] [0 0] [7] 444.65/150.27 = [c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z))] 444.65/150.27 444.65/150.27 444.65/150.27 The strictly oriented rules are moved into the weak component. 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_6(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) 444.65/150.27 , less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z)) } 444.65/150.27 Weak DPs: { concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 The following weak DPs constitute a sub-graph of the DG that is 444.65/150.27 closed under successors. The DPs are removed. 444.65/150.27 444.65/150.27 { concat^#(cons(u, v), y) -> c_12(concat^#(v, y)) } 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_6(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x)) 444.65/150.27 , less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z)) } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 Due to missing edges in the dependency-graph, the right-hand sides 444.65/150.27 of following rules could be simplified: 444.65/150.27 444.65/150.27 { less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_15(less_leaves^#(concat(u, v), concat(w, z)), 444.65/150.27 concat^#(u, v), 444.65/150.27 concat^#(w, z)) } 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(add(n, x)) -> c_5(shuffle^#(reverse(x)), reverse^#(x)) 444.65/150.27 , less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_6(less_leaves^#(concat(u, v), concat(w, z))) } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 We use the processor 'matrix interpretation of dimension 1' to 444.65/150.27 orient following rules strictly. 444.65/150.27 444.65/150.27 DPs: 444.65/150.27 { 6: less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_6(less_leaves^#(concat(u, v), concat(w, z))) } 444.65/150.27 Trs: { concat(leaf(), y) -> y } 444.65/150.27 444.65/150.27 Sub-proof: 444.65/150.27 ---------- 444.65/150.27 The following argument positions are usable: 444.65/150.27 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 444.65/150.27 Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}, Uargs(c_6) = {1} 444.65/150.27 444.65/150.27 TcT has computed the following constructor-based matrix 444.65/150.27 interpretation satisfying not(EDA). 444.65/150.27 444.65/150.27 [minus](x1, x2) = [0] 444.65/150.27 444.65/150.27 [0] = [7] 444.65/150.27 444.65/150.27 [s](x1) = [0] 444.65/150.27 444.65/150.27 [app](x1, x2) = [0] 444.65/150.27 444.65/150.27 [nil] = [0] 444.65/150.27 444.65/150.27 [add](x1, x2) = [1] x1 + [0] 444.65/150.27 444.65/150.27 [reverse](x1) = [0] 444.65/150.27 444.65/150.27 [concat](x1, x2) = [1] x1 + [1] x2 + [2] 444.65/150.27 444.65/150.27 [leaf] = [1] 444.65/150.27 444.65/150.27 [cons](x1, x2) = [1] x1 + [1] x2 + [6] 444.65/150.27 444.65/150.27 [minus^#](x1, x2) = [0] 444.65/150.27 444.65/150.27 [c_2](x1) = [7] x1 + [0] 444.65/150.27 444.65/150.27 [quot^#](x1, x2) = [0] 444.65/150.27 444.65/150.27 [c_4](x1, x2) = [7] x1 + [7] x2 + [0] 444.65/150.27 444.65/150.27 [app^#](x1, x2) = [0] 444.65/150.27 444.65/150.27 [c_6](x1) = [7] x1 + [0] 444.65/150.27 444.65/150.27 [reverse^#](x1) = [0] 444.65/150.27 444.65/150.27 [c_8](x1, x2) = [7] x1 + [7] x2 + [0] 444.65/150.27 444.65/150.27 [shuffle^#](x1) = [0] 444.65/150.27 444.65/150.27 [c_10](x1, x2) = [7] x1 + [7] x2 + [0] 444.65/150.27 444.65/150.27 [concat^#](x1, x2) = [7] x1 + [7] x2 + [0] 444.65/150.27 444.65/150.27 [c_12](x1) = [7] x1 + [0] 444.65/150.27 444.65/150.27 [less_leaves^#](x1, x2) = [1] x1 + [4] 444.65/150.27 444.65/150.27 [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 444.65/150.27 444.65/150.27 [c] = [0] 444.65/150.27 444.65/150.27 [c_1](x1) = [1] x1 + [0] 444.65/150.27 444.65/150.27 [c_2](x1, x2) = [1] x1 + [2] x2 + [0] 444.65/150.27 444.65/150.27 [c_3](x1) = [2] x1 + [0] 444.65/150.27 444.65/150.27 [c_4](x1, x2) = [4] x1 + [1] x2 + [0] 444.65/150.27 444.65/150.27 [c_5](x1, x2) = [4] x1 + [2] x2 + [0] 444.65/150.27 444.65/150.27 [c_6](x1) = [1] x1 + [0] 444.65/150.27 444.65/150.27 The order satisfies the following ordering constraints: 444.65/150.27 444.65/150.27 [minus(x, 0())] = [0] 444.65/150.27 ? [1] x + [0] 444.65/150.27 = [x] 444.65/150.27 444.65/150.27 [minus(s(x), s(y))] = [0] 444.65/150.27 >= [0] 444.65/150.27 = [minus(x, y)] 444.65/150.27 444.65/150.27 [app(nil(), y)] = [0] 444.65/150.27 ? [1] y + [0] 444.65/150.27 = [y] 444.65/150.27 444.65/150.27 [app(add(n, x), y)] = [0] 444.65/150.27 ? [1] n + [0] 444.65/150.27 = [add(n, app(x, y))] 444.65/150.27 444.65/150.27 [reverse(nil())] = [0] 444.65/150.27 >= [0] 444.65/150.27 = [nil()] 444.65/150.27 444.65/150.27 [reverse(add(n, x))] = [0] 444.65/150.27 >= [0] 444.65/150.27 = [app(reverse(x), add(n, nil()))] 444.65/150.27 444.65/150.27 [concat(leaf(), y)] = [1] y + [3] 444.65/150.27 > [1] y + [0] 444.65/150.27 = [y] 444.65/150.27 444.65/150.27 [concat(cons(u, v), y)] = [1] y + [1] u + [1] v + [8] 444.65/150.27 >= [1] y + [1] u + [1] v + [8] 444.65/150.27 = [cons(u, concat(v, y))] 444.65/150.27 444.65/150.27 [minus^#(s(x), s(y))] = [0] 444.65/150.27 >= [0] 444.65/150.27 = [c_1(minus^#(x, y))] 444.65/150.27 444.65/150.27 [quot^#(s(x), s(y))] = [0] 444.65/150.27 >= [0] 444.65/150.27 = [c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))] 444.65/150.27 444.65/150.27 [app^#(add(n, x), y)] = [0] 444.65/150.27 >= [0] 444.65/150.27 = [c_3(app^#(x, y))] 444.65/150.27 444.65/150.27 [reverse^#(add(n, x))] = [0] 444.65/150.27 >= [0] 444.65/150.27 = [c_4(app^#(reverse(x), add(n, nil())), reverse^#(x))] 444.65/150.27 444.65/150.27 [shuffle^#(add(n, x))] = [0] 444.65/150.27 >= [0] 444.65/150.27 = [c_5(shuffle^#(reverse(x)), reverse^#(x))] 444.65/150.27 444.65/150.27 [less_leaves^#(cons(u, v), cons(w, z))] = [1] u + [1] v + [10] 444.65/150.27 > [1] u + [1] v + [6] 444.65/150.27 = [c_6(less_leaves^#(concat(u, v), concat(w, z)))] 444.65/150.27 444.65/150.27 444.65/150.27 The strictly oriented rules are moved into the weak component. 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(add(n, x)) -> 444.65/150.27 c_5(shuffle^#(reverse(x)), reverse^#(x)) } 444.65/150.27 Weak DPs: 444.65/150.27 { less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_6(less_leaves^#(concat(u, v), concat(w, z))) } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 The following weak DPs constitute a sub-graph of the DG that is 444.65/150.27 closed under successors. The DPs are removed. 444.65/150.27 444.65/150.27 { less_leaves^#(cons(u, v), cons(w, z)) -> 444.65/150.27 c_6(less_leaves^#(concat(u, v), concat(w, z))) } 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(add(n, x)) -> 444.65/150.27 c_5(shuffle^#(reverse(x)), reverse^#(x)) } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) 444.65/150.27 , concat(leaf(), y) -> y 444.65/150.27 , concat(cons(u, v), y) -> cons(u, concat(v, y)) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 We replace rewrite rules by usable rules: 444.65/150.27 444.65/150.27 Weak Usable Rules: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.27 444.65/150.27 We are left with following problem, upon which TcT provides the 444.65/150.27 certificate YES(O(1),O(n^3)). 444.65/150.27 444.65/150.27 Strict DPs: 444.65/150.27 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 444.65/150.27 , quot^#(s(x), s(y)) -> 444.65/150.27 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.27 , shuffle^#(add(n, x)) -> 444.65/150.27 c_5(shuffle^#(reverse(x)), reverse^#(x)) } 444.65/150.27 Weak Trs: 444.65/150.27 { minus(x, 0()) -> x 444.65/150.27 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.27 , app(nil(), y) -> y 444.65/150.27 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.27 , reverse(nil()) -> nil() 444.65/150.27 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.27 Obligation: 444.65/150.27 innermost runtime complexity 444.65/150.27 Answer: 444.65/150.27 YES(O(1),O(n^3)) 444.65/150.27 444.65/150.27 We decompose the input problem according to the dependency graph 444.65/150.27 into the upper component 444.65/150.27 444.65/150.27 { quot^#(s(x), s(y)) -> 444.65/150.27 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.27 , shuffle^#(add(n, x)) -> 444.65/150.27 c_5(shuffle^#(reverse(x)), reverse^#(x)) } 444.65/150.27 444.65/150.27 and lower component 444.65/150.27 444.65/150.27 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 444.65/150.27 , app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.27 , reverse^#(add(n, x)) -> 444.65/150.27 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 444.65/150.27 444.65/150.27 Further, following extension rules are added to the lower 444.65/150.28 component. 444.65/150.28 444.65/150.28 { quot^#(s(x), s(y)) -> minus^#(x, y) 444.65/150.28 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 444.65/150.28 , shuffle^#(add(n, x)) -> reverse^#(x) 444.65/150.28 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 444.65/150.28 444.65/150.28 TcT solves the upper component with certificate YES(O(1),O(n^1)). 444.65/150.28 444.65/150.28 Sub-proof: 444.65/150.28 ---------- 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(n^1)). 444.65/150.28 444.65/150.28 Strict DPs: 444.65/150.28 { quot^#(s(x), s(y)) -> 444.65/150.28 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) 444.65/150.28 , shuffle^#(add(n, x)) -> 444.65/150.28 c_5(shuffle^#(reverse(x)), reverse^#(x)) } 444.65/150.28 Weak Trs: 444.65/150.28 { minus(x, 0()) -> x 444.65/150.28 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.28 , app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(n^1)) 444.65/150.28 444.65/150.28 We use the processor 'matrix interpretation of dimension 1' to 444.65/150.28 orient following rules strictly. 444.65/150.28 444.65/150.28 DPs: 444.65/150.28 { 1: quot^#(s(x), s(y)) -> 444.65/150.28 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 444.65/150.28 Trs: { minus(s(x), s(y)) -> minus(x, y) } 444.65/150.28 444.65/150.28 Sub-proof: 444.65/150.28 ---------- 444.65/150.28 The following argument positions are usable: 444.65/150.28 Uargs(c_2) = {1}, Uargs(c_5) = {1} 444.65/150.28 444.65/150.28 TcT has computed the following constructor-based matrix 444.65/150.28 interpretation satisfying not(EDA). 444.65/150.28 444.65/150.28 [minus](x1, x2) = [1] x1 + [0] 444.65/150.28 444.65/150.28 [0] = [7] 444.65/150.28 444.65/150.28 [s](x1) = [1] x1 + [3] 444.65/150.28 444.65/150.28 [app](x1, x2) = [0] 444.65/150.28 444.65/150.28 [nil] = [0] 444.65/150.28 444.65/150.28 [add](x1, x2) = [1] x1 + [0] 444.65/150.28 444.65/150.28 [reverse](x1) = [0] 444.65/150.28 444.65/150.28 [minus^#](x1, x2) = [1] 444.65/150.28 444.65/150.28 [quot^#](x1, x2) = [3] x1 + [0] 444.65/150.28 444.65/150.28 [reverse^#](x1) = [7] x1 + [7] 444.65/150.28 444.65/150.28 [shuffle^#](x1) = [0] 444.65/150.28 444.65/150.28 [c_2](x1, x2) = [1] x1 + [1] x2 + [1] 444.65/150.28 444.65/150.28 [c_5](x1, x2) = [4] x1 + [0] 444.65/150.28 444.65/150.28 The order satisfies the following ordering constraints: 444.65/150.28 444.65/150.28 [minus(x, 0())] = [1] x + [0] 444.65/150.28 >= [1] x + [0] 444.65/150.28 = [x] 444.65/150.28 444.65/150.28 [minus(s(x), s(y))] = [1] x + [3] 444.65/150.28 > [1] x + [0] 444.65/150.28 = [minus(x, y)] 444.65/150.28 444.65/150.28 [app(nil(), y)] = [0] 444.65/150.28 ? [1] y + [0] 444.65/150.28 = [y] 444.65/150.28 444.65/150.28 [app(add(n, x), y)] = [0] 444.65/150.28 ? [1] n + [0] 444.65/150.28 = [add(n, app(x, y))] 444.65/150.28 444.65/150.28 [reverse(nil())] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [nil()] 444.65/150.28 444.65/150.28 [reverse(add(n, x))] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [app(reverse(x), add(n, nil()))] 444.65/150.28 444.65/150.28 [quot^#(s(x), s(y))] = [3] x + [9] 444.65/150.28 > [3] x + [2] 444.65/150.28 = [c_2(quot^#(minus(x, y), s(y)), minus^#(x, y))] 444.65/150.28 444.65/150.28 [shuffle^#(add(n, x))] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [c_5(shuffle^#(reverse(x)), reverse^#(x))] 444.65/150.28 444.65/150.28 444.65/150.28 The strictly oriented rules are moved into the weak component. 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(n^1)). 444.65/150.28 444.65/150.28 Strict DPs: 444.65/150.28 { shuffle^#(add(n, x)) -> 444.65/150.28 c_5(shuffle^#(reverse(x)), reverse^#(x)) } 444.65/150.28 Weak DPs: 444.65/150.28 { quot^#(s(x), s(y)) -> 444.65/150.28 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 444.65/150.28 Weak Trs: 444.65/150.28 { minus(x, 0()) -> x 444.65/150.28 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.28 , app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(n^1)) 444.65/150.28 444.65/150.28 The following weak DPs constitute a sub-graph of the DG that is 444.65/150.28 closed under successors. The DPs are removed. 444.65/150.28 444.65/150.28 { quot^#(s(x), s(y)) -> 444.65/150.28 c_2(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(n^1)). 444.65/150.28 444.65/150.28 Strict DPs: 444.65/150.28 { shuffle^#(add(n, x)) -> 444.65/150.28 c_5(shuffle^#(reverse(x)), reverse^#(x)) } 444.65/150.28 Weak Trs: 444.65/150.28 { minus(x, 0()) -> x 444.65/150.28 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.28 , app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(n^1)) 444.65/150.28 444.65/150.28 Due to missing edges in the dependency-graph, the right-hand sides 444.65/150.28 of following rules could be simplified: 444.65/150.28 444.65/150.28 { shuffle^#(add(n, x)) -> 444.65/150.28 c_5(shuffle^#(reverse(x)), reverse^#(x)) } 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(n^1)). 444.65/150.28 444.65/150.28 Strict DPs: { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } 444.65/150.28 Weak Trs: 444.65/150.28 { minus(x, 0()) -> x 444.65/150.28 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.28 , app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(n^1)) 444.65/150.28 444.65/150.28 We replace rewrite rules by usable rules: 444.65/150.28 444.65/150.28 Weak Usable Rules: 444.65/150.28 { app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(n^1)). 444.65/150.28 444.65/150.28 Strict DPs: { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } 444.65/150.28 Weak Trs: 444.65/150.28 { app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(n^1)) 444.65/150.28 444.65/150.28 We use the processor 'matrix interpretation of dimension 1' to 444.65/150.28 orient following rules strictly. 444.65/150.28 444.65/150.28 DPs: 444.65/150.28 { 1: shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } 444.65/150.28 444.65/150.28 Sub-proof: 444.65/150.28 ---------- 444.65/150.28 The following argument positions are usable: 444.65/150.28 Uargs(c_1) = {1} 444.65/150.28 444.65/150.28 TcT has computed the following constructor-based matrix 444.65/150.28 interpretation satisfying not(EDA). 444.65/150.28 444.65/150.28 [minus](x1, x2) = [7] x1 + [7] x2 + [0] 444.65/150.28 444.65/150.28 [0] = [0] 444.65/150.28 444.65/150.28 [s](x1) = [1] x1 + [0] 444.65/150.28 444.65/150.28 [app](x1, x2) = [1] x1 + [1] x2 + [0] 444.65/150.28 444.65/150.28 [nil] = [0] 444.65/150.28 444.65/150.28 [add](x1, x2) = [1] x1 + [1] x2 + [1] 444.65/150.28 444.65/150.28 [reverse](x1) = [1] x1 + [0] 444.65/150.28 444.65/150.28 [minus^#](x1, x2) = [7] x1 + [7] x2 + [0] 444.65/150.28 444.65/150.28 [quot^#](x1, x2) = [7] x1 + [7] x2 + [0] 444.65/150.28 444.65/150.28 [reverse^#](x1) = [7] x1 + [0] 444.65/150.28 444.65/150.28 [shuffle^#](x1) = [2] x1 + [0] 444.65/150.28 444.65/150.28 [c_2](x1, x2) = [7] x1 + [7] x2 + [0] 444.65/150.28 444.65/150.28 [c_5](x1, x2) = [7] x1 + [7] x2 + [0] 444.65/150.28 444.65/150.28 [c] = [0] 444.65/150.28 444.65/150.28 [c_1](x1) = [1] x1 + [1] 444.65/150.28 444.65/150.28 The order satisfies the following ordering constraints: 444.65/150.28 444.65/150.28 [app(nil(), y)] = [1] y + [0] 444.65/150.28 >= [1] y + [0] 444.65/150.28 = [y] 444.65/150.28 444.65/150.28 [app(add(n, x), y)] = [1] x + [1] y + [1] n + [1] 444.65/150.28 >= [1] x + [1] y + [1] n + [1] 444.65/150.28 = [add(n, app(x, y))] 444.65/150.28 444.65/150.28 [reverse(nil())] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [nil()] 444.65/150.28 444.65/150.28 [reverse(add(n, x))] = [1] x + [1] n + [1] 444.65/150.28 >= [1] x + [1] n + [1] 444.65/150.28 = [app(reverse(x), add(n, nil()))] 444.65/150.28 444.65/150.28 [shuffle^#(add(n, x))] = [2] x + [2] n + [2] 444.65/150.28 > [2] x + [1] 444.65/150.28 = [c_1(shuffle^#(reverse(x)))] 444.65/150.28 444.65/150.28 444.65/150.28 The strictly oriented rules are moved into the weak component. 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(1)). 444.65/150.28 444.65/150.28 Weak DPs: { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } 444.65/150.28 Weak Trs: 444.65/150.28 { app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(1)) 444.65/150.28 444.65/150.28 The following weak DPs constitute a sub-graph of the DG that is 444.65/150.28 closed under successors. The DPs are removed. 444.65/150.28 444.65/150.28 { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) } 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(1)). 444.65/150.28 444.65/150.28 Weak Trs: 444.65/150.28 { app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(1)) 444.65/150.28 444.65/150.28 No rule is usable, rules are removed from the input problem. 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(1)). 444.65/150.28 444.65/150.28 Rules: Empty 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(1)) 444.65/150.28 444.65/150.28 Empty rules are trivially bounded 444.65/150.28 444.65/150.28 We return to the main proof. 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(n^2)). 444.65/150.28 444.65/150.28 Strict DPs: 444.65/150.28 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 444.65/150.28 , app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.28 , reverse^#(add(n, x)) -> 444.65/150.28 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 444.65/150.28 Weak DPs: 444.65/150.28 { quot^#(s(x), s(y)) -> minus^#(x, y) 444.65/150.28 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 444.65/150.28 , shuffle^#(add(n, x)) -> reverse^#(x) 444.65/150.28 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 444.65/150.28 Weak Trs: 444.65/150.28 { minus(x, 0()) -> x 444.65/150.28 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.28 , app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(n^2)) 444.65/150.28 444.65/150.28 We use the processor 'matrix interpretation of dimension 1' to 444.65/150.28 orient following rules strictly. 444.65/150.28 444.65/150.28 DPs: 444.65/150.28 { 1: minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 444.65/150.28 , 4: quot^#(s(x), s(y)) -> minus^#(x, y) 444.65/150.28 , 5: quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 444.65/150.28 Trs: { minus(s(x), s(y)) -> minus(x, y) } 444.65/150.28 444.65/150.28 Sub-proof: 444.65/150.28 ---------- 444.65/150.28 The following argument positions are usable: 444.65/150.28 Uargs(c_1) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1, 2} 444.65/150.28 444.65/150.28 TcT has computed the following constructor-based matrix 444.65/150.28 interpretation satisfying not(EDA). 444.65/150.28 444.65/150.28 [minus](x1, x2) = [1] x1 + [0] 444.65/150.28 444.65/150.28 [0] = [7] 444.65/150.28 444.65/150.28 [s](x1) = [1] x1 + [1] 444.65/150.28 444.65/150.28 [app](x1, x2) = [0] 444.65/150.28 444.65/150.28 [nil] = [0] 444.65/150.28 444.65/150.28 [add](x1, x2) = [1] x1 + [0] 444.65/150.28 444.65/150.28 [reverse](x1) = [0] 444.65/150.28 444.65/150.28 [minus^#](x1, x2) = [2] x2 + [6] 444.65/150.28 444.65/150.28 [quot^#](x1, x2) = [4] x1 + [4] x2 + [0] 444.65/150.28 444.65/150.28 [app^#](x1, x2) = [0] 444.65/150.28 444.65/150.28 [reverse^#](x1) = [0] 444.65/150.28 444.65/150.28 [shuffle^#](x1) = [0] 444.65/150.28 444.65/150.28 [c_1](x1) = [1] x1 + [0] 444.65/150.28 444.65/150.28 [c_3](x1) = [4] x1 + [0] 444.65/150.28 444.65/150.28 [c_4](x1, x2) = [2] x1 + [1] x2 + [0] 444.65/150.28 444.65/150.28 The order satisfies the following ordering constraints: 444.65/150.28 444.65/150.28 [minus(x, 0())] = [1] x + [0] 444.65/150.28 >= [1] x + [0] 444.65/150.28 = [x] 444.65/150.28 444.65/150.28 [minus(s(x), s(y))] = [1] x + [1] 444.65/150.28 > [1] x + [0] 444.65/150.28 = [minus(x, y)] 444.65/150.28 444.65/150.28 [app(nil(), y)] = [0] 444.65/150.28 ? [1] y + [0] 444.65/150.28 = [y] 444.65/150.28 444.65/150.28 [app(add(n, x), y)] = [0] 444.65/150.28 ? [1] n + [0] 444.65/150.28 = [add(n, app(x, y))] 444.65/150.28 444.65/150.28 [reverse(nil())] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [nil()] 444.65/150.28 444.65/150.28 [reverse(add(n, x))] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [app(reverse(x), add(n, nil()))] 444.65/150.28 444.65/150.28 [minus^#(s(x), s(y))] = [2] y + [8] 444.65/150.28 > [2] y + [6] 444.65/150.28 = [c_1(minus^#(x, y))] 444.65/150.28 444.65/150.28 [quot^#(s(x), s(y))] = [4] x + [4] y + [8] 444.65/150.28 > [2] y + [6] 444.65/150.28 = [minus^#(x, y)] 444.65/150.28 444.65/150.28 [quot^#(s(x), s(y))] = [4] x + [4] y + [8] 444.65/150.28 > [4] x + [4] y + [4] 444.65/150.28 = [quot^#(minus(x, y), s(y))] 444.65/150.28 444.65/150.28 [app^#(add(n, x), y)] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [c_3(app^#(x, y))] 444.65/150.28 444.65/150.28 [reverse^#(add(n, x))] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [c_4(app^#(reverse(x), add(n, nil())), reverse^#(x))] 444.65/150.28 444.65/150.28 [shuffle^#(add(n, x))] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [reverse^#(x)] 444.65/150.28 444.65/150.28 [shuffle^#(add(n, x))] = [0] 444.65/150.28 >= [0] 444.65/150.28 = [shuffle^#(reverse(x))] 444.65/150.28 444.65/150.28 444.65/150.28 The strictly oriented rules are moved into the weak component. 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(n^2)). 444.65/150.28 444.65/150.28 Strict DPs: 444.65/150.28 { app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.28 , reverse^#(add(n, x)) -> 444.65/150.28 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 444.65/150.28 Weak DPs: 444.65/150.28 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 444.65/150.28 , quot^#(s(x), s(y)) -> minus^#(x, y) 444.65/150.28 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 444.65/150.28 , shuffle^#(add(n, x)) -> reverse^#(x) 444.65/150.28 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 444.65/150.28 Weak Trs: 444.65/150.28 { minus(x, 0()) -> x 444.65/150.28 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.28 , app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(n^2)) 444.65/150.28 444.65/150.28 The following weak DPs constitute a sub-graph of the DG that is 444.65/150.28 closed under successors. The DPs are removed. 444.65/150.28 444.65/150.28 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 444.65/150.28 , quot^#(s(x), s(y)) -> minus^#(x, y) 444.65/150.28 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(n^2)). 444.65/150.28 444.65/150.28 Strict DPs: 444.65/150.28 { app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.28 , reverse^#(add(n, x)) -> 444.65/150.28 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 444.65/150.28 Weak DPs: 444.65/150.28 { shuffle^#(add(n, x)) -> reverse^#(x) 444.65/150.28 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 444.65/150.28 Weak Trs: 444.65/150.28 { minus(x, 0()) -> x 444.65/150.28 , minus(s(x), s(y)) -> minus(x, y) 444.65/150.28 , app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(n^2)) 444.65/150.28 444.65/150.28 We replace rewrite rules by usable rules: 444.65/150.28 444.65/150.28 Weak Usable Rules: 444.65/150.28 { app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(n^2)). 444.65/150.28 444.65/150.28 Strict DPs: 444.65/150.28 { app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.28 , reverse^#(add(n, x)) -> 444.65/150.28 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) } 444.65/150.28 Weak DPs: 444.65/150.28 { shuffle^#(add(n, x)) -> reverse^#(x) 444.65/150.28 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 444.65/150.28 Weak Trs: 444.65/150.28 { app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(n^2)) 444.65/150.28 444.65/150.28 We use the processor 'polynomial interpretation' to orient 444.65/150.28 following rules strictly. 444.65/150.28 444.65/150.28 DPs: 444.65/150.28 { 1: app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.28 , 2: reverse^#(add(n, x)) -> 444.65/150.28 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.28 , 3: shuffle^#(add(n, x)) -> reverse^#(x) 444.65/150.28 , 4: shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 444.65/150.28 444.65/150.28 Sub-proof: 444.65/150.28 ---------- 444.65/150.28 We consider the following typing: 444.65/150.28 444.65/150.28 minus :: (a,b) -> c 444.65/150.28 0 :: d 444.65/150.28 s :: e -> f 444.65/150.28 app :: (n,n) -> n 444.65/150.28 nil :: n 444.65/150.28 add :: (g,n) -> n 444.65/150.28 reverse :: n -> n 444.65/150.28 minus^# :: (h,i) -> j 444.65/150.28 quot^# :: (k,l) -> m 444.65/150.28 app^# :: (n,n) -> q 444.65/150.28 reverse^# :: n -> r 444.65/150.28 shuffle^# :: n -> r 444.65/150.28 c_1 :: o -> p 444.65/150.28 c_3 :: q -> q 444.65/150.28 c_4 :: (q,r) -> r 444.65/150.28 444.65/150.28 The following argument positions are considered usable: 444.65/150.28 444.65/150.28 Uargs(c_3) = {1}, Uargs(c_4) = {1, 2} 444.65/150.28 444.65/150.28 TcT has computed the following constructor-restricted 444.65/150.28 typedpolynomial interpretation. 444.65/150.28 444.65/150.28 [minus](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2 + 3*x2^2 444.65/150.28 444.65/150.28 [0]() = 0 444.65/150.28 444.65/150.28 [s](x1) = 3*x1 444.65/150.28 444.65/150.28 [app](x1, x2) = x1 + x2 444.65/150.28 444.65/150.28 [nil]() = 0 444.65/150.28 444.65/150.28 [add](x1, x2) = 1 + x2 444.65/150.28 444.65/150.28 [reverse](x1) = x1 444.65/150.28 444.65/150.28 [minus^#](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2 + 3*x2^2 444.65/150.28 444.65/150.28 [quot^#](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2 + 3*x2^2 444.65/150.28 444.65/150.28 [app^#](x1, x2) = 2*x1 444.65/150.28 444.65/150.28 [reverse^#](x1) = x1 + x1^2 444.65/150.28 444.65/150.28 [shuffle^#](x1) = 2*x1 + x1^2 444.65/150.28 444.65/150.28 [c_1](x1) = 3*x1 + 3*x1^2 444.65/150.28 444.65/150.28 [c_3](x1) = x1 444.65/150.28 444.65/150.28 [c_4](x1, x2) = x1 + x2 444.65/150.28 444.65/150.28 444.65/150.28 This order satisfies the following ordering constraints. 444.65/150.28 444.65/150.28 [app(nil(), y)] = y 444.65/150.28 >= y 444.65/150.28 = [y] 444.65/150.28 444.65/150.28 [app(add(n, x), y)] = 1 + x + y 444.65/150.28 >= 1 + x + y 444.65/150.28 = [add(n, app(x, y))] 444.65/150.28 444.65/150.28 [reverse(nil())] = 444.65/150.28 >= 444.65/150.28 = [nil()] 444.65/150.28 444.65/150.28 [reverse(add(n, x))] = 1 + x 444.65/150.28 >= x + 1 444.65/150.28 = [app(reverse(x), add(n, nil()))] 444.65/150.28 444.65/150.28 [app^#(add(n, x), y)] = 2 + 2*x 444.65/150.28 > 2*x 444.65/150.28 = [c_3(app^#(x, y))] 444.65/150.28 444.65/150.28 [reverse^#(add(n, x))] = 2 + 3*x + x^2 444.65/150.28 > 3*x + x^2 444.65/150.28 = [c_4(app^#(reverse(x), add(n, nil())), reverse^#(x))] 444.65/150.28 444.65/150.28 [shuffle^#(add(n, x))] = 3 + 4*x + x^2 444.65/150.28 > x + x^2 444.65/150.28 = [reverse^#(x)] 444.65/150.28 444.65/150.28 [shuffle^#(add(n, x))] = 3 + 4*x + x^2 444.65/150.28 > 2*x + x^2 444.65/150.28 = [shuffle^#(reverse(x))] 444.65/150.28 444.65/150.28 444.65/150.28 The strictly oriented rules are moved into the weak component. 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(1)). 444.65/150.28 444.65/150.28 Weak DPs: 444.65/150.28 { app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.28 , reverse^#(add(n, x)) -> 444.65/150.28 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.28 , shuffle^#(add(n, x)) -> reverse^#(x) 444.65/150.28 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 444.65/150.28 Weak Trs: 444.65/150.28 { app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(1)) 444.65/150.28 444.65/150.28 The following weak DPs constitute a sub-graph of the DG that is 444.65/150.28 closed under successors. The DPs are removed. 444.65/150.28 444.65/150.28 { app^#(add(n, x), y) -> c_3(app^#(x, y)) 444.65/150.28 , reverse^#(add(n, x)) -> 444.65/150.28 c_4(app^#(reverse(x), add(n, nil())), reverse^#(x)) 444.65/150.28 , shuffle^#(add(n, x)) -> reverse^#(x) 444.65/150.28 , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) } 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(1)). 444.65/150.28 444.65/150.28 Weak Trs: 444.65/150.28 { app(nil(), y) -> y 444.65/150.28 , app(add(n, x), y) -> add(n, app(x, y)) 444.65/150.28 , reverse(nil()) -> nil() 444.65/150.28 , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) } 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(1)) 444.65/150.28 444.65/150.28 No rule is usable, rules are removed from the input problem. 444.65/150.28 444.65/150.28 We are left with following problem, upon which TcT provides the 444.65/150.28 certificate YES(O(1),O(1)). 444.65/150.28 444.65/150.28 Rules: Empty 444.65/150.28 Obligation: 444.65/150.28 innermost runtime complexity 444.65/150.28 Answer: 444.65/150.28 YES(O(1),O(1)) 444.65/150.28 444.65/150.28 Empty rules are trivially bounded 444.65/150.28 444.65/150.28 Hurray, we answered YES(O(1),O(n^3)) 444.91/150.34 EOF