YES(O(1),O(n^5)) 1150.89/297.11 YES(O(1),O(n^5)) 1150.89/297.11 1150.89/297.11 We are left with following problem, upon which TcT provides the 1150.89/297.11 certificate YES(O(1),O(n^5)). 1150.89/297.11 1150.89/297.11 Strict Trs: 1150.89/297.11 { +(+(x, y), z) -> +(x, +(y, z)) 1150.89/297.11 , +(p1(), +(p1(), x)) -> +(p2(), x) 1150.89/297.11 , +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x) 1150.89/297.11 , +(p1(), +(p2(), p2())) -> p5() 1150.89/297.11 , +(p1(), p1()) -> p2() 1150.89/297.11 , +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)) 1150.89/297.11 , +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)) 1150.89/297.11 , +(p2(), +(p2(), p2())) -> +(p1(), p5()) 1150.89/297.11 , +(p2(), p1()) -> +(p1(), p2()) 1150.89/297.11 , +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)) 1150.89/297.11 , +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)) 1150.89/297.11 , +(p5(), +(p5(), x)) -> +(p10(), x) 1150.89/297.11 , +(p5(), p1()) -> +(p1(), p5()) 1150.89/297.11 , +(p5(), p2()) -> +(p2(), p5()) 1150.89/297.11 , +(p5(), p5()) -> p10() 1150.89/297.11 , +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)) 1150.89/297.11 , +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)) 1150.89/297.11 , +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)) 1150.89/297.11 , +(p10(), p1()) -> +(p1(), p10()) 1150.89/297.11 , +(p10(), p2()) -> +(p2(), p10()) 1150.89/297.11 , +(p10(), p5()) -> +(p5(), p10()) } 1150.89/297.11 Obligation: 1150.89/297.11 derivational complexity 1150.89/297.11 Answer: 1150.89/297.12 YES(O(1),O(n^5)) 1150.89/297.12 1150.89/297.12 We use the processor 'matrix interpretation of dimension 1' to 1150.89/297.12 orient following rules strictly. 1150.89/297.12 1150.89/297.12 Trs: 1150.89/297.12 { +(p1(), +(p1(), x)) -> +(p2(), x) 1150.89/297.12 , +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x) 1150.89/297.12 , +(p1(), +(p2(), p2())) -> p5() 1150.89/297.12 , +(p1(), p1()) -> p2() 1150.89/297.12 , +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)) 1150.89/297.12 , +(p2(), +(p2(), p2())) -> +(p1(), p5()) 1150.89/297.12 , +(p5(), +(p5(), x)) -> +(p10(), x) 1150.89/297.12 , +(p5(), p5()) -> p10() } 1150.89/297.12 1150.89/297.12 The induced complexity on above rules (modulo remaining rules) is 1150.89/297.12 YES(?,O(n^1)) . These rules are removed from the problem. Note that 1150.89/297.12 no rule is size-increasing. The overall complexity is obtained by 1150.89/297.12 multiplication . 1150.89/297.12 1150.89/297.12 Sub-proof: 1150.89/297.12 ---------- 1150.89/297.12 TcT has computed the following triangular matrix interpretation. 1150.89/297.12 1150.89/297.12 [+](x1, x2) = [1] x1 + [1] x2 + [2] 1150.89/297.12 1150.89/297.12 [p1] = [0] 1150.89/297.12 1150.89/297.12 [p2] = [0] 1150.89/297.12 1150.89/297.12 [p5] = [1] 1150.89/297.12 1150.89/297.12 [p10] = [2] 1150.89/297.12 1150.89/297.12 The order satisfies the following ordering constraints: 1150.89/297.12 1150.89/297.12 [+(+(x, y), z)] = [1] x + [1] y + [1] z + [4] 1150.89/297.12 >= [1] x + [1] y + [1] z + [4] 1150.89/297.12 = [+(x, +(y, z))] 1150.89/297.12 1150.89/297.12 [+(p1(), +(p1(), x))] = [1] x + [4] 1150.89/297.12 > [1] x + [2] 1150.89/297.12 = [+(p2(), x)] 1150.89/297.12 1150.89/297.12 [+(p1(), +(p2(), +(p2(), x)))] = [1] x + [6] 1150.89/297.12 > [1] x + [3] 1150.89/297.12 = [+(p5(), x)] 1150.89/297.12 1150.89/297.12 [+(p1(), +(p2(), p2()))] = [4] 1150.89/297.12 > [1] 1150.89/297.12 = [p5()] 1150.89/297.12 1150.89/297.12 [+(p1(), p1())] = [2] 1150.89/297.12 > [0] 1150.89/297.12 = [p2()] 1150.89/297.12 1150.89/297.12 [+(p2(), +(p1(), x))] = [1] x + [4] 1150.89/297.12 >= [1] x + [4] 1150.89/297.12 = [+(p1(), +(p2(), x))] 1150.89/297.12 1150.89/297.12 [+(p2(), +(p2(), +(p2(), x)))] = [1] x + [6] 1150.89/297.12 > [1] x + [5] 1150.89/297.12 = [+(p1(), +(p5(), x))] 1150.89/297.12 1150.89/297.12 [+(p2(), +(p2(), p2()))] = [4] 1150.89/297.12 > [3] 1150.89/297.12 = [+(p1(), p5())] 1150.89/297.12 1150.89/297.12 [+(p2(), p1())] = [2] 1150.89/297.12 >= [2] 1150.89/297.12 = [+(p1(), p2())] 1150.89/297.12 1150.89/297.12 [+(p5(), +(p1(), x))] = [1] x + [5] 1150.89/297.12 >= [1] x + [5] 1150.89/297.12 = [+(p1(), +(p5(), x))] 1150.89/297.12 1150.89/297.12 [+(p5(), +(p2(), x))] = [1] x + [5] 1150.89/297.12 >= [1] x + [5] 1150.89/297.12 = [+(p2(), +(p5(), x))] 1150.89/297.12 1150.89/297.12 [+(p5(), +(p5(), x))] = [1] x + [6] 1150.89/297.12 > [1] x + [4] 1150.89/297.12 = [+(p10(), x)] 1150.89/297.12 1150.89/297.12 [+(p5(), p1())] = [3] 1150.89/297.12 >= [3] 1150.89/297.12 = [+(p1(), p5())] 1150.89/297.12 1150.89/297.12 [+(p5(), p2())] = [3] 1150.89/297.12 >= [3] 1150.89/297.12 = [+(p2(), p5())] 1150.89/297.12 1150.89/297.12 [+(p5(), p5())] = [4] 1150.89/297.12 > [2] 1150.89/297.12 = [p10()] 1150.89/297.12 1150.89/297.12 [+(p10(), +(p1(), x))] = [1] x + [6] 1150.89/297.12 >= [1] x + [6] 1150.89/297.12 = [+(p1(), +(p10(), x))] 1150.89/297.12 1150.89/297.12 [+(p10(), +(p2(), x))] = [1] x + [6] 1150.89/297.12 >= [1] x + [6] 1150.89/297.12 = [+(p2(), +(p10(), x))] 1150.89/297.12 1150.89/297.12 [+(p10(), +(p5(), x))] = [1] x + [7] 1150.89/297.12 >= [1] x + [7] 1150.89/297.12 = [+(p5(), +(p10(), x))] 1150.89/297.12 1150.89/297.12 [+(p10(), p1())] = [4] 1150.89/297.12 >= [4] 1150.89/297.12 = [+(p1(), p10())] 1150.89/297.12 1150.89/297.12 [+(p10(), p2())] = [4] 1150.89/297.12 >= [4] 1150.89/297.12 = [+(p2(), p10())] 1150.89/297.12 1150.89/297.12 [+(p10(), p5())] = [5] 1150.89/297.12 >= [5] 1150.89/297.12 = [+(p5(), p10())] 1150.89/297.12 1150.89/297.12 1150.89/297.12 We return to the main proof. 1150.89/297.12 1150.89/297.12 We are left with following problem, upon which TcT provides the 1150.89/297.12 certificate YES(O(1),O(n^4)). 1150.89/297.12 1150.89/297.12 Strict Trs: 1150.89/297.12 { +(+(x, y), z) -> +(x, +(y, z)) 1150.89/297.12 , +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)) 1150.89/297.12 , +(p2(), p1()) -> +(p1(), p2()) 1150.89/297.12 , +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)) 1150.89/297.12 , +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)) 1150.89/297.12 , +(p5(), p1()) -> +(p1(), p5()) 1150.89/297.12 , +(p5(), p2()) -> +(p2(), p5()) 1150.89/297.12 , +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)) 1150.89/297.12 , +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)) 1150.89/297.12 , +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)) 1150.89/297.12 , +(p10(), p1()) -> +(p1(), p10()) 1150.89/297.12 , +(p10(), p2()) -> +(p2(), p10()) 1150.89/297.12 , +(p10(), p5()) -> +(p5(), p10()) } 1150.89/297.12 Obligation: 1150.89/297.12 derivational complexity 1150.89/297.12 Answer: 1150.89/297.12 YES(O(1),O(n^4)) 1150.89/297.12 1150.89/297.12 We use the processor 'matrix interpretation of dimension 2' to 1150.89/297.12 orient following rules strictly. 1150.89/297.12 1150.89/297.12 Trs: 1150.89/297.12 { +(+(x, y), z) -> +(x, +(y, z)) 1150.89/297.12 , +(p5(), p1()) -> +(p1(), p5()) 1150.89/297.12 , +(p5(), p2()) -> +(p2(), p5()) 1150.89/297.12 , +(p10(), p1()) -> +(p1(), p10()) 1150.89/297.12 , +(p10(), p2()) -> +(p2(), p10()) 1150.89/297.12 , +(p10(), p5()) -> +(p5(), p10()) } 1150.89/297.12 1150.89/297.12 The induced complexity on above rules (modulo remaining rules) is 1150.89/297.12 YES(?,O(n^2)) . These rules are removed from the problem. Note that 1150.89/297.12 no rule is size-increasing. The overall complexity is obtained by 1150.89/297.12 multiplication . 1150.89/297.12 1150.89/297.12 Sub-proof: 1150.89/297.12 ---------- 1150.89/297.12 TcT has computed the following triangular matrix interpretation. 1150.89/297.12 1150.89/297.12 [+](x1, x2) = [1 1] x1 + [1 0] x2 + [0] 1150.89/297.12 [0 1] [0 1] [2] 1150.89/297.12 1150.89/297.12 [p1] = [2] 1150.89/297.12 [0] 1150.89/297.12 1150.89/297.12 [p2] = [2] 1150.89/297.12 [0] 1150.89/297.12 1150.89/297.12 [p5] = [1] 1150.89/297.12 [1] 1150.89/297.12 1150.89/297.12 [p10] = [0] 1150.89/297.12 [2] 1150.89/297.12 1150.89/297.12 The order satisfies the following ordering constraints: 1150.89/297.12 1150.89/297.12 [+(+(x, y), z)] = [1 2] x + [1 1] y + [1 0] z + [2] 1150.89/297.12 [0 1] [0 1] [0 1] [4] 1150.89/297.12 > [1 1] x + [1 1] y + [1 0] z + [0] 1150.89/297.12 [0 1] [0 1] [0 1] [4] 1150.89/297.12 = [+(x, +(y, z))] 1150.89/297.12 1150.89/297.12 [+(p2(), +(p1(), x))] = [1 0] x + [4] 1150.89/297.12 [0 1] [4] 1150.89/297.12 >= [1 0] x + [4] 1150.89/297.12 [0 1] [4] 1150.89/297.12 = [+(p1(), +(p2(), x))] 1150.89/297.12 1150.89/297.12 [+(p2(), p1())] = [4] 1150.89/297.12 [2] 1150.89/297.12 >= [4] 1150.89/297.12 [2] 1150.89/297.12 = [+(p1(), p2())] 1150.89/297.12 1150.89/297.12 [+(p5(), +(p1(), x))] = [1 0] x + [4] 1150.89/297.12 [0 1] [5] 1150.89/297.12 >= [1 0] x + [4] 1150.89/297.12 [0 1] [5] 1150.89/297.12 = [+(p1(), +(p5(), x))] 1150.89/297.12 1150.89/297.12 [+(p5(), +(p2(), x))] = [1 0] x + [4] 1150.89/297.12 [0 1] [5] 1150.89/297.12 >= [1 0] x + [4] 1150.89/297.12 [0 1] [5] 1150.89/297.12 = [+(p2(), +(p5(), x))] 1150.89/297.12 1150.89/297.12 [+(p5(), p1())] = [4] 1150.89/297.12 [3] 1150.89/297.12 > [3] 1150.89/297.12 [3] 1150.89/297.12 = [+(p1(), p5())] 1150.89/297.12 1150.89/297.12 [+(p5(), p2())] = [4] 1150.89/297.12 [3] 1150.89/297.12 > [3] 1150.89/297.12 [3] 1150.89/297.12 = [+(p2(), p5())] 1150.89/297.12 1150.89/297.12 [+(p10(), +(p1(), x))] = [1 0] x + [4] 1150.89/297.12 [0 1] [6] 1150.89/297.12 >= [1 0] x + [4] 1150.89/297.12 [0 1] [6] 1150.89/297.12 = [+(p1(), +(p10(), x))] 1150.89/297.12 1150.89/297.12 [+(p10(), +(p2(), x))] = [1 0] x + [4] 1150.89/297.12 [0 1] [6] 1150.89/297.12 >= [1 0] x + [4] 1150.89/297.12 [0 1] [6] 1150.89/297.12 = [+(p2(), +(p10(), x))] 1150.89/297.12 1150.89/297.12 [+(p10(), +(p5(), x))] = [1 0] x + [4] 1150.89/297.12 [0 1] [7] 1150.89/297.12 >= [1 0] x + [4] 1150.89/297.12 [0 1] [7] 1150.89/297.12 = [+(p5(), +(p10(), x))] 1150.89/297.12 1150.89/297.12 [+(p10(), p1())] = [4] 1150.89/297.12 [4] 1150.89/297.12 > [2] 1150.89/297.12 [4] 1150.89/297.12 = [+(p1(), p10())] 1150.89/297.12 1150.89/297.12 [+(p10(), p2())] = [4] 1150.89/297.12 [4] 1150.89/297.12 > [2] 1150.89/297.12 [4] 1150.89/297.12 = [+(p2(), p10())] 1150.89/297.12 1150.89/297.12 [+(p10(), p5())] = [3] 1150.89/297.12 [5] 1150.89/297.12 > [2] 1150.89/297.12 [5] 1150.89/297.12 = [+(p5(), p10())] 1150.89/297.12 1150.89/297.12 1150.89/297.12 We return to the main proof. 1150.89/297.12 1150.89/297.12 We are left with following problem, upon which TcT provides the 1150.89/297.12 certificate YES(?,O(n^2)). 1150.89/297.12 1150.89/297.12 Strict Trs: 1150.89/297.12 { +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)) 1150.89/297.12 , +(p2(), p1()) -> +(p1(), p2()) 1150.89/297.12 , +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)) 1150.89/297.12 , +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)) 1150.89/297.12 , +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)) 1150.89/297.12 , +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)) 1150.89/297.12 , +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)) } 1150.89/297.12 Obligation: 1150.89/297.12 derivational complexity 1150.89/297.12 Answer: 1150.89/297.12 YES(?,O(n^2)) 1150.89/297.12 1150.89/297.12 TcT has computed the following triangular matrix interpretation. 1150.89/297.12 1150.89/297.12 [+](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 1150.89/297.12 [0 1] [0 1] [0] 1150.89/297.12 1150.89/297.12 [p1] = [0] 1150.89/297.12 [5] 1150.89/297.12 1150.89/297.12 [p2] = [0] 1150.89/297.12 [4] 1150.89/297.12 1150.89/297.12 [p5] = [0] 1150.89/297.12 [1] 1150.89/297.12 1150.89/297.12 [p10] = [0] 1150.89/297.12 [0] 1150.89/297.12 1150.89/297.12 The order satisfies the following ordering constraints: 1150.89/297.12 1150.89/297.12 [+(p2(), +(p1(), x))] = [1 2] x + [5] 1150.89/297.12 [0 1] [9] 1150.89/297.12 > [1 2] x + [4] 1150.89/297.12 [0 1] [9] 1150.89/297.12 = [+(p1(), +(p2(), x))] 1150.89/297.12 1150.89/297.12 [+(p2(), p1())] = [5] 1150.89/297.12 [9] 1150.89/297.12 > [4] 1150.89/297.12 [9] 1150.89/297.12 = [+(p1(), p2())] 1150.89/297.12 1150.89/297.12 [+(p5(), +(p1(), x))] = [1 2] x + [5] 1150.89/297.12 [0 1] [6] 1150.89/297.12 > [1 2] x + [1] 1150.89/297.12 [0 1] [6] 1150.89/297.12 = [+(p1(), +(p5(), x))] 1150.89/297.12 1150.89/297.12 [+(p5(), +(p2(), x))] = [1 2] x + [4] 1150.89/297.12 [0 1] [5] 1150.89/297.12 > [1 2] x + [1] 1150.89/297.12 [0 1] [5] 1150.89/297.12 = [+(p2(), +(p5(), x))] 1150.89/297.12 1150.89/297.12 [+(p10(), +(p1(), x))] = [1 2] x + [5] 1150.89/297.12 [0 1] [5] 1150.89/297.12 > [1 2] x + [0] 1150.89/297.12 [0 1] [5] 1150.89/297.12 = [+(p1(), +(p10(), x))] 1150.89/297.12 1150.89/297.12 [+(p10(), +(p2(), x))] = [1 2] x + [4] 1150.89/297.12 [0 1] [4] 1150.89/297.12 > [1 2] x + [0] 1150.89/297.12 [0 1] [4] 1150.89/297.12 = [+(p2(), +(p10(), x))] 1150.89/297.12 1150.89/297.12 [+(p10(), +(p5(), x))] = [1 2] x + [1] 1150.89/297.12 [0 1] [1] 1150.89/297.12 > [1 2] x + [0] 1150.89/297.12 [0 1] [1] 1150.89/297.12 = [+(p5(), +(p10(), x))] 1150.89/297.12 1150.89/297.12 1150.89/297.12 Hurray, we answered YES(O(1),O(n^5)) 1150.89/297.17 EOF