YES(O(1),O(n^10)) 218.97/60.03 YES(O(1),O(n^10)) 218.97/60.03 218.97/60.03 We are left with following problem, upon which TcT provides the 218.97/60.03 certificate YES(O(1),O(n^10)). 218.97/60.03 218.97/60.03 Strict Trs: 218.97/60.03 { rev(rev(x)) -> x 218.97/60.03 , rev(nil()) -> nil() 218.97/60.03 , rev(++(x, y)) -> ++(rev(y), rev(x)) 218.97/60.03 , ++(x, nil()) -> x 218.97/60.03 , ++(x, ++(y, z)) -> ++(++(x, y), z) 218.97/60.03 , ++(nil(), y) -> y 218.97/60.03 , ++(.(x, y), z) -> .(x, ++(y, z)) 218.97/60.03 , make(x) -> .(x, nil()) } 218.97/60.03 Obligation: 218.97/60.03 derivational complexity 218.97/60.03 Answer: 218.97/60.03 YES(O(1),O(n^10)) 218.97/60.03 218.97/60.03 We use the processor 'matrix interpretation of dimension 2' to 218.97/60.03 orient following rules strictly. 218.97/60.03 218.97/60.03 Trs: 218.97/60.03 { rev(rev(x)) -> x 218.97/60.03 , rev(nil()) -> nil() 218.97/60.03 , rev(++(x, y)) -> ++(rev(y), rev(x)) 218.97/60.03 , ++(x, nil()) -> x 218.97/60.03 , ++(nil(), y) -> y 218.97/60.03 , make(x) -> .(x, nil()) } 218.97/60.03 218.97/60.03 The induced complexity on above rules (modulo remaining rules) is 218.97/60.03 YES(?,O(n^2)) . These rules are removed from the problem. Note that 218.97/60.03 none of the weakly oriented rules is size-increasing. The overall 218.97/60.03 complexity is obtained by composition . 218.97/60.03 218.97/60.03 Sub-proof: 218.97/60.03 ---------- 218.97/60.03 TcT has computed the following triangular matrix interpretation. 218.97/60.03 218.97/60.03 [rev](x1) = [1 1] x1 + [1] 218.97/60.03 [0 1] [0] 218.97/60.03 218.97/60.03 [nil] = [0] 218.97/60.03 [0] 218.97/60.03 218.97/60.03 [++](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 218.97/60.03 [0 1] [0 1] [2] 218.97/60.03 218.97/60.03 [.](x1, x2) = [1 2] x1 + [1 0] x2 + [0] 218.97/60.03 [0 1] [0 0] [2] 218.97/60.03 218.97/60.03 [make](x1) = [1 2] x1 + [1] 218.97/60.03 [0 1] [2] 218.97/60.03 218.97/60.03 The order satisfies the following ordering constraints: 218.97/60.03 218.97/60.03 [rev(rev(x))] = [1 2] x + [2] 218.97/60.03 [0 1] [0] 218.97/60.03 > [1 0] x + [0] 218.97/60.03 [0 1] [0] 218.97/60.03 = [x] 218.97/60.03 218.97/60.03 [rev(nil())] = [1] 218.97/60.03 [0] 218.97/60.03 > [0] 218.97/60.03 [0] 218.97/60.03 = [nil()] 218.97/60.03 218.97/60.03 [rev(++(x, y))] = [1 1] x + [1 1] y + [5] 218.97/60.03 [0 1] [0 1] [2] 218.97/60.03 > [1 1] x + [1 1] y + [4] 218.97/60.03 [0 1] [0 1] [2] 218.97/60.03 = [++(rev(y), rev(x))] 218.97/60.03 218.97/60.03 [++(x, nil())] = [1 0] x + [2] 218.97/60.03 [0 1] [2] 218.97/60.03 > [1 0] x + [0] 218.97/60.03 [0 1] [0] 218.97/60.03 = [x] 218.97/60.03 218.97/60.03 [++(x, ++(y, z))] = [1 0] x + [1 0] y + [1 0] z + [4] 218.97/60.03 [0 1] [0 1] [0 1] [4] 218.97/60.03 >= [1 0] x + [1 0] y + [1 0] z + [4] 218.97/60.03 [0 1] [0 1] [0 1] [4] 218.97/60.03 = [++(++(x, y), z)] 218.97/60.03 218.97/60.03 [++(nil(), y)] = [1 0] y + [2] 218.97/60.03 [0 1] [2] 218.97/60.03 > [1 0] y + [0] 218.97/60.03 [0 1] [0] 218.97/60.03 = [y] 218.97/60.03 218.97/60.03 [++(.(x, y), z)] = [1 2] x + [1 0] y + [1 0] z + [2] 218.97/60.03 [0 1] [0 0] [0 1] [4] 218.97/60.03 >= [1 2] x + [1 0] y + [1 0] z + [2] 218.97/60.03 [0 1] [0 0] [0 0] [2] 218.97/60.03 = [.(x, ++(y, z))] 218.97/60.03 218.97/60.03 [make(x)] = [1 2] x + [1] 218.97/60.03 [0 1] [2] 218.97/60.03 > [1 2] x + [0] 218.97/60.03 [0 1] [2] 218.97/60.03 = [.(x, nil())] 218.97/60.03 218.97/60.03 218.97/60.03 We return to the main proof. 218.97/60.03 218.97/60.03 We are left with following problem, upon which TcT provides the 218.97/60.03 certificate YES(O(1),O(n^4)). 218.97/60.03 218.97/60.03 Strict Trs: 218.97/60.03 { ++(x, ++(y, z)) -> ++(++(x, y), z) 218.97/60.03 , ++(.(x, y), z) -> .(x, ++(y, z)) } 218.97/60.03 Obligation: 218.97/60.03 derivational complexity 218.97/60.03 Answer: 218.97/60.03 YES(O(1),O(n^4)) 218.97/60.03 218.97/60.03 We use the processor 'matrix interpretation of dimension 2' to 218.97/60.03 orient following rules strictly. 218.97/60.03 218.97/60.03 Trs: { ++(x, ++(y, z)) -> ++(++(x, y), z) } 218.97/60.03 218.97/60.03 The induced complexity on above rules (modulo remaining rules) is 218.97/60.03 YES(?,O(n^2)) . These rules are removed from the problem. Note that 218.97/60.03 no rule is size-increasing. The overall complexity is obtained by 218.97/60.03 multiplication . 218.97/60.03 218.97/60.03 Sub-proof: 218.97/60.03 ---------- 218.97/60.03 TcT has computed the following triangular matrix interpretation. 218.97/60.03 218.97/60.03 [++](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 218.97/60.03 [0 1] [0 1] [1] 218.97/60.03 218.97/60.03 [.](x1, x2) = [1 2] x1 + [1 0] x2 + [0] 218.97/60.03 [0 1] [0 0] [0] 218.97/60.03 218.97/60.03 The order satisfies the following ordering constraints: 218.97/60.03 218.97/60.03 [++(x, ++(y, z))] = [1 0] x + [1 1] y + [1 2] z + [1] 218.97/60.03 [0 1] [0 1] [0 1] [2] 218.97/60.03 > [1 0] x + [1 1] y + [1 1] z + [0] 218.97/60.03 [0 1] [0 1] [0 1] [2] 218.97/60.03 = [++(++(x, y), z)] 218.97/60.03 218.97/60.03 [++(.(x, y), z)] = [1 2] x + [1 0] y + [1 1] z + [0] 218.97/60.03 [0 1] [0 0] [0 1] [1] 218.97/60.03 >= [1 2] x + [1 0] y + [1 1] z + [0] 218.97/60.03 [0 1] [0 0] [0 0] [0] 218.97/60.03 = [.(x, ++(y, z))] 218.97/60.03 218.97/60.03 218.97/60.03 We return to the main proof. 218.97/60.03 218.97/60.03 We are left with following problem, upon which TcT provides the 218.97/60.03 certificate YES(?,O(n^2)). 218.97/60.03 218.97/60.03 Strict Trs: { ++(.(x, y), z) -> .(x, ++(y, z)) } 218.97/60.03 Obligation: 218.97/60.03 derivational complexity 218.97/60.03 Answer: 218.97/60.03 YES(?,O(n^2)) 218.97/60.03 218.97/60.03 TcT has computed the following triangular matrix interpretation. 218.97/60.03 218.97/60.03 [++](x1, x2) = [1 4] x1 + [1 7] x2 + [0] 218.97/60.03 [0 1] [0 0] [0] 218.97/60.03 218.97/60.03 [.](x1, x2) = [1 7] x1 + [1 4] x2 + [0] 218.97/60.03 [0 1] [0 1] [2] 218.97/60.03 218.97/60.03 The order satisfies the following ordering constraints: 218.97/60.03 218.97/60.03 [++(.(x, y), z)] = [1 11] x + [1 8] y + [1 7] z + [8] 218.97/60.03 [0 1] [0 1] [0 0] [2] 218.97/60.03 > [1 7] x + [1 8] y + [1 7] z + [0] 218.97/60.03 [0 1] [0 1] [0 0] [2] 218.97/60.03 = [.(x, ++(y, z))] 218.97/60.03 218.97/60.03 218.97/60.03 Hurray, we answered YES(O(1),O(n^10)) 218.97/60.07 EOF