YES(O(1),O(n^2)) 304.12/156.73 YES(O(1),O(n^2)) 304.12/156.73 304.12/156.73 We are left with following problem, upon which TcT provides the 304.12/156.73 certificate YES(O(1),O(n^2)). 304.12/156.73 304.12/156.73 Strict Trs: 304.12/156.73 { sort(nil()) -> nil() 304.12/156.73 , sort(cons(x, y)) -> insert(x, sort(y)) 304.12/156.73 , insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 304.12/156.73 , choose(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 choose(x, cons(v, w), y, z) } 304.12/156.73 Obligation: 304.12/156.73 innermost runtime complexity 304.12/156.73 Answer: 304.12/156.73 YES(O(1),O(n^2)) 304.12/156.73 304.12/156.73 We add the following dependency tuples: 304.12/156.73 304.12/156.73 Strict DPs: 304.12/156.73 { sort^#(nil()) -> c_1() 304.12/156.73 , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , insert^#(x, nil()) -> c_3() 304.12/156.73 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , choose^#(x, cons(v, w), y, 0()) -> c_5() 304.12/156.73 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) 304.12/156.73 , choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) } 304.12/156.73 304.12/156.73 and mark the set of starting terms. 304.12/156.73 304.12/156.73 We are left with following problem, upon which TcT provides the 304.12/156.73 certificate YES(O(1),O(n^2)). 304.12/156.73 304.12/156.73 Strict DPs: 304.12/156.73 { sort^#(nil()) -> c_1() 304.12/156.73 , sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , insert^#(x, nil()) -> c_3() 304.12/156.73 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , choose^#(x, cons(v, w), y, 0()) -> c_5() 304.12/156.73 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) 304.12/156.73 , choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) } 304.12/156.73 Weak Trs: 304.12/156.73 { sort(nil()) -> nil() 304.12/156.73 , sort(cons(x, y)) -> insert(x, sort(y)) 304.12/156.73 , insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 304.12/156.73 , choose(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 choose(x, cons(v, w), y, z) } 304.12/156.73 Obligation: 304.12/156.73 innermost runtime complexity 304.12/156.73 Answer: 304.12/156.73 YES(O(1),O(n^2)) 304.12/156.73 304.12/156.73 We estimate the number of application of {1,3,5} by applications of 304.12/156.73 Pre({1,3,5}) = {2,4,6,7}. Here rules are labeled as follows: 304.12/156.73 304.12/156.73 DPs: 304.12/156.73 { 1: sort^#(nil()) -> c_1() 304.12/156.73 , 2: sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , 3: insert^#(x, nil()) -> c_3() 304.12/156.73 , 4: insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , 5: choose^#(x, cons(v, w), y, 0()) -> c_5() 304.12/156.73 , 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) 304.12/156.73 , 7: choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) } 304.12/156.73 304.12/156.73 We are left with following problem, upon which TcT provides the 304.12/156.73 certificate YES(O(1),O(n^2)). 304.12/156.73 304.12/156.73 Strict DPs: 304.12/156.73 { sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) 304.12/156.73 , choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) } 304.12/156.73 Weak DPs: 304.12/156.73 { sort^#(nil()) -> c_1() 304.12/156.73 , insert^#(x, nil()) -> c_3() 304.12/156.73 , choose^#(x, cons(v, w), y, 0()) -> c_5() } 304.12/156.73 Weak Trs: 304.12/156.73 { sort(nil()) -> nil() 304.12/156.73 , sort(cons(x, y)) -> insert(x, sort(y)) 304.12/156.73 , insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 304.12/156.73 , choose(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 choose(x, cons(v, w), y, z) } 304.12/156.73 Obligation: 304.12/156.73 innermost runtime complexity 304.12/156.73 Answer: 304.12/156.73 YES(O(1),O(n^2)) 304.12/156.73 304.12/156.73 The following weak DPs constitute a sub-graph of the DG that is 304.12/156.73 closed under successors. The DPs are removed. 304.12/156.73 304.12/156.73 { sort^#(nil()) -> c_1() 304.12/156.73 , insert^#(x, nil()) -> c_3() 304.12/156.73 , choose^#(x, cons(v, w), y, 0()) -> c_5() } 304.12/156.73 304.12/156.73 We are left with following problem, upon which TcT provides the 304.12/156.73 certificate YES(O(1),O(n^2)). 304.12/156.73 304.12/156.73 Strict DPs: 304.12/156.73 { sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) 304.12/156.73 , choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) } 304.12/156.73 Weak Trs: 304.12/156.73 { sort(nil()) -> nil() 304.12/156.73 , sort(cons(x, y)) -> insert(x, sort(y)) 304.12/156.73 , insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 304.12/156.73 , choose(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 choose(x, cons(v, w), y, z) } 304.12/156.73 Obligation: 304.12/156.73 innermost runtime complexity 304.12/156.73 Answer: 304.12/156.73 YES(O(1),O(n^2)) 304.12/156.73 304.12/156.73 We use the processor 'matrix interpretation of dimension 2' to 304.12/156.73 orient following rules strictly. 304.12/156.73 304.12/156.73 DPs: 304.12/156.73 { 3: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) } 304.12/156.73 Trs: 304.12/156.73 { sort(cons(x, y)) -> insert(x, sort(y)) 304.12/156.73 , insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) } 304.12/156.73 304.12/156.73 Sub-proof: 304.12/156.73 ---------- 304.12/156.73 The following argument positions are usable: 304.12/156.73 Uargs(c_2) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_6) = {1}, 304.12/156.73 Uargs(c_7) = {1} 304.12/156.73 304.12/156.73 TcT has computed the following constructor-based matrix 304.12/156.73 interpretation satisfying not(EDA). 304.12/156.73 304.12/156.73 [sort](x1) = [4 0] x1 + [0] 304.12/156.73 [0 1] [0] 304.12/156.73 304.12/156.73 [nil] = [0] 304.12/156.73 [4] 304.12/156.73 304.12/156.73 [cons](x1, x2) = [1 1] x2 + [1] 304.12/156.73 [0 1] [4] 304.12/156.73 304.12/156.73 [insert](x1, x2) = [1 2] x2 + [0] 304.12/156.73 [0 1] [4] 304.12/156.73 304.12/156.73 [choose](x1, x2, x3, x4) = [1 2] x2 + [0] 304.12/156.73 [0 1] [4] 304.12/156.73 304.12/156.73 [0] = [0] 304.12/156.73 [0] 304.12/156.73 304.12/156.73 [s](x1) = [1] 304.12/156.73 [1] 304.12/156.73 304.12/156.73 [sort^#](x1) = [2 0] x1 + [0] 304.12/156.73 [0 0] [0] 304.12/156.73 304.12/156.73 [c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 304.12/156.73 [0 0] [0 0] [0] 304.12/156.73 304.12/156.73 [insert^#](x1, x2) = [0 0] x1 + [0 1] x2 + [0] 304.12/156.73 [4 4] [0 0] [0] 304.12/156.73 304.12/156.73 [c_4](x1) = [1 0] x1 + [0] 304.12/156.73 [0 0] [0] 304.12/156.73 304.12/156.73 [choose^#](x1, x2, x3, x4) = [0 0] x1 + [0 1] x2 + [0 0] x3 + [0] 304.12/156.73 [0 4] [2 0] [3 3] [0] 304.12/156.73 304.12/156.73 [c_6](x1) = [1 0] x1 + [1] 304.12/156.73 [0 0] [2] 304.12/156.73 304.12/156.73 [c_7](x1) = [1 0] x1 + [0] 304.12/156.73 [0 0] [3] 304.12/156.73 304.12/156.73 The order satisfies the following ordering constraints: 304.12/156.73 304.12/156.73 [sort(nil())] = [0] 304.12/156.73 [4] 304.12/156.73 >= [0] 304.12/156.73 [4] 304.12/156.73 = [nil()] 304.12/156.73 304.12/156.73 [sort(cons(x, y))] = [4 4] y + [4] 304.12/156.73 [0 1] [4] 304.12/156.73 > [4 2] y + [0] 304.12/156.73 [0 1] [4] 304.12/156.73 = [insert(x, sort(y))] 304.12/156.73 304.12/156.73 [insert(x, nil())] = [8] 304.12/156.73 [8] 304.12/156.73 > [5] 304.12/156.73 [8] 304.12/156.73 = [cons(x, nil())] 304.12/156.73 304.12/156.73 [insert(x, cons(v, w))] = [1 3] w + [9] 304.12/156.73 [0 1] [8] 304.12/156.73 >= [1 3] w + [9] 304.12/156.73 [0 1] [8] 304.12/156.73 = [choose(x, cons(v, w), x, v)] 304.12/156.73 304.12/156.73 [choose(x, cons(v, w), y, 0())] = [1 3] w + [9] 304.12/156.73 [0 1] [8] 304.12/156.73 > [1 2] w + [6] 304.12/156.73 [0 1] [8] 304.12/156.73 = [cons(x, cons(v, w))] 304.12/156.73 304.12/156.73 [choose(x, cons(v, w), 0(), s(z))] = [1 3] w + [9] 304.12/156.73 [0 1] [8] 304.12/156.73 > [1 3] w + [5] 304.12/156.73 [0 1] [8] 304.12/156.73 = [cons(v, insert(x, w))] 304.12/156.73 304.12/156.73 [choose(x, cons(v, w), s(y), s(z))] = [1 3] w + [9] 304.12/156.73 [0 1] [8] 304.12/156.73 >= [1 3] w + [9] 304.12/156.73 [0 1] [8] 304.12/156.73 = [choose(x, cons(v, w), y, z)] 304.12/156.73 304.12/156.73 [sort^#(cons(x, y))] = [2 2] y + [2] 304.12/156.73 [0 0] [0] 304.12/156.73 >= [2 1] y + [2] 304.12/156.73 [0 0] [0] 304.12/156.73 = [c_2(insert^#(x, sort(y)), sort^#(y))] 304.12/156.73 304.12/156.73 [insert^#(x, cons(v, w))] = [0 0] x + [0 1] w + [4] 304.12/156.73 [4 4] [0 0] [0] 304.12/156.73 >= [0 1] w + [4] 304.12/156.73 [0 0] [0] 304.12/156.73 = [c_4(choose^#(x, cons(v, w), x, v))] 304.12/156.73 304.12/156.73 [choose^#(x, cons(v, w), 0(), s(z))] = [0 0] x + [0 1] w + [4] 304.12/156.73 [0 4] [2 2] [2] 304.12/156.73 > [0 1] w + [1] 304.12/156.73 [0 0] [2] 304.12/156.73 = [c_6(insert^#(x, w))] 304.12/156.73 304.12/156.73 [choose^#(x, cons(v, w), s(y), s(z))] = [0 0] x + [0 1] w + [4] 304.12/156.73 [0 4] [2 2] [8] 304.12/156.73 >= [0 1] w + [4] 304.12/156.73 [0 0] [3] 304.12/156.73 = [c_7(choose^#(x, cons(v, w), y, z))] 304.12/156.73 304.12/156.73 304.12/156.73 The strictly oriented rules are moved into the weak component. 304.12/156.73 304.12/156.73 We are left with following problem, upon which TcT provides the 304.12/156.73 certificate YES(O(1),O(n^2)). 304.12/156.73 304.12/156.73 Strict DPs: 304.12/156.73 { sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) } 304.12/156.73 Weak DPs: 304.12/156.73 { choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) } 304.12/156.73 Weak Trs: 304.12/156.73 { sort(nil()) -> nil() 304.12/156.73 , sort(cons(x, y)) -> insert(x, sort(y)) 304.12/156.73 , insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 304.12/156.73 , choose(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 choose(x, cons(v, w), y, z) } 304.12/156.73 Obligation: 304.12/156.73 innermost runtime complexity 304.12/156.73 Answer: 304.12/156.73 YES(O(1),O(n^2)) 304.12/156.73 304.12/156.73 We use the processor 'matrix interpretation of dimension 2' to 304.12/156.73 orient following rules strictly. 304.12/156.73 304.12/156.73 DPs: 304.12/156.73 { 1: sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , 4: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) } 304.12/156.73 Trs: 304.12/156.73 { insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) } 304.12/156.73 304.12/156.73 Sub-proof: 304.12/156.73 ---------- 304.12/156.73 The following argument positions are usable: 304.12/156.73 Uargs(c_2) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_6) = {1}, 304.12/156.73 Uargs(c_7) = {1} 304.12/156.73 304.12/156.73 TcT has computed the following constructor-based matrix 304.12/156.73 interpretation satisfying not(EDA). 304.12/156.73 304.12/156.73 [sort](x1) = [6 4] x1 + [0] 304.12/156.73 [0 1] [0] 304.12/156.73 304.12/156.73 [nil] = [0] 304.12/156.73 [0] 304.12/156.73 304.12/156.73 [cons](x1, x2) = [1 1] x2 + [0] 304.12/156.73 [0 1] [1] 304.12/156.73 304.12/156.73 [insert](x1, x2) = [1 6] x2 + [4] 304.12/156.73 [0 1] [1] 304.12/156.73 304.12/156.73 [choose](x1, x2, x3, x4) = [1 6] x2 + [2] 304.12/156.73 [0 1] [1] 304.12/156.73 304.12/156.73 [0] = [2] 304.12/156.73 [0] 304.12/156.73 304.12/156.73 [s](x1) = [0 0] x1 + [0] 304.12/156.73 [0 1] [0] 304.12/156.73 304.12/156.73 [sort^#](x1) = [3 5] x1 + [0] 304.12/156.73 [4 0] [0] 304.12/156.73 304.12/156.73 [c_2](x1, x2) = [2 0] x1 + [1 0] x2 + [1] 304.12/156.73 [0 0] [0 0] [0] 304.12/156.73 304.12/156.73 [insert^#](x1, x2) = [0 1] x2 + [0] 304.12/156.73 [0 0] [4] 304.12/156.73 304.12/156.73 [c_4](x1) = [1 0] x1 + [0] 304.12/156.73 [0 0] [3] 304.12/156.73 304.12/156.73 [choose^#](x1, x2, x3, x4) = [0 0] x1 + [0 1] x2 + [0 0] x3 + [0] 304.12/156.73 [4 4] [0 0] [4 4] [0] 304.12/156.73 304.12/156.73 [c_6](x1) = [1 0] x1 + [0] 304.12/156.73 [0 0] [3] 304.12/156.73 304.12/156.73 [c_7](x1) = [1 0] x1 + [0] 304.12/156.73 [0 0] [0] 304.12/156.73 304.12/156.73 The order satisfies the following ordering constraints: 304.12/156.73 304.12/156.73 [sort(nil())] = [0] 304.12/156.73 [0] 304.12/156.73 >= [0] 304.12/156.73 [0] 304.12/156.73 = [nil()] 304.12/156.73 304.12/156.73 [sort(cons(x, y))] = [6 10] y + [4] 304.12/156.73 [0 1] [1] 304.12/156.73 >= [6 10] y + [4] 304.12/156.73 [0 1] [1] 304.12/156.73 = [insert(x, sort(y))] 304.12/156.73 304.12/156.73 [insert(x, nil())] = [4] 304.12/156.73 [1] 304.12/156.73 > [0] 304.12/156.73 [1] 304.12/156.73 = [cons(x, nil())] 304.12/156.73 304.12/156.73 [insert(x, cons(v, w))] = [1 7] w + [10] 304.12/156.73 [0 1] [2] 304.12/156.73 > [1 7] w + [8] 304.12/156.73 [0 1] [2] 304.12/156.73 = [choose(x, cons(v, w), x, v)] 304.12/156.73 304.12/156.73 [choose(x, cons(v, w), y, 0())] = [1 7] w + [8] 304.12/156.73 [0 1] [2] 304.12/156.73 > [1 2] w + [1] 304.12/156.73 [0 1] [2] 304.12/156.73 = [cons(x, cons(v, w))] 304.12/156.73 304.12/156.73 [choose(x, cons(v, w), 0(), s(z))] = [1 7] w + [8] 304.12/156.73 [0 1] [2] 304.12/156.73 > [1 7] w + [5] 304.12/156.73 [0 1] [2] 304.12/156.73 = [cons(v, insert(x, w))] 304.12/156.73 304.12/156.73 [choose(x, cons(v, w), s(y), s(z))] = [1 7] w + [8] 304.12/156.73 [0 1] [2] 304.12/156.73 >= [1 7] w + [8] 304.12/156.73 [0 1] [2] 304.12/156.73 = [choose(x, cons(v, w), y, z)] 304.12/156.73 304.12/156.73 [sort^#(cons(x, y))] = [3 8] y + [5] 304.12/156.73 [4 4] [0] 304.12/156.73 > [3 7] y + [1] 304.12/156.73 [0 0] [0] 304.12/156.73 = [c_2(insert^#(x, sort(y)), sort^#(y))] 304.12/156.73 304.12/156.73 [insert^#(x, cons(v, w))] = [0 1] w + [1] 304.12/156.73 [0 0] [4] 304.12/156.73 >= [0 1] w + [1] 304.12/156.73 [0 0] [3] 304.12/156.73 = [c_4(choose^#(x, cons(v, w), x, v))] 304.12/156.73 304.12/156.73 [choose^#(x, cons(v, w), 0(), s(z))] = [0 0] x + [0 1] w + [1] 304.12/156.73 [4 4] [0 0] [8] 304.12/156.73 > [0 1] w + [0] 304.12/156.73 [0 0] [3] 304.12/156.73 = [c_6(insert^#(x, w))] 304.12/156.73 304.12/156.73 [choose^#(x, cons(v, w), s(y), s(z))] = [0 0] x + [0 0] y + [0 1] w + [1] 304.12/156.73 [4 4] [0 4] [0 0] [0] 304.12/156.73 >= [0 1] w + [1] 304.12/156.73 [0 0] [0] 304.12/156.73 = [c_7(choose^#(x, cons(v, w), y, z))] 304.12/156.73 304.12/156.73 304.12/156.73 We return to the main proof. Consider the set of all dependency 304.12/156.73 pairs 304.12/156.73 304.12/156.73 : 304.12/156.73 { 1: sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , 2: insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , 3: choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) 304.12/156.73 , 4: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) } 304.12/156.73 304.12/156.73 Processor 'matrix interpretation of dimension 2' induces the 304.12/156.73 complexity certificate YES(?,O(n^2)) on application of dependency 304.12/156.73 pairs {1,4}. These cover all (indirect) predecessors of dependency 304.12/156.73 pairs {1,2,4}, their number of application is equally bounded. The 304.12/156.73 dependency pairs are shifted into the weak component. 304.12/156.73 304.12/156.73 We are left with following problem, upon which TcT provides the 304.12/156.73 certificate YES(O(1),O(n^2)). 304.12/156.73 304.12/156.73 Strict DPs: 304.12/156.73 { choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) } 304.12/156.73 Weak DPs: 304.12/156.73 { sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) } 304.12/156.73 Weak Trs: 304.12/156.73 { sort(nil()) -> nil() 304.12/156.73 , sort(cons(x, y)) -> insert(x, sort(y)) 304.12/156.73 , insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 304.12/156.73 , choose(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 choose(x, cons(v, w), y, z) } 304.12/156.73 Obligation: 304.12/156.73 innermost runtime complexity 304.12/156.73 Answer: 304.12/156.73 YES(O(1),O(n^2)) 304.12/156.73 304.12/156.73 We use the processor 'polynomial interpretation' to orient 304.12/156.73 following rules strictly. 304.12/156.73 304.12/156.73 DPs: 304.12/156.73 { 1: choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) 304.12/156.73 , 2: sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) } 304.12/156.73 304.12/156.73 Sub-proof: 304.12/156.73 ---------- 304.12/156.73 We consider the following typing: 304.12/156.73 304.12/156.73 sort :: b -> b 304.12/156.73 nil :: b 304.12/156.73 cons :: (c,b) -> b 304.12/156.73 insert :: (c,b) -> b 304.12/156.73 choose :: (c,b,c,c) -> b 304.12/156.73 0 :: c 304.12/156.73 s :: c -> c 304.12/156.73 sort^# :: b -> a 304.12/156.73 c_2 :: (d,a) -> a 304.12/156.73 insert^# :: (c,b) -> d 304.12/156.73 c_4 :: e -> d 304.12/156.73 choose^# :: (c,b,c,c) -> e 304.12/156.73 c_6 :: d -> e 304.12/156.73 c_7 :: e -> e 304.12/156.73 304.12/156.73 The following argument positions are considered usable: 304.12/156.73 304.12/156.73 Uargs(c_2) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_6) = {1}, 304.12/156.73 Uargs(c_7) = {1} 304.12/156.73 304.12/156.73 TcT has computed the following constructor-restricted 304.12/156.73 typedpolynomial interpretation. 304.12/156.73 304.12/156.73 [sort](x1) = x1 304.12/156.73 304.12/156.73 [nil]() = 0 304.12/156.73 304.12/156.73 [cons](x1, x2) = 1 + x1 + x2 304.12/156.73 304.12/156.73 [insert](x1, x2) = 1 + x1 + x2 304.12/156.73 304.12/156.73 [choose](x1, x2, x3, x4) = 1 + x1 + x2 304.12/156.73 304.12/156.73 [0]() = 0 304.12/156.73 304.12/156.73 [s](x1) = 2 + x1 304.12/156.73 304.12/156.73 [sort^#](x1) = 2*x1 + x1^2 304.12/156.73 304.12/156.73 [c_2](x1, x2) = x1 + x2 304.12/156.73 304.12/156.73 [insert^#](x1, x2) = 2*x1 + 2*x1*x2 304.12/156.73 304.12/156.73 [c_4](x1) = x1 304.12/156.73 304.12/156.73 [choose^#](x1, x2, x3, x4) = 2*x1*x2 + 2*x3 304.12/156.73 304.12/156.73 [c_6](x1) = x1 304.12/156.73 304.12/156.73 [c_7](x1) = x1 304.12/156.73 304.12/156.73 304.12/156.73 This order satisfies the following ordering constraints. 304.12/156.73 304.12/156.73 [sort(nil())] = 304.12/156.73 >= 304.12/156.73 = [nil()] 304.12/156.73 304.12/156.73 [sort(cons(x, y))] = 1 + x + y 304.12/156.73 >= 1 + x + y 304.12/156.73 = [insert(x, sort(y))] 304.12/156.73 304.12/156.73 [insert(x, nil())] = 1 + x 304.12/156.73 >= 1 + x 304.12/156.73 = [cons(x, nil())] 304.12/156.73 304.12/156.73 [insert(x, cons(v, w))] = 2 + x + v + w 304.12/156.73 >= 2 + x + v + w 304.12/156.73 = [choose(x, cons(v, w), x, v)] 304.12/156.73 304.12/156.73 [choose(x, cons(v, w), y, 0())] = 2 + x + v + w 304.12/156.73 >= 2 + x + v + w 304.12/156.73 = [cons(x, cons(v, w))] 304.12/156.73 304.12/156.73 [choose(x, cons(v, w), 0(), s(z))] = 2 + x + v + w 304.12/156.73 >= 2 + v + x + w 304.12/156.73 = [cons(v, insert(x, w))] 304.12/156.73 304.12/156.73 [choose(x, cons(v, w), s(y), s(z))] = 2 + x + v + w 304.12/156.73 >= 2 + x + v + w 304.12/156.73 = [choose(x, cons(v, w), y, z)] 304.12/156.73 304.12/156.73 [sort^#(cons(x, y))] = 3 + 4*x + 4*y + x^2 + x*y + y*x + y^2 304.12/156.73 > 2*x + 2*x*y + 2*y + y^2 304.12/156.73 = [c_2(insert^#(x, sort(y)), sort^#(y))] 304.12/156.73 304.12/156.73 [insert^#(x, cons(v, w))] = 4*x + 2*x*v + 2*x*w 304.12/156.73 >= 4*x + 2*x*v + 2*x*w 304.12/156.73 = [c_4(choose^#(x, cons(v, w), x, v))] 304.12/156.73 304.12/156.73 [choose^#(x, cons(v, w), 0(), s(z))] = 2*x + 2*x*v + 2*x*w 304.12/156.73 >= 2*x + 2*x*w 304.12/156.73 = [c_6(insert^#(x, w))] 304.12/156.73 304.12/156.73 [choose^#(x, cons(v, w), s(y), s(z))] = 2*x + 2*x*v + 2*x*w + 4 + 2*y 304.12/156.73 > 2*x + 2*x*v + 2*x*w + 2*y 304.12/156.73 = [c_7(choose^#(x, cons(v, w), y, z))] 304.12/156.73 304.12/156.73 304.12/156.73 The strictly oriented rules are moved into the weak component. 304.12/156.73 304.12/156.73 We are left with following problem, upon which TcT provides the 304.12/156.73 certificate YES(O(1),O(1)). 304.12/156.73 304.12/156.73 Weak DPs: 304.12/156.73 { sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) 304.12/156.73 , choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) } 304.12/156.73 Weak Trs: 304.12/156.73 { sort(nil()) -> nil() 304.12/156.73 , sort(cons(x, y)) -> insert(x, sort(y)) 304.12/156.73 , insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 304.12/156.73 , choose(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 choose(x, cons(v, w), y, z) } 304.12/156.73 Obligation: 304.12/156.73 innermost runtime complexity 304.12/156.73 Answer: 304.12/156.73 YES(O(1),O(1)) 304.12/156.73 304.12/156.73 The following weak DPs constitute a sub-graph of the DG that is 304.12/156.73 closed under successors. The DPs are removed. 304.12/156.73 304.12/156.73 { sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) 304.12/156.73 , insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v)) 304.12/156.73 , choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) 304.12/156.73 , choose^#(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 c_7(choose^#(x, cons(v, w), y, z)) } 304.12/156.73 304.12/156.73 We are left with following problem, upon which TcT provides the 304.12/156.73 certificate YES(O(1),O(1)). 304.12/156.73 304.12/156.73 Weak Trs: 304.12/156.73 { sort(nil()) -> nil() 304.12/156.73 , sort(cons(x, y)) -> insert(x, sort(y)) 304.12/156.73 , insert(x, nil()) -> cons(x, nil()) 304.12/156.73 , insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v) 304.12/156.73 , choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) 304.12/156.73 , choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)) 304.12/156.73 , choose(x, cons(v, w), s(y), s(z)) -> 304.12/156.73 choose(x, cons(v, w), y, z) } 304.12/156.73 Obligation: 304.12/156.73 innermost runtime complexity 304.12/156.73 Answer: 304.12/156.73 YES(O(1),O(1)) 304.12/156.73 304.12/156.73 No rule is usable, rules are removed from the input problem. 304.12/156.73 304.12/156.73 We are left with following problem, upon which TcT provides the 304.12/156.73 certificate YES(O(1),O(1)). 304.12/156.73 304.12/156.73 Rules: Empty 304.12/156.73 Obligation: 304.12/156.73 innermost runtime complexity 304.12/156.73 Answer: 304.12/156.73 YES(O(1),O(1)) 304.12/156.73 304.12/156.73 Empty rules are trivially bounded 304.12/156.73 304.12/156.73 Hurray, we answered YES(O(1),O(n^2)) 304.29/156.81 EOF