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