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