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