YES(O(1),O(n^2)) 753.95/297.34 YES(O(1),O(n^2)) 753.95/297.34 753.95/297.34 We are left with following problem, upon which TcT provides the 753.95/297.34 certificate YES(O(1),O(n^2)). 753.95/297.34 753.95/297.34 Strict Trs: 753.95/297.34 { a12(a12(x1)) -> x1 753.95/297.34 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.34 , a12(a34(x1)) -> a34(a12(x1)) 753.95/297.34 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.34 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.34 , a13(x1) -> a12(a23(a12(x1))) 753.95/297.34 , a13(a13(x1)) -> x1 753.95/297.34 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.34 , a14(a14(x1)) -> x1 753.95/297.34 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.34 , a15(a15(x1)) -> x1 753.95/297.34 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.34 , a16(a16(x1)) -> x1 753.95/297.34 , a23(a23(x1)) -> x1 753.95/297.34 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.34 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.34 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.34 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.34 , a24(a24(x1)) -> x1 753.95/297.34 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.34 , a25(a25(x1)) -> x1 753.95/297.34 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.34 , a26(a26(x1)) -> x1 753.95/297.34 , a34(a34(x1)) -> x1 753.95/297.34 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.34 , a34(a56(x1)) -> a56(a34(x1)) 753.95/297.34 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.34 , a35(a35(x1)) -> x1 753.95/297.34 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.34 , a36(a36(x1)) -> x1 753.95/297.34 , a45(a45(x1)) -> x1 753.95/297.34 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.34 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.34 , a46(a46(x1)) -> x1 753.95/297.34 , a56(a56(x1)) -> x1 } 753.95/297.34 Obligation: 753.95/297.34 derivational complexity 753.95/297.34 Answer: 753.95/297.34 YES(O(1),O(n^2)) 753.95/297.34 753.95/297.34 We use the processor 'matrix interpretation of dimension 1' to 753.95/297.34 orient following rules strictly. 753.95/297.34 753.95/297.34 Trs: 753.95/297.34 { a13(x1) -> a12(a23(a12(x1))) 753.95/297.34 , a13(a13(x1)) -> x1 753.95/297.34 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.34 , a14(a14(x1)) -> x1 753.95/297.34 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.34 , a15(a15(x1)) -> x1 753.95/297.34 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.34 , a16(a16(x1)) -> x1 753.95/297.34 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.34 , a24(a24(x1)) -> x1 753.95/297.34 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.34 , a25(a25(x1)) -> x1 753.95/297.34 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.34 , a26(a26(x1)) -> x1 753.95/297.34 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.34 , a35(a35(x1)) -> x1 753.95/297.34 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.34 , a36(a36(x1)) -> x1 753.95/297.34 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.34 , a46(a46(x1)) -> x1 } 753.95/297.34 753.95/297.34 The induced complexity on above rules (modulo remaining rules) is 753.95/297.34 YES(?,O(n^1)) . These rules are moved into the corresponding weak 753.95/297.34 component(s). 753.95/297.34 753.95/297.34 Sub-proof: 753.95/297.34 ---------- 753.95/297.34 TcT has computed the following triangular matrix interpretation. 753.95/297.34 753.95/297.34 [a12](x1) = [1] x1 + [0] 753.95/297.34 753.95/297.34 [a13](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a14](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a15](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a16](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a23](x1) = [1] x1 + [0] 753.95/297.34 753.95/297.34 [a24](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a25](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a26](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a34](x1) = [1] x1 + [0] 753.95/297.34 753.95/297.34 [a35](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a36](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a45](x1) = [1] x1 + [0] 753.95/297.34 753.95/297.34 [a46](x1) = [1] x1 + [2] 753.95/297.34 753.95/297.34 [a56](x1) = [1] x1 + [0] 753.95/297.34 753.95/297.34 The order satisfies the following ordering constraints: 753.95/297.34 753.95/297.34 [a12(a12(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a12(a23(a12(a23(a12(a23(x1))))))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a12(a34(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [a34(a12(x1))] 753.95/297.34 753.95/297.34 [a12(a45(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [a45(a12(x1))] 753.95/297.34 753.95/297.34 [a12(a56(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [a56(a12(x1))] 753.95/297.34 753.95/297.34 [a13(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a12(a23(a12(x1)))] 753.95/297.34 753.95/297.34 [a13(a13(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a14(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.34 753.95/297.34 [a14(a14(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a15(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.34 753.95/297.34 [a15(a15(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a16(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.34 753.95/297.34 [a16(a16(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a23(a23(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a23(a34(a23(a34(a23(a34(x1))))))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a23(a45(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [a45(a23(x1))] 753.95/297.34 753.95/297.34 [a23(a56(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [a56(a23(x1))] 753.95/297.34 753.95/297.34 [a24(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a23(a34(a23(x1)))] 753.95/297.34 753.95/297.34 [a24(a24(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a25(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.34 753.95/297.34 [a25(a25(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a26(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.34 753.95/297.34 [a26(a26(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a34(a34(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a34(a45(a34(a45(a34(a45(x1))))))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a34(a56(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [a56(a34(x1))] 753.95/297.34 753.95/297.34 [a35(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a34(a45(a34(x1)))] 753.95/297.34 753.95/297.34 [a35(a35(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a36(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.34 753.95/297.34 [a36(a36(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a45(a45(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a45(a56(a45(a56(a45(a56(x1))))))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a46(x1)] = [1] x1 + [2] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [a45(a56(a45(x1)))] 753.95/297.34 753.95/297.34 [a46(a46(x1))] = [1] x1 + [4] 753.95/297.34 > [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 [a56(a56(x1))] = [1] x1 + [0] 753.95/297.34 >= [1] x1 + [0] 753.95/297.34 = [x1] 753.95/297.34 753.95/297.34 753.95/297.34 We return to the main proof. 753.95/297.34 753.95/297.34 We are left with following problem, upon which TcT provides the 753.95/297.35 certificate YES(O(1),O(n^2)). 753.95/297.35 753.95/297.35 Strict Trs: 753.95/297.35 { a12(a12(x1)) -> x1 753.95/297.35 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.35 , a12(a34(x1)) -> a34(a12(x1)) 753.95/297.35 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.35 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.35 , a23(a23(x1)) -> x1 753.95/297.35 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.35 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.35 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.35 , a34(a34(x1)) -> x1 753.95/297.35 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.35 , a34(a56(x1)) -> a56(a34(x1)) 753.95/297.35 , a45(a45(x1)) -> x1 753.95/297.35 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.35 , a56(a56(x1)) -> x1 } 753.95/297.35 Weak Trs: 753.95/297.35 { a13(x1) -> a12(a23(a12(x1))) 753.95/297.35 , a13(a13(x1)) -> x1 753.95/297.35 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.35 , a14(a14(x1)) -> x1 753.95/297.35 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.35 , a15(a15(x1)) -> x1 753.95/297.35 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.35 , a16(a16(x1)) -> x1 753.95/297.35 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.35 , a24(a24(x1)) -> x1 753.95/297.35 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.35 , a25(a25(x1)) -> x1 753.95/297.35 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.35 , a26(a26(x1)) -> x1 753.95/297.35 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.35 , a35(a35(x1)) -> x1 753.95/297.35 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.35 , a36(a36(x1)) -> x1 753.95/297.35 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.35 , a46(a46(x1)) -> x1 } 753.95/297.35 Obligation: 753.95/297.35 derivational complexity 753.95/297.35 Answer: 753.95/297.35 YES(O(1),O(n^2)) 753.95/297.35 753.95/297.35 We use the processor 'matrix interpretation of dimension 1' to 753.95/297.35 orient following rules strictly. 753.95/297.35 753.95/297.35 Trs: 753.95/297.35 { a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.35 , a56(a56(x1)) -> x1 } 753.95/297.35 753.95/297.35 The induced complexity on above rules (modulo remaining rules) is 753.95/297.35 YES(?,O(n^1)) . These rules are moved into the corresponding weak 753.95/297.35 component(s). 753.95/297.35 753.95/297.35 Sub-proof: 753.95/297.35 ---------- 753.95/297.35 TcT has computed the following triangular matrix interpretation. 753.95/297.35 753.95/297.35 [a12](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a13](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a14](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a15](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a16](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a23](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a24](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a25](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a26](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a34](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a35](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a36](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a45](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a46](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a56](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 The order satisfies the following ordering constraints: 753.95/297.35 753.95/297.35 [a12(a12(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a12(a23(a12(a23(a12(a23(x1))))))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a12(a34(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a34(a12(x1))] 753.95/297.35 753.95/297.35 [a12(a45(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a45(a12(x1))] 753.95/297.35 753.95/297.35 [a12(a56(x1))] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a56(a12(x1))] 753.95/297.35 753.95/297.35 [a13(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a12(a23(a12(x1)))] 753.95/297.35 753.95/297.35 [a13(a13(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a14(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.35 753.95/297.35 [a14(a14(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a15(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.35 753.95/297.35 [a15(a15(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a16(x1)] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [1] 753.95/297.35 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.35 753.95/297.35 [a16(a16(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a23(a23(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a23(a34(a23(a34(a23(a34(x1))))))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a23(a45(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a45(a23(x1))] 753.95/297.35 753.95/297.35 [a23(a56(x1))] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a56(a23(x1))] 753.95/297.35 753.95/297.35 [a24(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a23(a34(a23(x1)))] 753.95/297.35 753.95/297.35 [a24(a24(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a25(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.35 753.95/297.35 [a25(a25(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a26(x1)] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [1] 753.95/297.35 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.35 753.95/297.35 [a26(a26(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a34(a34(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a34(a45(a34(a45(a34(a45(x1))))))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a34(a56(x1))] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a56(a34(x1))] 753.95/297.35 753.95/297.35 [a35(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a34(a45(a34(x1)))] 753.95/297.35 753.95/297.35 [a35(a35(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a36(x1)] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.35 753.95/297.35 [a36(a36(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a45(a45(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a45(a56(a45(a56(a45(a56(x1))))))] = [1] x1 + [3] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a46(x1)] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a45(a56(a45(x1)))] 753.95/297.35 753.95/297.35 [a46(a46(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a56(a56(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 753.95/297.35 We return to the main proof. 753.95/297.35 753.95/297.35 We are left with following problem, upon which TcT provides the 753.95/297.35 certificate YES(O(1),O(n^2)). 753.95/297.35 753.95/297.35 Strict Trs: 753.95/297.35 { a12(a12(x1)) -> x1 753.95/297.35 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.35 , a12(a34(x1)) -> a34(a12(x1)) 753.95/297.35 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.35 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.35 , a23(a23(x1)) -> x1 753.95/297.35 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.35 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.35 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.35 , a34(a34(x1)) -> x1 753.95/297.35 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.35 , a34(a56(x1)) -> a56(a34(x1)) 753.95/297.35 , a45(a45(x1)) -> x1 } 753.95/297.35 Weak Trs: 753.95/297.35 { a13(x1) -> a12(a23(a12(x1))) 753.95/297.35 , a13(a13(x1)) -> x1 753.95/297.35 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.35 , a14(a14(x1)) -> x1 753.95/297.35 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.35 , a15(a15(x1)) -> x1 753.95/297.35 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.35 , a16(a16(x1)) -> x1 753.95/297.35 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.35 , a24(a24(x1)) -> x1 753.95/297.35 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.35 , a25(a25(x1)) -> x1 753.95/297.35 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.35 , a26(a26(x1)) -> x1 753.95/297.35 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.35 , a35(a35(x1)) -> x1 753.95/297.35 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.35 , a36(a36(x1)) -> x1 753.95/297.35 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.35 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.35 , a46(a46(x1)) -> x1 753.95/297.35 , a56(a56(x1)) -> x1 } 753.95/297.35 Obligation: 753.95/297.35 derivational complexity 753.95/297.35 Answer: 753.95/297.35 YES(O(1),O(n^2)) 753.95/297.35 753.95/297.35 We use the processor 'matrix interpretation of dimension 1' to 753.95/297.35 orient following rules strictly. 753.95/297.35 753.95/297.35 Trs: 753.95/297.35 { a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.35 , a45(a45(x1)) -> x1 } 753.95/297.35 753.95/297.35 The induced complexity on above rules (modulo remaining rules) is 753.95/297.35 YES(?,O(n^1)) . These rules are moved into the corresponding weak 753.95/297.35 component(s). 753.95/297.35 753.95/297.35 Sub-proof: 753.95/297.35 ---------- 753.95/297.35 TcT has computed the following triangular matrix interpretation. 753.95/297.35 753.95/297.35 [a12](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a13](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a14](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a15](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a16](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a23](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a24](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a25](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a26](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a34](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a35](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a36](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a45](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a46](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a56](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 The order satisfies the following ordering constraints: 753.95/297.35 753.95/297.35 [a12(a12(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a12(a23(a12(a23(a12(a23(x1))))))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a12(a34(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a34(a12(x1))] 753.95/297.35 753.95/297.35 [a12(a45(x1))] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a45(a12(x1))] 753.95/297.35 753.95/297.35 [a12(a56(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a56(a12(x1))] 753.95/297.35 753.95/297.35 [a13(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a12(a23(a12(x1)))] 753.95/297.35 753.95/297.35 [a13(a13(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a14(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.35 753.95/297.35 [a14(a14(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a15(x1)] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [1] 753.95/297.35 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.35 753.95/297.35 [a15(a15(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a16(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.35 753.95/297.35 [a16(a16(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a23(a23(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a23(a34(a23(a34(a23(a34(x1))))))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a23(a45(x1))] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a45(a23(x1))] 753.95/297.35 753.95/297.35 [a23(a56(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a56(a23(x1))] 753.95/297.35 753.95/297.35 [a24(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a23(a34(a23(x1)))] 753.95/297.35 753.95/297.35 [a24(a24(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a25(x1)] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [1] 753.95/297.35 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.35 753.95/297.35 [a25(a25(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a26(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.35 753.95/297.35 [a26(a26(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a34(a34(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a34(a45(a34(a45(a34(a45(x1))))))] = [1] x1 + [3] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a34(a56(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a56(a34(x1))] 753.95/297.35 753.95/297.35 [a35(x1)] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a34(a45(a34(x1)))] 753.95/297.35 753.95/297.35 [a35(a35(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a36(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.35 753.95/297.35 [a36(a36(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a45(a45(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a45(a56(a45(a56(a45(a56(x1))))))] = [1] x1 + [3] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a46(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a45(a56(a45(x1)))] 753.95/297.35 753.95/297.35 [a46(a46(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a56(a56(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 753.95/297.35 We return to the main proof. 753.95/297.35 753.95/297.35 We are left with following problem, upon which TcT provides the 753.95/297.35 certificate YES(O(1),O(n^2)). 753.95/297.35 753.95/297.35 Strict Trs: 753.95/297.35 { a12(a12(x1)) -> x1 753.95/297.35 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.35 , a12(a34(x1)) -> a34(a12(x1)) 753.95/297.35 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.35 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.35 , a23(a23(x1)) -> x1 753.95/297.35 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.35 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.35 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.35 , a34(a34(x1)) -> x1 753.95/297.35 , a34(a56(x1)) -> a56(a34(x1)) } 753.95/297.35 Weak Trs: 753.95/297.35 { a13(x1) -> a12(a23(a12(x1))) 753.95/297.35 , a13(a13(x1)) -> x1 753.95/297.35 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.35 , a14(a14(x1)) -> x1 753.95/297.35 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.35 , a15(a15(x1)) -> x1 753.95/297.35 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.35 , a16(a16(x1)) -> x1 753.95/297.35 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.35 , a24(a24(x1)) -> x1 753.95/297.35 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.35 , a25(a25(x1)) -> x1 753.95/297.35 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.35 , a26(a26(x1)) -> x1 753.95/297.35 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.35 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.35 , a35(a35(x1)) -> x1 753.95/297.35 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.35 , a36(a36(x1)) -> x1 753.95/297.35 , a45(a45(x1)) -> x1 753.95/297.35 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.35 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.35 , a46(a46(x1)) -> x1 753.95/297.35 , a56(a56(x1)) -> x1 } 753.95/297.35 Obligation: 753.95/297.35 derivational complexity 753.95/297.35 Answer: 753.95/297.35 YES(O(1),O(n^2)) 753.95/297.35 753.95/297.35 We use the processor 'matrix interpretation of dimension 1' to 753.95/297.35 orient following rules strictly. 753.95/297.35 753.95/297.35 Trs: 753.95/297.35 { a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.35 , a34(a34(x1)) -> x1 } 753.95/297.35 753.95/297.35 The induced complexity on above rules (modulo remaining rules) is 753.95/297.35 YES(?,O(n^1)) . These rules are moved into the corresponding weak 753.95/297.35 component(s). 753.95/297.35 753.95/297.35 Sub-proof: 753.95/297.35 ---------- 753.95/297.35 TcT has computed the following triangular matrix interpretation. 753.95/297.35 753.95/297.35 [a12](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a13](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a14](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a15](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a16](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a23](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a24](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a25](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a26](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a34](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a35](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a36](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a45](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a46](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a56](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 The order satisfies the following ordering constraints: 753.95/297.35 753.95/297.35 [a12(a12(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a12(a23(a12(a23(a12(a23(x1))))))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a12(a34(x1))] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a34(a12(x1))] 753.95/297.35 753.95/297.35 [a12(a45(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a45(a12(x1))] 753.95/297.35 753.95/297.35 [a12(a56(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a56(a12(x1))] 753.95/297.35 753.95/297.35 [a13(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a12(a23(a12(x1)))] 753.95/297.35 753.95/297.35 [a13(a13(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a14(x1)] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.35 753.95/297.35 [a14(a14(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a15(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.35 753.95/297.35 [a15(a15(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a16(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.35 753.95/297.35 [a16(a16(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a23(a23(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a23(a34(a23(a34(a23(a34(x1))))))] = [1] x1 + [3] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a23(a45(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a45(a23(x1))] 753.95/297.35 753.95/297.35 [a23(a56(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [a56(a23(x1))] 753.95/297.35 753.95/297.35 [a24(x1)] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a23(a34(a23(x1)))] 753.95/297.35 753.95/297.35 [a24(a24(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a25(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.35 753.95/297.35 [a25(a25(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a26(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.35 753.95/297.35 [a26(a26(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a34(a34(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a34(a45(a34(a45(a34(a45(x1))))))] = [1] x1 + [3] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a34(a56(x1))] = [1] x1 + [1] 753.95/297.35 >= [1] x1 + [1] 753.95/297.35 = [a56(a34(x1))] 753.95/297.35 753.95/297.35 [a35(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a34(a45(a34(x1)))] 753.95/297.35 753.95/297.35 [a35(a35(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a36(x1)] = [1] x1 + [2] 753.95/297.35 >= [1] x1 + [2] 753.95/297.35 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.35 753.95/297.35 [a36(a36(x1))] = [1] x1 + [4] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a45(a45(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a45(a56(a45(a56(a45(a56(x1))))))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a46(x1)] = [1] x1 + [1] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [a45(a56(a45(x1)))] 753.95/297.35 753.95/297.35 [a46(a46(x1))] = [1] x1 + [2] 753.95/297.35 > [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 [a56(a56(x1))] = [1] x1 + [0] 753.95/297.35 >= [1] x1 + [0] 753.95/297.35 = [x1] 753.95/297.35 753.95/297.35 753.95/297.35 We return to the main proof. 753.95/297.35 753.95/297.35 We are left with following problem, upon which TcT provides the 753.95/297.35 certificate YES(O(1),O(n^2)). 753.95/297.35 753.95/297.35 Strict Trs: 753.95/297.35 { a12(a12(x1)) -> x1 753.95/297.35 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.35 , a12(a34(x1)) -> a34(a12(x1)) 753.95/297.35 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.35 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.35 , a23(a23(x1)) -> x1 753.95/297.35 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.35 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.35 , a34(a56(x1)) -> a56(a34(x1)) } 753.95/297.35 Weak Trs: 753.95/297.35 { a13(x1) -> a12(a23(a12(x1))) 753.95/297.35 , a13(a13(x1)) -> x1 753.95/297.35 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.35 , a14(a14(x1)) -> x1 753.95/297.35 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.35 , a15(a15(x1)) -> x1 753.95/297.35 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.35 , a16(a16(x1)) -> x1 753.95/297.35 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.35 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.35 , a24(a24(x1)) -> x1 753.95/297.35 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.35 , a25(a25(x1)) -> x1 753.95/297.35 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.35 , a26(a26(x1)) -> x1 753.95/297.35 , a34(a34(x1)) -> x1 753.95/297.35 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.35 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.35 , a35(a35(x1)) -> x1 753.95/297.35 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.35 , a36(a36(x1)) -> x1 753.95/297.35 , a45(a45(x1)) -> x1 753.95/297.35 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.35 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.35 , a46(a46(x1)) -> x1 753.95/297.35 , a56(a56(x1)) -> x1 } 753.95/297.35 Obligation: 753.95/297.35 derivational complexity 753.95/297.35 Answer: 753.95/297.35 YES(O(1),O(n^2)) 753.95/297.35 753.95/297.35 We use the processor 'matrix interpretation of dimension 1' to 753.95/297.35 orient following rules strictly. 753.95/297.35 753.95/297.35 Trs: 753.95/297.35 { a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.35 , a23(a23(x1)) -> x1 } 753.95/297.35 753.95/297.35 The induced complexity on above rules (modulo remaining rules) is 753.95/297.35 YES(?,O(n^1)) . These rules are moved into the corresponding weak 753.95/297.35 component(s). 753.95/297.35 753.95/297.35 Sub-proof: 753.95/297.35 ---------- 753.95/297.35 TcT has computed the following triangular matrix interpretation. 753.95/297.35 753.95/297.35 [a12](x1) = [1] x1 + [0] 753.95/297.35 753.95/297.35 [a13](x1) = [1] x1 + [1] 753.95/297.35 753.95/297.35 [a14](x1) = [1] x1 + [2] 753.95/297.35 753.95/297.35 [a15](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a16](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a23](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a24](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a25](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a26](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a34](x1) = [1] x1 + [0] 753.95/297.36 753.95/297.36 [a35](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a36](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a45](x1) = [1] x1 + [0] 753.95/297.36 753.95/297.36 [a46](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a56](x1) = [1] x1 + [0] 753.95/297.36 753.95/297.36 The order satisfies the following ordering constraints: 753.95/297.36 753.95/297.36 [a12(a12(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a12(a23(a12(a23(a12(a23(x1))))))] = [1] x1 + [3] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a12(a34(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [a34(a12(x1))] 753.95/297.36 753.95/297.36 [a12(a45(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [a45(a12(x1))] 753.95/297.36 753.95/297.36 [a12(a56(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [a56(a12(x1))] 753.95/297.36 753.95/297.36 [a13(x1)] = [1] x1 + [1] 753.95/297.36 >= [1] x1 + [1] 753.95/297.36 = [a12(a23(a12(x1)))] 753.95/297.36 753.95/297.36 [a13(a13(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a14(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.36 753.95/297.36 [a14(a14(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a15(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.36 753.95/297.36 [a15(a15(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a16(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.36 753.95/297.36 [a16(a16(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a23(a23(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a23(a34(a23(a34(a23(a34(x1))))))] = [1] x1 + [3] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a23(a45(x1))] = [1] x1 + [1] 753.95/297.36 >= [1] x1 + [1] 753.95/297.36 = [a45(a23(x1))] 753.95/297.36 753.95/297.36 [a23(a56(x1))] = [1] x1 + [1] 753.95/297.36 >= [1] x1 + [1] 753.95/297.36 = [a56(a23(x1))] 753.95/297.36 753.95/297.36 [a24(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a23(a34(a23(x1)))] 753.95/297.36 753.95/297.36 [a24(a24(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a25(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.36 753.95/297.36 [a25(a25(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a26(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.36 753.95/297.36 [a26(a26(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a34(a34(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a34(a45(a34(a45(a34(a45(x1))))))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a34(a56(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [a56(a34(x1))] 753.95/297.36 753.95/297.36 [a35(x1)] = [1] x1 + [1] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [a34(a45(a34(x1)))] 753.95/297.36 753.95/297.36 [a35(a35(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a36(x1)] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.36 753.95/297.36 [a36(a36(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a45(a45(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a45(a56(a45(a56(a45(a56(x1))))))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a46(x1)] = [1] x1 + [1] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [a45(a56(a45(x1)))] 753.95/297.36 753.95/297.36 [a46(a46(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a56(a56(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 753.95/297.36 We return to the main proof. 753.95/297.36 753.95/297.36 We are left with following problem, upon which TcT provides the 753.95/297.36 certificate YES(O(1),O(n^2)). 753.95/297.36 753.95/297.36 Strict Trs: 753.95/297.36 { a12(a12(x1)) -> x1 753.95/297.36 , a12(a34(x1)) -> a34(a12(x1)) 753.95/297.36 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.36 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.36 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.36 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.36 , a34(a56(x1)) -> a56(a34(x1)) } 753.95/297.36 Weak Trs: 753.95/297.36 { a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.36 , a13(x1) -> a12(a23(a12(x1))) 753.95/297.36 , a13(a13(x1)) -> x1 753.95/297.36 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.36 , a14(a14(x1)) -> x1 753.95/297.36 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.36 , a15(a15(x1)) -> x1 753.95/297.36 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.36 , a16(a16(x1)) -> x1 753.95/297.36 , a23(a23(x1)) -> x1 753.95/297.36 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.36 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.36 , a24(a24(x1)) -> x1 753.95/297.36 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.36 , a25(a25(x1)) -> x1 753.95/297.36 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.36 , a26(a26(x1)) -> x1 753.95/297.36 , a34(a34(x1)) -> x1 753.95/297.36 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.36 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.36 , a35(a35(x1)) -> x1 753.95/297.36 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.36 , a36(a36(x1)) -> x1 753.95/297.36 , a45(a45(x1)) -> x1 753.95/297.36 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.36 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.36 , a46(a46(x1)) -> x1 753.95/297.36 , a56(a56(x1)) -> x1 } 753.95/297.36 Obligation: 753.95/297.36 derivational complexity 753.95/297.36 Answer: 753.95/297.36 YES(O(1),O(n^2)) 753.95/297.36 753.95/297.36 We use the processor 'matrix interpretation of dimension 1' to 753.95/297.36 orient following rules strictly. 753.95/297.36 753.95/297.36 Trs: { a12(a12(x1)) -> x1 } 753.95/297.36 753.95/297.36 The induced complexity on above rules (modulo remaining rules) is 753.95/297.36 YES(?,O(n^1)) . These rules are moved into the corresponding weak 753.95/297.36 component(s). 753.95/297.36 753.95/297.36 Sub-proof: 753.95/297.36 ---------- 753.95/297.36 TcT has computed the following triangular matrix interpretation. 753.95/297.36 753.95/297.36 [a12](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a13](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a14](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a15](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a16](x1) = [1] x1 + [2] 753.95/297.36 753.95/297.36 [a23](x1) = [1] x1 + [0] 753.95/297.36 753.95/297.36 [a24](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a25](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a26](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a34](x1) = [1] x1 + [0] 753.95/297.36 753.95/297.36 [a35](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a36](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a45](x1) = [1] x1 + [0] 753.95/297.36 753.95/297.36 [a46](x1) = [1] x1 + [1] 753.95/297.36 753.95/297.36 [a56](x1) = [1] x1 + [0] 753.95/297.36 753.95/297.36 The order satisfies the following ordering constraints: 753.95/297.36 753.95/297.36 [a12(a12(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a12(a23(a12(a23(a12(a23(x1))))))] = [1] x1 + [3] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a12(a34(x1))] = [1] x1 + [1] 753.95/297.36 >= [1] x1 + [1] 753.95/297.36 = [a34(a12(x1))] 753.95/297.36 753.95/297.36 [a12(a45(x1))] = [1] x1 + [1] 753.95/297.36 >= [1] x1 + [1] 753.95/297.36 = [a45(a12(x1))] 753.95/297.36 753.95/297.36 [a12(a56(x1))] = [1] x1 + [1] 753.95/297.36 >= [1] x1 + [1] 753.95/297.36 = [a56(a12(x1))] 753.95/297.36 753.95/297.36 [a13(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a12(a23(a12(x1)))] 753.95/297.36 753.95/297.36 [a13(a13(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a14(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.36 753.95/297.36 [a14(a14(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a15(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.36 753.95/297.36 [a15(a15(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a16(x1)] = [1] x1 + [2] 753.95/297.36 >= [1] x1 + [2] 753.95/297.36 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.36 753.95/297.36 [a16(a16(x1))] = [1] x1 + [4] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a23(a23(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a23(a34(a23(a34(a23(a34(x1))))))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a23(a45(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [a45(a23(x1))] 753.95/297.36 753.95/297.36 [a23(a56(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [a56(a23(x1))] 753.95/297.36 753.95/297.36 [a24(x1)] = [1] x1 + [1] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [a23(a34(a23(x1)))] 753.95/297.36 753.95/297.36 [a24(a24(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a25(x1)] = [1] x1 + [1] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.36 753.95/297.36 [a25(a25(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a26(x1)] = [1] x1 + [1] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.36 753.95/297.36 [a26(a26(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a34(a34(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a34(a45(a34(a45(a34(a45(x1))))))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a34(a56(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [a56(a34(x1))] 753.95/297.36 753.95/297.36 [a35(x1)] = [1] x1 + [1] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [a34(a45(a34(x1)))] 753.95/297.36 753.95/297.36 [a35(a35(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a36(x1)] = [1] x1 + [1] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.36 753.95/297.36 [a36(a36(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a45(a45(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a45(a56(a45(a56(a45(a56(x1))))))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a46(x1)] = [1] x1 + [1] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [a45(a56(a45(x1)))] 753.95/297.36 753.95/297.36 [a46(a46(x1))] = [1] x1 + [2] 753.95/297.36 > [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a56(a56(x1))] = [1] x1 + [0] 753.95/297.36 >= [1] x1 + [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 753.95/297.36 We return to the main proof. 753.95/297.36 753.95/297.36 We are left with following problem, upon which TcT provides the 753.95/297.36 certificate YES(O(1),O(n^2)). 753.95/297.36 753.95/297.36 Strict Trs: 753.95/297.36 { a12(a34(x1)) -> a34(a12(x1)) 753.95/297.36 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.36 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.36 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.36 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.36 , a34(a56(x1)) -> a56(a34(x1)) } 753.95/297.36 Weak Trs: 753.95/297.36 { a12(a12(x1)) -> x1 753.95/297.36 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.36 , a13(x1) -> a12(a23(a12(x1))) 753.95/297.36 , a13(a13(x1)) -> x1 753.95/297.36 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.36 , a14(a14(x1)) -> x1 753.95/297.36 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.36 , a15(a15(x1)) -> x1 753.95/297.36 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.36 , a16(a16(x1)) -> x1 753.95/297.36 , a23(a23(x1)) -> x1 753.95/297.36 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.36 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.36 , a24(a24(x1)) -> x1 753.95/297.36 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.36 , a25(a25(x1)) -> x1 753.95/297.36 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.36 , a26(a26(x1)) -> x1 753.95/297.36 , a34(a34(x1)) -> x1 753.95/297.36 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.36 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.36 , a35(a35(x1)) -> x1 753.95/297.36 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.36 , a36(a36(x1)) -> x1 753.95/297.36 , a45(a45(x1)) -> x1 753.95/297.36 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.36 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.36 , a46(a46(x1)) -> x1 753.95/297.36 , a56(a56(x1)) -> x1 } 753.95/297.36 Obligation: 753.95/297.36 derivational complexity 753.95/297.36 Answer: 753.95/297.36 YES(O(1),O(n^2)) 753.95/297.36 753.95/297.36 We use the processor 'matrix interpretation of dimension 2' to 753.95/297.36 orient following rules strictly. 753.95/297.36 753.95/297.36 Trs: { a34(a56(x1)) -> a56(a34(x1)) } 753.95/297.36 753.95/297.36 The induced complexity on above rules (modulo remaining rules) is 753.95/297.36 YES(?,O(n^2)) . These rules are moved into the corresponding weak 753.95/297.36 component(s). 753.95/297.36 753.95/297.36 Sub-proof: 753.95/297.36 ---------- 753.95/297.36 TcT has computed the following triangular matrix interpretation. 753.95/297.36 753.95/297.36 [a12](x1) = [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 753.95/297.36 [a13](x1) = [1 1] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 753.95/297.36 [a14](x1) = [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 753.95/297.36 [a15](x1) = [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 753.95/297.36 [a16](x1) = [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 753.95/297.36 [a23](x1) = [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 753.95/297.36 [a24](x1) = [1 1] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 753.95/297.36 [a25](x1) = [1 2] x1 + [1] 753.95/297.36 [0 1] [2] 753.95/297.36 753.95/297.36 [a26](x1) = [1 2] x1 + [2] 753.95/297.36 [0 1] [1] 753.95/297.36 753.95/297.36 [a34](x1) = [1 1] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 753.95/297.36 [a35](x1) = [1 2] x1 + [1] 753.95/297.36 [0 1] [2] 753.95/297.36 753.95/297.36 [a36](x1) = [1 2] x1 + [2] 753.95/297.36 [0 1] [1] 753.95/297.36 753.95/297.36 [a45](x1) = [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 753.95/297.36 [a46](x1) = [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 753.95/297.36 [a56](x1) = [1 0] x1 + [0] 753.95/297.36 [0 1] [1] 753.95/297.36 753.95/297.36 The order satisfies the following ordering constraints: 753.95/297.36 753.95/297.36 [a12(a12(x1))] = [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a12(a23(a12(a23(a12(a23(x1))))))] = [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a12(a34(x1))] = [1 1] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 1] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [a34(a12(x1))] 753.95/297.36 753.95/297.36 [a12(a45(x1))] = [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [a45(a12(x1))] 753.95/297.36 753.95/297.36 [a12(a56(x1))] = [1 0] x1 + [0] 753.95/297.36 [0 1] [1] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [1] 753.95/297.36 = [a56(a12(x1))] 753.95/297.36 753.95/297.36 [a13(x1)] = [1 1] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [a12(a23(a12(x1)))] 753.95/297.36 753.95/297.36 [a13(a13(x1))] = [1 2] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a14(x1)] = [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 > [1 1] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.36 753.95/297.36 [a14(a14(x1))] = [1 4] x1 + [4] 753.95/297.36 [0 1] [2] 753.95/297.36 > [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a15(x1)] = [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 > [1 2] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.36 753.95/297.36 [a15(a15(x1))] = [1 4] x1 + [4] 753.95/297.36 [0 1] [2] 753.95/297.36 > [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a16(x1)] = [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 >= [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.36 753.95/297.36 [a16(a16(x1))] = [1 4] x1 + [4] 753.95/297.36 [0 1] [2] 753.95/297.36 > [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a23(a23(x1))] = [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a23(a34(a23(a34(a23(a34(x1))))))] = [1 3] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a23(a45(x1))] = [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [a45(a23(x1))] 753.95/297.36 753.95/297.36 [a23(a56(x1))] = [1 0] x1 + [0] 753.95/297.36 [0 1] [1] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [1] 753.95/297.36 = [a56(a23(x1))] 753.95/297.36 753.95/297.36 [a24(x1)] = [1 1] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 1] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [a23(a34(a23(x1)))] 753.95/297.36 753.95/297.36 [a24(a24(x1))] = [1 2] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a25(x1)] = [1 2] x1 + [1] 753.95/297.36 [0 1] [2] 753.95/297.36 > [1 2] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.36 753.95/297.36 [a25(a25(x1))] = [1 4] x1 + [6] 753.95/297.36 [0 1] [4] 753.95/297.36 > [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a26(x1)] = [1 2] x1 + [2] 753.95/297.36 [0 1] [1] 753.95/297.36 > [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.36 753.95/297.36 [a26(a26(x1))] = [1 4] x1 + [6] 753.95/297.36 [0 1] [2] 753.95/297.36 > [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a34(a34(x1))] = [1 2] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a34(a45(a34(a45(a34(a45(x1))))))] = [1 3] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a34(a56(x1))] = [1 1] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 > [1 1] x1 + [0] 753.95/297.36 [0 1] [1] 753.95/297.36 = [a56(a34(x1))] 753.95/297.36 753.95/297.36 [a35(x1)] = [1 2] x1 + [1] 753.95/297.36 [0 1] [2] 753.95/297.36 > [1 2] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [a34(a45(a34(x1)))] 753.95/297.36 753.95/297.36 [a35(a35(x1))] = [1 4] x1 + [6] 753.95/297.36 [0 1] [4] 753.95/297.36 > [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a36(x1)] = [1 2] x1 + [2] 753.95/297.36 [0 1] [1] 753.95/297.36 > [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.36 753.95/297.36 [a36(a36(x1))] = [1 4] x1 + [6] 753.95/297.36 [0 1] [2] 753.95/297.36 > [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a45(a45(x1))] = [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a45(a56(a45(a56(a45(a56(x1))))))] = [1 0] x1 + [0] 753.95/297.36 [0 1] [3] 753.95/297.36 >= [1 0] x1 + [0] 753.95/297.36 [0 1] [0] 753.95/297.36 = [x1] 753.95/297.36 753.95/297.36 [a46(x1)] = [1 2] x1 + [1] 753.95/297.36 [0 1] [1] 753.95/297.36 > [1 0] x1 + [0] 753.95/297.36 [0 1] [1] 753.95/297.36 = [a45(a56(a45(x1)))] 753.95/297.36 753.95/297.36 [a46(a46(x1))] = [1 4] x1 + [4] 753.95/297.36 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a56(a56(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [2] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 753.95/297.37 We return to the main proof. 753.95/297.37 753.95/297.37 We are left with following problem, upon which TcT provides the 753.95/297.37 certificate YES(O(1),O(n^2)). 753.95/297.37 753.95/297.37 Strict Trs: 753.95/297.37 { a12(a34(x1)) -> a34(a12(x1)) 753.95/297.37 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.37 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.37 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.37 , a23(a56(x1)) -> a56(a23(x1)) } 753.95/297.37 Weak Trs: 753.95/297.37 { a12(a12(x1)) -> x1 753.95/297.37 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.37 , a13(x1) -> a12(a23(a12(x1))) 753.95/297.37 , a13(a13(x1)) -> x1 753.95/297.37 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.37 , a14(a14(x1)) -> x1 753.95/297.37 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.37 , a15(a15(x1)) -> x1 753.95/297.37 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.37 , a16(a16(x1)) -> x1 753.95/297.37 , a23(a23(x1)) -> x1 753.95/297.37 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.37 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.37 , a24(a24(x1)) -> x1 753.95/297.37 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.37 , a25(a25(x1)) -> x1 753.95/297.37 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.37 , a26(a26(x1)) -> x1 753.95/297.37 , a34(a34(x1)) -> x1 753.95/297.37 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.37 , a34(a56(x1)) -> a56(a34(x1)) 753.95/297.37 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.37 , a35(a35(x1)) -> x1 753.95/297.37 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.37 , a36(a36(x1)) -> x1 753.95/297.37 , a45(a45(x1)) -> x1 753.95/297.37 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.37 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.37 , a46(a46(x1)) -> x1 753.95/297.37 , a56(a56(x1)) -> x1 } 753.95/297.37 Obligation: 753.95/297.37 derivational complexity 753.95/297.37 Answer: 753.95/297.37 YES(O(1),O(n^2)) 753.95/297.37 753.95/297.37 We use the processor 'matrix interpretation of dimension 2' to 753.95/297.37 orient following rules strictly. 753.95/297.37 753.95/297.37 Trs: { a12(a56(x1)) -> a56(a12(x1)) } 753.95/297.37 753.95/297.37 The induced complexity on above rules (modulo remaining rules) is 753.95/297.37 YES(?,O(n^2)) . These rules are moved into the corresponding weak 753.95/297.37 component(s). 753.95/297.37 753.95/297.37 Sub-proof: 753.95/297.37 ---------- 753.95/297.37 TcT has computed the following triangular matrix interpretation. 753.95/297.37 753.95/297.37 [a12](x1) = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a13](x1) = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a14](x1) = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a15](x1) = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a16](x1) = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a23](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a24](x1) = [1 2] x1 + [1] 753.95/297.37 [0 1] [2] 753.95/297.37 753.95/297.37 [a25](x1) = [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a26](x1) = [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a34](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a35](x1) = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a36](x1) = [1 1] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a45](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a46](x1) = [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a56](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 The order satisfies the following ordering constraints: 753.95/297.37 753.95/297.37 [a12(a12(x1))] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a12(a23(a12(a23(a12(a23(x1))))))] = [1 3] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a12(a34(x1))] = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a34(a12(x1))] 753.95/297.37 753.95/297.37 [a12(a45(x1))] = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a45(a12(x1))] 753.95/297.37 753.95/297.37 [a12(a56(x1))] = [1 1] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 1] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a56(a12(x1))] 753.95/297.37 753.95/297.37 [a13(x1)] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a12(a23(a12(x1)))] 753.95/297.37 753.95/297.37 [a13(a13(x1))] = [1 4] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a14(x1)] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.37 753.95/297.37 [a14(a14(x1))] = [1 4] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a15(x1)] = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.37 753.95/297.37 [a15(a15(x1))] = [1 4] x1 + [6] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a16(x1)] = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.37 753.95/297.37 [a16(a16(x1))] = [1 4] x1 + [6] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a23(a23(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a23(a34(a23(a34(a23(a34(x1))))))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a23(a45(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a45(a23(x1))] 753.95/297.37 753.95/297.37 [a23(a56(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a56(a23(x1))] 753.95/297.37 753.95/297.37 [a24(x1)] = [1 2] x1 + [1] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a23(a34(a23(x1)))] 753.95/297.37 753.95/297.37 [a24(a24(x1))] = [1 4] x1 + [6] 753.95/297.37 [0 1] [4] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a25(x1)] = [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.37 753.95/297.37 [a25(a25(x1))] = [1 4] x1 + [4] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a26(x1)] = [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.37 753.95/297.37 [a26(a26(x1))] = [1 4] x1 + [4] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a34(a34(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a34(a45(a34(a45(a34(a45(x1))))))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a34(a56(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a56(a34(x1))] 753.95/297.37 753.95/297.37 [a35(x1)] = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a34(a45(a34(x1)))] 753.95/297.37 753.95/297.37 [a35(a35(x1))] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a36(x1)] = [1 1] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.37 753.95/297.37 [a36(a36(x1))] = [1 2] x1 + [5] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a45(a45(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a45(a56(a45(a56(a45(a56(x1))))))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [3] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a46(x1)] = [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a45(a56(a45(x1)))] 753.95/297.37 753.95/297.37 [a46(a46(x1))] = [1 4] x1 + [4] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a56(a56(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [2] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 753.95/297.37 We return to the main proof. 753.95/297.37 753.95/297.37 We are left with following problem, upon which TcT provides the 753.95/297.37 certificate YES(O(1),O(n^2)). 753.95/297.37 753.95/297.37 Strict Trs: 753.95/297.37 { a12(a34(x1)) -> a34(a12(x1)) 753.95/297.37 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.37 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.37 , a23(a56(x1)) -> a56(a23(x1)) } 753.95/297.37 Weak Trs: 753.95/297.37 { a12(a12(x1)) -> x1 753.95/297.37 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.37 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.37 , a13(x1) -> a12(a23(a12(x1))) 753.95/297.37 , a13(a13(x1)) -> x1 753.95/297.37 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.37 , a14(a14(x1)) -> x1 753.95/297.37 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.37 , a15(a15(x1)) -> x1 753.95/297.37 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.37 , a16(a16(x1)) -> x1 753.95/297.37 , a23(a23(x1)) -> x1 753.95/297.37 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.37 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.37 , a24(a24(x1)) -> x1 753.95/297.37 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.37 , a25(a25(x1)) -> x1 753.95/297.37 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.37 , a26(a26(x1)) -> x1 753.95/297.37 , a34(a34(x1)) -> x1 753.95/297.37 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.37 , a34(a56(x1)) -> a56(a34(x1)) 753.95/297.37 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.37 , a35(a35(x1)) -> x1 753.95/297.37 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.37 , a36(a36(x1)) -> x1 753.95/297.37 , a45(a45(x1)) -> x1 753.95/297.37 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.37 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.37 , a46(a46(x1)) -> x1 753.95/297.37 , a56(a56(x1)) -> x1 } 753.95/297.37 Obligation: 753.95/297.37 derivational complexity 753.95/297.37 Answer: 753.95/297.37 YES(O(1),O(n^2)) 753.95/297.37 753.95/297.37 We use the processor 'matrix interpretation of dimension 2' to 753.95/297.37 orient following rules strictly. 753.95/297.37 753.95/297.37 Trs: { a23(a56(x1)) -> a56(a23(x1)) } 753.95/297.37 753.95/297.37 The induced complexity on above rules (modulo remaining rules) is 753.95/297.37 YES(?,O(n^2)) . These rules are moved into the corresponding weak 753.95/297.37 component(s). 753.95/297.37 753.95/297.37 Sub-proof: 753.95/297.37 ---------- 753.95/297.37 TcT has computed the following triangular matrix interpretation. 753.95/297.37 753.95/297.37 [a12](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a13](x1) = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a14](x1) = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a15](x1) = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a16](x1) = [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a23](x1) = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a24](x1) = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a25](x1) = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a26](x1) = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a34](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a35](x1) = [1 2] x1 + [1] 753.95/297.37 [0 1] [2] 753.95/297.37 753.95/297.37 [a36](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a45](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a46](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a56](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 The order satisfies the following ordering constraints: 753.95/297.37 753.95/297.37 [a12(a12(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a12(a23(a12(a23(a12(a23(x1))))))] = [1 3] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a12(a34(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a34(a12(x1))] 753.95/297.37 753.95/297.37 [a12(a45(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a45(a12(x1))] 753.95/297.37 753.95/297.37 [a12(a56(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a56(a12(x1))] 753.95/297.37 753.95/297.37 [a13(x1)] = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a12(a23(a12(x1)))] 753.95/297.37 753.95/297.37 [a13(a13(x1))] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a14(x1)] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.37 753.95/297.37 [a14(a14(x1))] = [1 4] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a15(x1)] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.37 753.95/297.37 [a15(a15(x1))] = [1 4] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a16(x1)] = [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 >= [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.37 753.95/297.37 [a16(a16(x1))] = [1 4] x1 + [4] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a23(a23(x1))] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a23(a34(a23(a34(a23(a34(x1))))))] = [1 3] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a23(a45(x1))] = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a45(a23(x1))] 753.95/297.37 753.95/297.37 [a23(a56(x1))] = [1 1] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 1] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a56(a23(x1))] 753.95/297.37 753.95/297.37 [a24(x1)] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a23(a34(a23(x1)))] 753.95/297.37 753.95/297.37 [a24(a24(x1))] = [1 4] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a25(x1)] = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.37 753.95/297.37 [a25(a25(x1))] = [1 4] x1 + [6] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a26(x1)] = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.37 753.95/297.37 [a26(a26(x1))] = [1 4] x1 + [6] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a34(a34(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a34(a45(a34(a45(a34(a45(x1))))))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a34(a56(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a56(a34(x1))] 753.95/297.37 753.95/297.37 [a35(x1)] = [1 2] x1 + [1] 753.95/297.37 [0 1] [2] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a34(a45(a34(x1)))] 753.95/297.37 753.95/297.37 [a35(a35(x1))] = [1 4] x1 + [6] 753.95/297.37 [0 1] [4] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a36(x1)] = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.37 753.95/297.37 [a36(a36(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [2] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a45(a45(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a45(a56(a45(a56(a45(a56(x1))))))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [3] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a46(x1)] = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a45(a56(a45(x1)))] 753.95/297.37 753.95/297.37 [a46(a46(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [2] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a56(a56(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [2] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 753.95/297.37 We return to the main proof. 753.95/297.37 753.95/297.37 We are left with following problem, upon which TcT provides the 753.95/297.37 certificate YES(O(1),O(n^2)). 753.95/297.37 753.95/297.37 Strict Trs: 753.95/297.37 { a12(a34(x1)) -> a34(a12(x1)) 753.95/297.37 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.37 , a23(a45(x1)) -> a45(a23(x1)) } 753.95/297.37 Weak Trs: 753.95/297.37 { a12(a12(x1)) -> x1 753.95/297.37 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.37 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.37 , a13(x1) -> a12(a23(a12(x1))) 753.95/297.37 , a13(a13(x1)) -> x1 753.95/297.37 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.37 , a14(a14(x1)) -> x1 753.95/297.37 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.37 , a15(a15(x1)) -> x1 753.95/297.37 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.37 , a16(a16(x1)) -> x1 753.95/297.37 , a23(a23(x1)) -> x1 753.95/297.37 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.37 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.37 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.37 , a24(a24(x1)) -> x1 753.95/297.37 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.37 , a25(a25(x1)) -> x1 753.95/297.37 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.37 , a26(a26(x1)) -> x1 753.95/297.37 , a34(a34(x1)) -> x1 753.95/297.37 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.37 , a34(a56(x1)) -> a56(a34(x1)) 753.95/297.37 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.37 , a35(a35(x1)) -> x1 753.95/297.37 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.37 , a36(a36(x1)) -> x1 753.95/297.37 , a45(a45(x1)) -> x1 753.95/297.37 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.37 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.37 , a46(a46(x1)) -> x1 753.95/297.37 , a56(a56(x1)) -> x1 } 753.95/297.37 Obligation: 753.95/297.37 derivational complexity 753.95/297.37 Answer: 753.95/297.37 YES(O(1),O(n^2)) 753.95/297.37 753.95/297.37 We use the processor 'matrix interpretation of dimension 2' to 753.95/297.37 orient following rules strictly. 753.95/297.37 753.95/297.37 Trs: { a23(a45(x1)) -> a45(a23(x1)) } 753.95/297.37 753.95/297.37 The induced complexity on above rules (modulo remaining rules) is 753.95/297.37 YES(?,O(n^2)) . These rules are moved into the corresponding weak 753.95/297.37 component(s). 753.95/297.37 753.95/297.37 Sub-proof: 753.95/297.37 ---------- 753.95/297.37 TcT has computed the following triangular matrix interpretation. 753.95/297.37 753.95/297.37 [a12](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a13](x1) = [1 1] x1 + [16] 753.95/297.37 [0 1] [16] 753.95/297.37 753.95/297.37 [a14](x1) = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a15](x1) = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a16](x1) = [1 8] x1 + [4] 753.95/297.37 [0 1] [2] 753.95/297.37 753.95/297.37 [a23](x1) = [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a24](x1) = [1 16] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a25](x1) = [1 16] x1 + [16] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a26](x1) = [1 3] x1 + [4] 753.95/297.37 [0 1] [6] 753.95/297.37 753.95/297.37 [a34](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 [a35](x1) = [1 0] x1 + [16] 753.95/297.37 [0 1] [16] 753.95/297.37 753.95/297.37 [a36](x1) = [1 4] x1 + [8] 753.95/297.37 [0 1] [2] 753.95/297.37 753.95/297.37 [a45](x1) = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 753.95/297.37 [a46](x1) = [1 0] x1 + [4] 753.95/297.37 [0 1] [16] 753.95/297.37 753.95/297.37 [a56](x1) = [1 0] x1 + [2] 753.95/297.37 [0 1] [0] 753.95/297.37 753.95/297.37 The order satisfies the following ordering constraints: 753.95/297.37 753.95/297.37 [a12(a12(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a12(a23(a12(a23(a12(a23(x1))))))] = [1 3] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a12(a34(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a34(a12(x1))] 753.95/297.37 753.95/297.37 [a12(a45(x1))] = [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a45(a12(x1))] 753.95/297.37 753.95/297.37 [a12(a56(x1))] = [1 0] x1 + [2] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [2] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a56(a12(x1))] 753.95/297.37 753.95/297.37 [a13(x1)] = [1 1] x1 + [16] 753.95/297.37 [0 1] [16] 753.95/297.37 > [1 1] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a12(a23(a12(x1)))] 753.95/297.37 753.95/297.37 [a13(a13(x1))] = [1 2] x1 + [48] 753.95/297.37 [0 1] [32] 753.95/297.37 > [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a14(x1)] = [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 2] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.37 753.95/297.37 [a14(a14(x1))] = [1 4] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 >= [1 0] x1 + [0] 753.95/297.37 [0 1] [0] 753.95/297.37 = [x1] 753.95/297.37 753.95/297.37 [a15(x1)] = [1 2] x1 + [2] 753.95/297.37 [0 1] [1] 753.95/297.37 > [1 2] x1 + [1] 753.95/297.37 [0 1] [1] 753.95/297.37 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.37 753.95/297.38 [a15(a15(x1))] = [1 4] x1 + [6] 753.95/297.38 [0 1] [2] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a16(x1)] = [1 8] x1 + [4] 753.95/297.38 [0 1] [2] 753.95/297.38 >= [1 2] x1 + [4] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.38 753.95/297.38 [a16(a16(x1))] = [1 16] x1 + [24] 753.95/297.38 [0 1] [4] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a23(a23(x1))] = [1 2] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a23(a34(a23(a34(a23(a34(x1))))))] = [1 3] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a23(a45(x1))] = [1 1] x1 + [1] 753.95/297.38 [0 1] [1] 753.95/297.38 > [1 1] x1 + [0] 753.95/297.38 [0 1] [1] 753.95/297.38 = [a45(a23(x1))] 753.95/297.38 753.95/297.38 [a23(a56(x1))] = [1 1] x1 + [2] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 1] x1 + [2] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a56(a23(x1))] 753.95/297.38 753.95/297.38 [a24(x1)] = [1 16] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 2] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a23(a34(a23(x1)))] 753.95/297.38 753.95/297.38 [a24(a24(x1))] = [1 32] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a25(x1)] = [1 16] x1 + [16] 753.95/297.38 [0 1] [1] 753.95/297.38 > [1 2] x1 + [1] 753.95/297.38 [0 1] [1] 753.95/297.38 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.38 753.95/297.38 [a25(a25(x1))] = [1 32] x1 + [48] 753.95/297.38 [0 1] [2] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a26(x1)] = [1 3] x1 + [4] 753.95/297.38 [0 1] [6] 753.95/297.38 >= [1 2] x1 + [4] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.38 753.95/297.38 [a26(a26(x1))] = [1 6] x1 + [26] 753.95/297.38 [0 1] [12] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a34(a34(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a34(a45(a34(a45(a34(a45(x1))))))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [3] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a34(a56(x1))] = [1 0] x1 + [2] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [2] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a56(a34(x1))] 753.95/297.38 753.95/297.38 [a35(x1)] = [1 0] x1 + [16] 753.95/297.38 [0 1] [16] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [1] 753.95/297.38 = [a34(a45(a34(x1)))] 753.95/297.38 753.95/297.38 [a35(a35(x1))] = [1 0] x1 + [32] 753.95/297.38 [0 1] [32] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a36(x1)] = [1 4] x1 + [8] 753.95/297.38 [0 1] [2] 753.95/297.38 > [1 0] x1 + [2] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.38 753.95/297.38 [a36(a36(x1))] = [1 8] x1 + [24] 753.95/297.38 [0 1] [4] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a45(a45(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [2] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a45(a56(a45(a56(a45(a56(x1))))))] = [1 0] x1 + [6] 753.95/297.38 [0 1] [3] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a46(x1)] = [1 0] x1 + [4] 753.95/297.38 [0 1] [16] 753.95/297.38 > [1 0] x1 + [2] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a45(a56(a45(x1)))] 753.95/297.38 753.95/297.38 [a46(a46(x1))] = [1 0] x1 + [8] 753.95/297.38 [0 1] [32] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a56(a56(x1))] = [1 0] x1 + [4] 753.95/297.38 [0 1] [0] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 753.95/297.38 We return to the main proof. 753.95/297.38 753.95/297.38 We are left with following problem, upon which TcT provides the 753.95/297.38 certificate YES(O(1),O(n^2)). 753.95/297.38 753.95/297.38 Strict Trs: 753.95/297.38 { a12(a34(x1)) -> a34(a12(x1)) 753.95/297.38 , a12(a45(x1)) -> a45(a12(x1)) } 753.95/297.38 Weak Trs: 753.95/297.38 { a12(a12(x1)) -> x1 753.95/297.38 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.38 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.38 , a13(x1) -> a12(a23(a12(x1))) 753.95/297.38 , a13(a13(x1)) -> x1 753.95/297.38 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.38 , a14(a14(x1)) -> x1 753.95/297.38 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.38 , a15(a15(x1)) -> x1 753.95/297.38 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.38 , a16(a16(x1)) -> x1 753.95/297.38 , a23(a23(x1)) -> x1 753.95/297.38 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.38 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.38 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.38 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.38 , a24(a24(x1)) -> x1 753.95/297.38 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.38 , a25(a25(x1)) -> x1 753.95/297.38 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.38 , a26(a26(x1)) -> x1 753.95/297.38 , a34(a34(x1)) -> x1 753.95/297.38 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.38 , a34(a56(x1)) -> a56(a34(x1)) 753.95/297.38 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.38 , a35(a35(x1)) -> x1 753.95/297.38 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.38 , a36(a36(x1)) -> x1 753.95/297.38 , a45(a45(x1)) -> x1 753.95/297.38 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.38 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.38 , a46(a46(x1)) -> x1 753.95/297.38 , a56(a56(x1)) -> x1 } 753.95/297.38 Obligation: 753.95/297.38 derivational complexity 753.95/297.38 Answer: 753.95/297.38 YES(O(1),O(n^2)) 753.95/297.38 753.95/297.38 We use the processor 'matrix interpretation of dimension 2' to 753.95/297.38 orient following rules strictly. 753.95/297.38 753.95/297.38 Trs: { a12(a45(x1)) -> a45(a12(x1)) } 753.95/297.38 753.95/297.38 The induced complexity on above rules (modulo remaining rules) is 753.95/297.38 YES(?,O(n^2)) . These rules are moved into the corresponding weak 753.95/297.38 component(s). 753.95/297.38 753.95/297.38 Sub-proof: 753.95/297.38 ---------- 753.95/297.38 TcT has computed the following triangular matrix interpretation. 753.95/297.38 753.95/297.38 [a12](x1) = [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 [a13](x1) = [1 4] x1 + [0] 753.95/297.38 [0 1] [8] 753.95/297.38 753.95/297.38 [a14](x1) = [1 16] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 [a15](x1) = [1 2] x1 + [16] 753.95/297.38 [0 1] [8] 753.95/297.38 753.95/297.38 [a16](x1) = [1 2] x1 + [8] 753.95/297.38 [0 1] [16] 753.95/297.38 753.95/297.38 [a23](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 [a24](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 753.95/297.38 [a25](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 753.95/297.38 [a26](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [12] 753.95/297.38 753.95/297.38 [a34](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 [a35](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 753.95/297.38 [a36](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 753.95/297.38 [a45](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [4] 753.95/297.38 753.95/297.38 [a46](x1) = [1 1] x1 + [16] 753.95/297.38 [0 1] [16] 753.95/297.38 753.95/297.38 [a56](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 The order satisfies the following ordering constraints: 753.95/297.38 753.95/297.38 [a12(a12(x1))] = [1 2] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a12(a23(a12(a23(a12(a23(x1))))))] = [1 3] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a12(a34(x1))] = [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a34(a12(x1))] 753.95/297.38 753.95/297.38 [a12(a45(x1))] = [1 1] x1 + [4] 753.95/297.38 [0 1] [4] 753.95/297.38 > [1 1] x1 + [0] 753.95/297.38 [0 1] [4] 753.95/297.38 = [a45(a12(x1))] 753.95/297.38 753.95/297.38 [a12(a56(x1))] = [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a56(a12(x1))] 753.95/297.38 753.95/297.38 [a13(x1)] = [1 4] x1 + [0] 753.95/297.38 [0 1] [8] 753.95/297.38 >= [1 2] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a12(a23(a12(x1)))] 753.95/297.38 753.95/297.38 [a13(a13(x1))] = [1 8] x1 + [32] 753.95/297.38 [0 1] [16] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a14(x1)] = [1 16] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 2] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.38 753.95/297.38 [a14(a14(x1))] = [1 32] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a15(x1)] = [1 2] x1 + [16] 753.95/297.38 [0 1] [8] 753.95/297.38 > [1 2] x1 + [4] 753.95/297.38 [0 1] [4] 753.95/297.38 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.38 753.95/297.38 [a15(a15(x1))] = [1 4] x1 + [48] 753.95/297.38 [0 1] [16] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a16(x1)] = [1 2] x1 + [8] 753.95/297.38 [0 1] [16] 753.95/297.38 >= [1 2] x1 + [8] 753.95/297.38 [0 1] [8] 753.95/297.38 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.38 753.95/297.38 [a16(a16(x1))] = [1 4] x1 + [48] 753.95/297.38 [0 1] [32] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a23(a23(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a23(a34(a23(a34(a23(a34(x1))))))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a23(a45(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [4] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [4] 753.95/297.38 = [a45(a23(x1))] 753.95/297.38 753.95/297.38 [a23(a56(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a56(a23(x1))] 753.95/297.38 753.95/297.38 [a24(x1)] = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a23(a34(a23(x1)))] 753.95/297.38 753.95/297.38 [a24(a24(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [32] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a25(x1)] = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [4] 753.95/297.38 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.38 753.95/297.38 [a25(a25(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [32] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a26(x1)] = [1 0] x1 + [0] 753.95/297.38 [0 1] [12] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [8] 753.95/297.38 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.38 753.95/297.38 [a26(a26(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [24] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a34(a34(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a34(a45(a34(a45(a34(a45(x1))))))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [12] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a34(a56(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a56(a34(x1))] 753.95/297.38 753.95/297.38 [a35(x1)] = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [4] 753.95/297.38 = [a34(a45(a34(x1)))] 753.95/297.38 753.95/297.38 [a35(a35(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [32] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a36(x1)] = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [8] 753.95/297.38 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.38 753.95/297.38 [a36(a36(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [32] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a45(a45(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [8] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a45(a56(a45(a56(a45(a56(x1))))))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [12] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a46(x1)] = [1 1] x1 + [16] 753.95/297.38 [0 1] [16] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [8] 753.95/297.38 = [a45(a56(a45(x1)))] 753.95/297.38 753.95/297.38 [a46(a46(x1))] = [1 2] x1 + [48] 753.95/297.38 [0 1] [32] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a56(a56(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 753.95/297.38 We return to the main proof. 753.95/297.38 753.95/297.38 We are left with following problem, upon which TcT provides the 753.95/297.38 certificate YES(O(1),O(n^2)). 753.95/297.38 753.95/297.38 Strict Trs: { a12(a34(x1)) -> a34(a12(x1)) } 753.95/297.38 Weak Trs: 753.95/297.38 { a12(a12(x1)) -> x1 753.95/297.38 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.38 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.38 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.38 , a13(x1) -> a12(a23(a12(x1))) 753.95/297.38 , a13(a13(x1)) -> x1 753.95/297.38 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.38 , a14(a14(x1)) -> x1 753.95/297.38 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.38 , a15(a15(x1)) -> x1 753.95/297.38 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.38 , a16(a16(x1)) -> x1 753.95/297.38 , a23(a23(x1)) -> x1 753.95/297.38 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.38 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.38 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.38 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.38 , a24(a24(x1)) -> x1 753.95/297.38 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.38 , a25(a25(x1)) -> x1 753.95/297.38 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.38 , a26(a26(x1)) -> x1 753.95/297.38 , a34(a34(x1)) -> x1 753.95/297.38 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.38 , a34(a56(x1)) -> a56(a34(x1)) 753.95/297.38 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.38 , a35(a35(x1)) -> x1 753.95/297.38 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.38 , a36(a36(x1)) -> x1 753.95/297.38 , a45(a45(x1)) -> x1 753.95/297.38 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.38 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.38 , a46(a46(x1)) -> x1 753.95/297.38 , a56(a56(x1)) -> x1 } 753.95/297.38 Obligation: 753.95/297.38 derivational complexity 753.95/297.38 Answer: 753.95/297.38 YES(O(1),O(n^2)) 753.95/297.38 753.95/297.38 We use the processor 'matrix interpretation of dimension 2' to 753.95/297.38 orient following rules strictly. 753.95/297.38 753.95/297.38 Trs: { a12(a34(x1)) -> a34(a12(x1)) } 753.95/297.38 753.95/297.38 The induced complexity on above rules (modulo remaining rules) is 753.95/297.38 YES(?,O(n^2)) . These rules are moved into the corresponding weak 753.95/297.38 component(s). 753.95/297.38 753.95/297.38 Sub-proof: 753.95/297.38 ---------- 753.95/297.38 TcT has computed the following triangular matrix interpretation. 753.95/297.38 753.95/297.38 [a12](x1) = [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 [a13](x1) = [1 16] x1 + [16] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 [a14](x1) = [1 16] x1 + [2] 753.95/297.38 [0 1] [2] 753.95/297.38 753.95/297.38 [a15](x1) = [1 17] x1 + [2] 753.95/297.38 [0 1] [2] 753.95/297.38 753.95/297.38 [a16](x1) = [1 9] x1 + [4] 753.95/297.38 [0 1] [4] 753.95/297.38 753.95/297.38 [a23](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 [a24](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 753.95/297.38 [a25](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 753.95/297.38 [a26](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 753.95/297.38 [a34](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [1] 753.95/297.38 753.95/297.38 [a35](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [2] 753.95/297.38 753.95/297.38 [a36](x1) = [1 8] x1 + [16] 753.95/297.38 [0 1] [2] 753.95/297.38 753.95/297.38 [a45](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 [a46](x1) = [1 16] x1 + [16] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 [a56](x1) = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 753.95/297.38 The order satisfies the following ordering constraints: 753.95/297.38 753.95/297.38 [a12(a12(x1))] = [1 2] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a12(a23(a12(a23(a12(a23(x1))))))] = [1 3] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a12(a34(x1))] = [1 1] x1 + [1] 753.95/297.38 [0 1] [1] 753.95/297.38 > [1 1] x1 + [0] 753.95/297.38 [0 1] [1] 753.95/297.38 = [a34(a12(x1))] 753.95/297.38 753.95/297.38 [a12(a45(x1))] = [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a45(a12(x1))] 753.95/297.38 753.95/297.38 [a12(a56(x1))] = [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 1] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a56(a12(x1))] 753.95/297.38 753.95/297.38 [a13(x1)] = [1 16] x1 + [16] 753.95/297.38 [0 1] [0] 753.95/297.38 > [1 2] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a12(a23(a12(x1)))] 753.95/297.38 753.95/297.38 [a13(a13(x1))] = [1 32] x1 + [32] 753.95/297.38 [0 1] [0] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a14(x1)] = [1 16] x1 + [2] 753.95/297.38 [0 1] [2] 753.95/297.38 > [1 2] x1 + [1] 753.95/297.38 [0 1] [1] 753.95/297.38 = [a12(a23(a34(a23(a12(x1)))))] 753.95/297.38 753.95/297.38 [a14(a14(x1))] = [1 32] x1 + [36] 753.95/297.38 [0 1] [4] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a15(x1)] = [1 17] x1 + [2] 753.95/297.38 [0 1] [2] 753.95/297.38 >= [1 2] x1 + [2] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a12(a23(a34(a45(a34(a23(a12(x1)))))))] 753.95/297.38 753.95/297.38 [a15(a15(x1))] = [1 34] x1 + [38] 753.95/297.38 [0 1] [4] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a16(x1)] = [1 9] x1 + [4] 753.95/297.38 [0 1] [4] 753.95/297.38 > [1 2] x1 + [2] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))] 753.95/297.38 753.95/297.38 [a16(a16(x1))] = [1 18] x1 + [44] 753.95/297.38 [0 1] [8] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a23(a23(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a23(a34(a23(a34(a23(a34(x1))))))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [3] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a23(a45(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a45(a23(x1))] 753.95/297.38 753.95/297.38 [a23(a56(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a56(a23(x1))] 753.95/297.38 753.95/297.38 [a24(x1)] = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [1] 753.95/297.38 = [a23(a34(a23(x1)))] 753.95/297.38 753.95/297.38 [a24(a24(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [32] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a25(x1)] = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a23(a34(a45(a34(a23(x1)))))] 753.95/297.38 753.95/297.38 [a25(a25(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [32] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a26(x1)] = [1 0] x1 + [0] 753.95/297.38 [0 1] [16] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a23(a34(a45(a56(a45(a34(a23(x1)))))))] 753.95/297.38 753.95/297.38 [a26(a26(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [32] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a34(a34(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [2] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a34(a45(a34(a45(a34(a45(x1))))))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [3] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a34(a56(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [1] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [1] 753.95/297.38 = [a56(a34(x1))] 753.95/297.38 753.95/297.38 [a35(x1)] = [1 0] x1 + [0] 753.95/297.38 [0 1] [2] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a34(a45(a34(x1)))] 753.95/297.38 753.95/297.38 [a35(a35(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [4] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a36(x1)] = [1 8] x1 + [16] 753.95/297.38 [0 1] [2] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [2] 753.95/297.38 = [a34(a45(a56(a45(a34(x1)))))] 753.95/297.38 753.95/297.38 [a36(a36(x1))] = [1 16] x1 + [48] 753.95/297.38 [0 1] [4] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a45(a45(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a45(a56(a45(a56(a45(a56(x1))))))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a46(x1)] = [1 16] x1 + [16] 753.95/297.38 [0 1] [0] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [a45(a56(a45(x1)))] 753.95/297.38 753.95/297.38 [a46(a46(x1))] = [1 32] x1 + [32] 753.95/297.38 [0 1] [0] 753.95/297.38 > [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 [a56(a56(x1))] = [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 >= [1 0] x1 + [0] 753.95/297.38 [0 1] [0] 753.95/297.38 = [x1] 753.95/297.38 753.95/297.38 753.95/297.38 We return to the main proof. 753.95/297.38 753.95/297.38 We are left with following problem, upon which TcT provides the 753.95/297.38 certificate YES(O(1),O(1)). 753.95/297.38 753.95/297.38 Weak Trs: 753.95/297.38 { a12(a12(x1)) -> x1 753.95/297.38 , a12(a23(a12(a23(a12(a23(x1)))))) -> x1 753.95/297.38 , a12(a34(x1)) -> a34(a12(x1)) 753.95/297.38 , a12(a45(x1)) -> a45(a12(x1)) 753.95/297.38 , a12(a56(x1)) -> a56(a12(x1)) 753.95/297.38 , a13(x1) -> a12(a23(a12(x1))) 753.95/297.38 , a13(a13(x1)) -> x1 753.95/297.38 , a14(x1) -> a12(a23(a34(a23(a12(x1))))) 753.95/297.38 , a14(a14(x1)) -> x1 753.95/297.38 , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) 753.95/297.38 , a15(a15(x1)) -> x1 753.95/297.38 , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) 753.95/297.38 , a16(a16(x1)) -> x1 753.95/297.38 , a23(a23(x1)) -> x1 753.95/297.38 , a23(a34(a23(a34(a23(a34(x1)))))) -> x1 753.95/297.38 , a23(a45(x1)) -> a45(a23(x1)) 753.95/297.38 , a23(a56(x1)) -> a56(a23(x1)) 753.95/297.38 , a24(x1) -> a23(a34(a23(x1))) 753.95/297.38 , a24(a24(x1)) -> x1 753.95/297.38 , a25(x1) -> a23(a34(a45(a34(a23(x1))))) 753.95/297.38 , a25(a25(x1)) -> x1 753.95/297.38 , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) 753.95/297.38 , a26(a26(x1)) -> x1 753.95/297.38 , a34(a34(x1)) -> x1 753.95/297.38 , a34(a45(a34(a45(a34(a45(x1)))))) -> x1 753.95/297.38 , a34(a56(x1)) -> a56(a34(x1)) 753.95/297.38 , a35(x1) -> a34(a45(a34(x1))) 753.95/297.38 , a35(a35(x1)) -> x1 753.95/297.38 , a36(x1) -> a34(a45(a56(a45(a34(x1))))) 753.95/297.38 , a36(a36(x1)) -> x1 753.95/297.38 , a45(a45(x1)) -> x1 753.95/297.38 , a45(a56(a45(a56(a45(a56(x1)))))) -> x1 753.95/297.38 , a46(x1) -> a45(a56(a45(x1))) 753.95/297.38 , a46(a46(x1)) -> x1 753.95/297.38 , a56(a56(x1)) -> x1 } 753.95/297.38 Obligation: 753.95/297.38 derivational complexity 753.95/297.38 Answer: 753.95/297.38 YES(O(1),O(1)) 753.95/297.38 753.95/297.38 Empty rules are trivially bounded 753.95/297.38 753.95/297.38 Hurray, we answered YES(O(1),O(n^2)) 754.23/297.53 EOF