YES(O(1),O(n^2)) 162.85/60.07 YES(O(1),O(n^2)) 162.85/60.07 162.85/60.07 We are left with following problem, upon which TcT provides the 162.85/60.07 certificate YES(O(1),O(n^2)). 162.85/60.07 162.85/60.07 Strict Trs: 162.85/60.07 { ++(x, nil()) -> x 162.85/60.07 , ++(++(x, y), z) -> ++(x, ++(y, z)) 162.85/60.07 , ++(nil(), y) -> y 162.85/60.07 , ++(.(x, y), z) -> .(x, ++(y, z)) } 162.85/60.07 Obligation: 162.85/60.07 derivational complexity 162.85/60.07 Answer: 162.85/60.07 YES(O(1),O(n^2)) 162.85/60.07 162.85/60.07 We use the processor 'matrix interpretation of dimension 1' to 162.85/60.07 orient following rules strictly. 162.85/60.07 162.85/60.07 Trs: 162.85/60.07 { ++(x, nil()) -> x 162.85/60.07 , ++(nil(), y) -> y } 162.85/60.07 162.85/60.07 The induced complexity on above rules (modulo remaining rules) is 162.85/60.07 YES(?,O(n^1)) . These rules are moved into the corresponding weak 162.85/60.07 component(s). 162.85/60.07 162.85/60.07 Sub-proof: 162.85/60.07 ---------- 162.85/60.07 TcT has computed the following triangular matrix interpretation. 162.85/60.07 162.85/60.07 [++](x1, x2) = [1] x1 + [1] x2 + [0] 162.85/60.07 162.85/60.07 [nil] = [2] 162.85/60.07 162.85/60.07 [.](x1, x2) = [1] x1 + [1] x2 + [0] 162.85/60.07 162.85/60.07 The order satisfies the following ordering constraints: 162.85/60.07 162.85/60.07 [++(x, nil())] = [1] x + [2] 162.85/60.07 > [1] x + [0] 162.85/60.07 = [x] 162.85/60.07 162.85/60.07 [++(++(x, y), z)] = [1] y + [1] x + [1] z + [0] 162.85/60.07 >= [1] y + [1] x + [1] z + [0] 162.85/60.07 = [++(x, ++(y, z))] 162.85/60.07 162.85/60.07 [++(nil(), y)] = [1] y + [2] 162.85/60.07 > [1] y + [0] 162.85/60.07 = [y] 162.85/60.07 162.85/60.07 [++(.(x, y), z)] = [1] y + [1] x + [1] z + [0] 162.85/60.07 >= [1] y + [1] x + [1] z + [0] 162.85/60.07 = [.(x, ++(y, z))] 162.85/60.07 162.85/60.07 162.85/60.07 We return to the main proof. 162.85/60.07 162.85/60.07 We are left with following problem, upon which TcT provides the 162.85/60.07 certificate YES(O(1),O(n^2)). 162.85/60.07 162.85/60.07 Strict Trs: 162.85/60.07 { ++(++(x, y), z) -> ++(x, ++(y, z)) 162.85/60.07 , ++(.(x, y), z) -> .(x, ++(y, z)) } 162.85/60.07 Weak Trs: 162.85/60.07 { ++(x, nil()) -> x 162.85/60.07 , ++(nil(), y) -> y } 162.85/60.07 Obligation: 162.85/60.07 derivational complexity 162.85/60.07 Answer: 162.85/60.07 YES(O(1),O(n^2)) 162.85/60.07 162.85/60.07 We use the processor 'matrix interpretation of dimension 2' to 162.85/60.07 orient following rules strictly. 162.85/60.07 162.85/60.07 Trs: { ++(.(x, y), z) -> .(x, ++(y, z)) } 162.85/60.07 162.85/60.07 The induced complexity on above rules (modulo remaining rules) is 162.85/60.07 YES(?,O(n^2)) . These rules are moved into the corresponding weak 162.85/60.07 component(s). 162.85/60.07 162.85/60.07 Sub-proof: 162.85/60.07 ---------- 162.85/60.07 TcT has computed the following triangular matrix interpretation. 162.85/60.07 162.85/60.07 [++](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 162.85/60.07 [0 1] [0 1] [0] 162.85/60.07 162.85/60.07 [nil] = [1] 162.85/60.07 [2] 162.85/60.07 162.85/60.07 [.](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 162.85/60.07 [0 1] [0 1] [1] 162.85/60.07 162.85/60.07 The order satisfies the following ordering constraints: 162.85/60.07 162.85/60.07 [++(x, nil())] = [1 1] x + [1] 162.85/60.07 [0 1] [2] 162.85/60.07 > [1 0] x + [0] 162.85/60.07 [0 1] [0] 162.85/60.07 = [x] 162.85/60.07 162.85/60.07 [++(++(x, y), z)] = [1 1] y + [1 2] x + [1 0] z + [0] 162.85/60.07 [0 1] [0 1] [0 1] [0] 162.85/60.07 >= [1 1] y + [1 1] x + [1 0] z + [0] 162.85/60.07 [0 1] [0 1] [0 1] [0] 162.85/60.07 = [++(x, ++(y, z))] 162.85/60.07 162.85/60.07 [++(nil(), y)] = [1 0] y + [3] 162.85/60.07 [0 1] [2] 162.85/60.07 > [1 0] y + [0] 162.85/60.07 [0 1] [0] 162.85/60.07 = [y] 162.85/60.07 162.85/60.07 [++(.(x, y), z)] = [1 1] y + [1 2] x + [1 0] z + [1] 162.85/60.07 [0 1] [0 1] [0 1] [1] 162.85/60.07 > [1 1] y + [1 1] x + [1 0] z + [0] 162.85/60.07 [0 1] [0 1] [0 1] [1] 162.85/60.07 = [.(x, ++(y, z))] 162.85/60.07 162.85/60.07 162.85/60.07 We return to the main proof. 162.85/60.07 162.85/60.07 We are left with following problem, upon which TcT provides the 162.85/60.07 certificate YES(O(1),O(n^2)). 162.85/60.07 162.85/60.07 Strict Trs: { ++(++(x, y), z) -> ++(x, ++(y, z)) } 162.85/60.07 Weak Trs: 162.85/60.07 { ++(x, nil()) -> x 162.85/60.07 , ++(nil(), y) -> y 162.85/60.07 , ++(.(x, y), z) -> .(x, ++(y, z)) } 162.85/60.07 Obligation: 162.85/60.07 derivational complexity 162.85/60.07 Answer: 162.85/60.07 YES(O(1),O(n^2)) 162.85/60.07 162.85/60.07 We use the processor 'matrix interpretation of dimension 2' to 162.85/60.07 orient following rules strictly. 162.85/60.07 162.85/60.07 Trs: { ++(++(x, y), z) -> ++(x, ++(y, z)) } 162.85/60.07 162.85/60.07 The induced complexity on above rules (modulo remaining rules) is 162.85/60.07 YES(?,O(n^2)) . These rules are moved into the corresponding weak 162.85/60.07 component(s). 162.85/60.07 162.85/60.07 Sub-proof: 162.85/60.07 ---------- 162.85/60.07 TcT has computed the following triangular matrix interpretation. 162.85/60.07 162.85/60.07 [++](x1, x2) = [1 2] x1 + [1 0] x2 + [0] 162.85/60.07 [0 1] [0 1] [2] 162.85/60.07 162.85/60.07 [nil] = [1] 162.85/60.07 [1] 162.85/60.07 162.85/60.07 [.](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 162.85/60.07 [0 1] [0 1] [2] 162.85/60.07 162.85/60.07 The order satisfies the following ordering constraints: 162.85/60.07 162.85/60.07 [++(x, nil())] = [1 2] x + [1] 162.85/60.07 [0 1] [3] 162.85/60.07 > [1 0] x + [0] 162.85/60.07 [0 1] [0] 162.85/60.07 = [x] 162.85/60.07 162.85/60.07 [++(++(x, y), z)] = [1 2] y + [1 4] x + [1 0] z + [4] 162.85/60.07 [0 1] [0 1] [0 1] [4] 162.85/60.07 > [1 2] y + [1 2] x + [1 0] z + [0] 162.85/60.07 [0 1] [0 1] [0 1] [4] 162.85/60.07 = [++(x, ++(y, z))] 162.85/60.07 162.85/60.07 [++(nil(), y)] = [1 0] y + [3] 162.85/60.07 [0 1] [3] 162.85/60.07 > [1 0] y + [0] 162.85/60.07 [0 1] [0] 162.85/60.07 = [y] 162.85/60.07 162.85/60.07 [++(.(x, y), z)] = [1 2] y + [1 3] x + [1 0] z + [4] 162.85/60.07 [0 1] [0 1] [0 1] [4] 162.85/60.07 > [1 2] y + [1 1] x + [1 0] z + [0] 162.85/60.07 [0 1] [0 1] [0 1] [4] 162.85/60.07 = [.(x, ++(y, z))] 162.85/60.07 162.85/60.07 162.85/60.07 We return to the main proof. 162.85/60.07 162.85/60.07 We are left with following problem, upon which TcT provides the 162.85/60.07 certificate YES(O(1),O(1)). 162.85/60.07 162.85/60.07 Weak Trs: 162.85/60.07 { ++(x, nil()) -> x 162.85/60.07 , ++(++(x, y), z) -> ++(x, ++(y, z)) 162.85/60.07 , ++(nil(), y) -> y 162.85/60.07 , ++(.(x, y), z) -> .(x, ++(y, z)) } 162.85/60.07 Obligation: 162.85/60.07 derivational complexity 162.85/60.07 Answer: 162.85/60.07 YES(O(1),O(1)) 162.85/60.07 162.85/60.07 Empty rules are trivially bounded 162.85/60.07 162.85/60.07 Hurray, we answered YES(O(1),O(n^2)) 162.85/60.08 EOF