YES(O(1),O(n^6)) 1064.60/297.06 YES(O(1),O(n^6)) 1064.60/297.06 1064.60/297.06 We are left with following problem, upon which TcT provides the 1064.60/297.06 certificate YES(O(1),O(n^6)). 1064.60/297.06 1064.60/297.06 Strict Trs: 1064.60/297.06 { a12(a12(a12(a12(x1)))) -> x1 1064.60/297.06 , a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> 1064.60/297.06 x1 1064.60/297.06 , a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) 1064.60/297.06 , a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) 1064.60/297.06 , a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) 1064.60/297.06 , a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) 1064.60/297.06 , a13(a13(a13(a13(x1)))) -> x1 1064.60/297.06 , a14(a14(x1)) -> 1064.60/297.06 a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) 1064.60/297.06 , a14(a14(a14(a14(x1)))) -> x1 1064.60/297.06 , a15(a15(x1)) -> 1064.60/297.06 a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) 1064.60/297.06 , a15(a15(a15(a15(x1)))) -> x1 1064.60/297.06 , a16(a16(x1)) -> 1064.60/297.06 a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) 1064.60/297.06 , a16(a16(a16(a16(x1)))) -> x1 1064.60/297.06 , a23(a23(a23(a23(x1)))) -> x1 1064.60/297.06 , a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> 1064.60/297.06 x1 1064.60/297.06 , a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) 1064.60/297.06 , a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) 1064.60/297.06 , a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) 1064.60/297.06 , a24(a24(a24(a24(x1)))) -> x1 1064.60/297.06 , a25(a25(x1)) -> 1064.60/297.06 a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) 1064.60/297.06 , a25(a25(a25(a25(x1)))) -> x1 1064.60/297.06 , a26(a26(x1)) -> 1064.60/297.06 a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) 1064.60/297.06 , a26(a26(a26(a26(x1)))) -> x1 1064.60/297.06 , a34(a34(a34(a34(x1)))) -> x1 1064.60/297.06 , a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> 1064.60/297.06 x1 1064.60/297.06 , a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) 1064.60/297.06 , a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) 1064.60/297.06 , a35(a35(a35(a35(x1)))) -> x1 1064.60/297.06 , a36(a36(x1)) -> 1064.60/297.06 a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) 1064.60/297.06 , a36(a36(a36(a36(x1)))) -> x1 1064.60/297.06 , a45(a45(a45(a45(x1)))) -> x1 1064.60/297.06 , a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> 1064.60/297.06 x1 1064.60/297.06 , a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) 1064.60/297.06 , a46(a46(a46(a46(x1)))) -> x1 1064.60/297.06 , a56(a56(a56(a56(x1)))) -> x1 } 1064.60/297.06 Obligation: 1064.60/297.06 derivational complexity 1064.60/297.06 Answer: 1064.60/297.06 YES(O(1),O(n^6)) 1064.60/297.06 1064.60/297.06 We use the processor 'matrix interpretation of dimension 1' to 1064.60/297.06 orient following rules strictly. 1064.60/297.06 1064.60/297.06 Trs: 1064.60/297.06 { a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1)))))) 1064.60/297.06 , a13(a13(a13(a13(x1)))) -> x1 1064.60/297.06 , a14(a14(x1)) -> 1064.60/297.06 a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) 1064.60/297.06 , a14(a14(a14(a14(x1)))) -> x1 1064.60/297.06 , a15(a15(x1)) -> 1064.60/297.06 a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) 1064.60/297.06 , a15(a15(a15(a15(x1)))) -> x1 1064.60/297.06 , a16(a16(x1)) -> 1064.60/297.06 a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) 1064.60/297.06 , a16(a16(a16(a16(x1)))) -> x1 1064.60/297.06 , a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1)))))) 1064.60/297.06 , a24(a24(a24(a24(x1)))) -> x1 1064.60/297.06 , a25(a25(x1)) -> 1064.60/297.06 a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) 1064.60/297.06 , a25(a25(a25(a25(x1)))) -> x1 1064.60/297.06 , a26(a26(x1)) -> 1064.60/297.06 a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) 1064.60/297.06 , a26(a26(a26(a26(x1)))) -> x1 1064.60/297.06 , a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1)))))) 1064.60/297.06 , a35(a35(a35(a35(x1)))) -> x1 1064.60/297.06 , a36(a36(x1)) -> 1064.60/297.06 a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) 1064.60/297.06 , a36(a36(a36(a36(x1)))) -> x1 1064.60/297.06 , a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1)))))) 1064.60/297.06 , a46(a46(a46(a46(x1)))) -> x1 } 1064.60/297.06 1064.60/297.06 The induced complexity on above rules (modulo remaining rules) is 1064.60/297.06 YES(?,O(n^1)) . These rules are removed from the problem. Note that 1064.60/297.06 none of the weakly oriented rules is size-increasing. The overall 1064.60/297.06 complexity is obtained by composition . 1064.60/297.06 1064.60/297.06 Sub-proof: 1064.60/297.06 ---------- 1064.60/297.06 TcT has computed the following triangular matrix interpretation. 1064.60/297.06 1064.60/297.06 [a12](x1) = [1] x1 + [0] 1064.60/297.06 1064.60/297.06 [a13](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a14](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a15](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a16](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a23](x1) = [1] x1 + [0] 1064.60/297.06 1064.60/297.06 [a24](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a25](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a26](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a34](x1) = [1] x1 + [0] 1064.60/297.06 1064.60/297.06 [a35](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a36](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a45](x1) = [1] x1 + [0] 1064.60/297.06 1064.60/297.06 [a46](x1) = [1] x1 + [1] 1064.60/297.06 1064.60/297.06 [a56](x1) = [1] x1 + [0] 1064.60/297.06 1064.60/297.06 The order satisfies the following ordering constraints: 1064.60/297.06 1064.60/297.06 [a12(a12(a12(a12(x1))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1))))))))))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a12(a12(a34(a34(x1))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [a34(a34(a12(a12(x1))))] 1064.60/297.06 1064.60/297.06 [a12(a12(a45(a45(x1))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [a45(a45(a12(a12(x1))))] 1064.60/297.06 1064.60/297.06 [a12(a12(a56(a56(x1))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [a56(a56(a12(a12(x1))))] 1064.60/297.06 1064.60/297.06 [a13(a13(x1))] = [1] x1 + [2] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [a12(a12(a23(a23(a12(a12(x1))))))] 1064.60/297.06 1064.60/297.06 [a13(a13(a13(a13(x1))))] = [1] x1 + [4] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a14(a14(x1))] = [1] x1 + [2] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))))] 1064.60/297.06 1064.60/297.06 [a14(a14(a14(a14(x1))))] = [1] x1 + [4] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a15(a15(x1))] = [1] x1 + [2] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))] 1064.60/297.06 1064.60/297.06 [a15(a15(a15(a15(x1))))] = [1] x1 + [4] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a16(a16(x1))] = [1] x1 + [2] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))))] 1064.60/297.06 1064.60/297.06 [a16(a16(a16(a16(x1))))] = [1] x1 + [4] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a23(a23(a23(a23(x1))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1))))))))))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a23(a23(a45(a45(x1))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [a45(a45(a23(a23(x1))))] 1064.60/297.06 1064.60/297.06 [a23(a23(a56(a56(x1))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [a56(a56(a23(a23(x1))))] 1064.60/297.06 1064.60/297.06 [a24(a24(x1))] = [1] x1 + [2] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [a23(a23(a34(a34(a23(a23(x1))))))] 1064.60/297.06 1064.60/297.06 [a24(a24(a24(a24(x1))))] = [1] x1 + [4] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a25(a25(x1))] = [1] x1 + [2] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))))] 1064.60/297.06 1064.60/297.06 [a25(a25(a25(a25(x1))))] = [1] x1 + [4] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a26(a26(x1))] = [1] x1 + [2] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))))] 1064.60/297.06 1064.60/297.06 [a26(a26(a26(a26(x1))))] = [1] x1 + [4] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a34(a34(a34(a34(x1))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1))))))))))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a34(a34(a56(a56(x1))))] = [1] x1 + [0] 1064.60/297.06 >= [1] x1 + [0] 1064.60/297.06 = [a56(a56(a34(a34(x1))))] 1064.60/297.06 1064.60/297.06 [a35(a35(x1))] = [1] x1 + [2] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [a34(a34(a45(a45(a34(a34(x1))))))] 1064.60/297.06 1064.60/297.06 [a35(a35(a35(a35(x1))))] = [1] x1 + [4] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.06 1064.60/297.06 [a36(a36(x1))] = [1] x1 + [2] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))))] 1064.60/297.06 1064.60/297.06 [a36(a36(a36(a36(x1))))] = [1] x1 + [4] 1064.60/297.06 > [1] x1 + [0] 1064.60/297.06 = [x1] 1064.60/297.07 1064.60/297.07 [a45(a45(a45(a45(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1))))))))))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a46(a46(x1))] = [1] x1 + [2] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [a45(a45(a56(a56(a45(a45(x1))))))] 1064.60/297.07 1064.60/297.07 [a46(a46(a46(a46(x1))))] = [1] x1 + [4] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a56(a56(a56(a56(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 1064.60/297.07 We return to the main proof. 1064.60/297.07 1064.60/297.07 We are left with following problem, upon which TcT provides the 1064.60/297.07 certificate YES(O(1),O(n^5)). 1064.60/297.07 1064.60/297.07 Strict Trs: 1064.60/297.07 { a12(a12(a12(a12(x1)))) -> x1 1064.60/297.07 , a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> 1064.60/297.07 x1 1064.60/297.07 , a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) 1064.60/297.07 , a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) 1064.60/297.07 , a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) 1064.60/297.07 , a23(a23(a23(a23(x1)))) -> x1 1064.60/297.07 , a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> 1064.60/297.07 x1 1064.60/297.07 , a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) 1064.60/297.07 , a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) 1064.60/297.07 , a34(a34(a34(a34(x1)))) -> x1 1064.60/297.07 , a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> 1064.60/297.07 x1 1064.60/297.07 , a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) 1064.60/297.07 , a45(a45(a45(a45(x1)))) -> x1 1064.60/297.07 , a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> 1064.60/297.07 x1 1064.60/297.07 , a56(a56(a56(a56(x1)))) -> x1 } 1064.60/297.07 Obligation: 1064.60/297.07 derivational complexity 1064.60/297.07 Answer: 1064.60/297.07 YES(O(1),O(n^5)) 1064.60/297.07 1064.60/297.07 We use the processor 'matrix interpretation of dimension 1' to 1064.60/297.07 orient following rules strictly. 1064.60/297.07 1064.60/297.07 Trs: 1064.60/297.07 { a12(a12(a12(a12(x1)))) -> x1 1064.60/297.07 , a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) -> 1064.60/297.07 x1 1064.60/297.07 , a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) -> 1064.60/297.07 x1 1064.60/297.07 , a45(a45(a45(a45(x1)))) -> x1 1064.60/297.07 , a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) -> 1064.60/297.07 x1 } 1064.60/297.07 1064.60/297.07 The induced complexity on above rules (modulo remaining rules) is 1064.60/297.07 YES(?,O(n^1)) . These rules are removed from the problem. Note that 1064.60/297.07 no rule is size-increasing. The overall complexity is obtained by 1064.60/297.07 multiplication . 1064.60/297.07 1064.60/297.07 Sub-proof: 1064.60/297.07 ---------- 1064.60/297.07 TcT has computed the following triangular matrix interpretation. 1064.60/297.07 1064.60/297.07 [a12](x1) = [1] x1 + [1] 1064.60/297.07 1064.60/297.07 [a23](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 [a34](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 [a45](x1) = [1] x1 + [1] 1064.60/297.07 1064.60/297.07 [a56](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 The order satisfies the following ordering constraints: 1064.60/297.07 1064.60/297.07 [a12(a12(a12(a12(x1))))] = [1] x1 + [4] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1))))))))))))] = [1] x1 + [6] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a12(a12(a34(a34(x1))))] = [1] x1 + [2] 1064.60/297.07 >= [1] x1 + [2] 1064.60/297.07 = [a34(a34(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a12(a12(a45(a45(x1))))] = [1] x1 + [4] 1064.60/297.07 >= [1] x1 + [4] 1064.60/297.07 = [a45(a45(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a12(a12(a56(a56(x1))))] = [1] x1 + [2] 1064.60/297.07 >= [1] x1 + [2] 1064.60/297.07 = [a56(a56(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a23(a23(a23(a23(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1))))))))))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a23(a23(a45(a45(x1))))] = [1] x1 + [2] 1064.60/297.07 >= [1] x1 + [2] 1064.60/297.07 = [a45(a45(a23(a23(x1))))] 1064.60/297.07 1064.60/297.07 [a23(a23(a56(a56(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [a56(a56(a23(a23(x1))))] 1064.60/297.07 1064.60/297.07 [a34(a34(a34(a34(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1))))))))))))] = [1] x1 + [6] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a34(a34(a56(a56(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [a56(a56(a34(a34(x1))))] 1064.60/297.07 1064.60/297.07 [a45(a45(a45(a45(x1))))] = [1] x1 + [4] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1))))))))))))] = [1] x1 + [6] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a56(a56(a56(a56(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 1064.60/297.07 We return to the main proof. 1064.60/297.07 1064.60/297.07 We are left with following problem, upon which TcT provides the 1064.60/297.07 certificate YES(O(1),O(n^4)). 1064.60/297.07 1064.60/297.07 Strict Trs: 1064.60/297.07 { a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) 1064.60/297.07 , a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) 1064.60/297.07 , a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) 1064.60/297.07 , a23(a23(a23(a23(x1)))) -> x1 1064.60/297.07 , a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> 1064.60/297.07 x1 1064.60/297.07 , a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) 1064.60/297.07 , a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) 1064.60/297.07 , a34(a34(a34(a34(x1)))) -> x1 1064.60/297.07 , a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) 1064.60/297.07 , a56(a56(a56(a56(x1)))) -> x1 } 1064.60/297.07 Obligation: 1064.60/297.07 derivational complexity 1064.60/297.07 Answer: 1064.60/297.07 YES(O(1),O(n^4)) 1064.60/297.07 1064.60/297.07 We use the processor 'matrix interpretation of dimension 1' to 1064.60/297.07 orient following rules strictly. 1064.60/297.07 1064.60/297.07 Trs: 1064.60/297.07 { a23(a23(a23(a23(x1)))) -> x1 1064.60/297.07 , a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) -> 1064.60/297.07 x1 1064.60/297.07 , a56(a56(a56(a56(x1)))) -> x1 } 1064.60/297.07 1064.60/297.07 The induced complexity on above rules (modulo remaining rules) is 1064.60/297.07 YES(?,O(n^1)) . These rules are removed from the problem. Note that 1064.60/297.07 no rule is size-increasing. The overall complexity is obtained by 1064.60/297.07 multiplication . 1064.60/297.07 1064.60/297.07 Sub-proof: 1064.60/297.07 ---------- 1064.60/297.07 TcT has computed the following triangular matrix interpretation. 1064.60/297.07 1064.60/297.07 [a12](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 [a23](x1) = [1] x1 + [1] 1064.60/297.07 1064.60/297.07 [a34](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 [a45](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 [a56](x1) = [1] x1 + [1] 1064.60/297.07 1064.60/297.07 The order satisfies the following ordering constraints: 1064.60/297.07 1064.60/297.07 [a12(a12(a34(a34(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [a34(a34(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a12(a12(a45(a45(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [a45(a45(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a12(a12(a56(a56(x1))))] = [1] x1 + [2] 1064.60/297.07 >= [1] x1 + [2] 1064.60/297.07 = [a56(a56(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a23(a23(a23(a23(x1))))] = [1] x1 + [4] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1))))))))))))] = [1] x1 + [6] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a23(a23(a45(a45(x1))))] = [1] x1 + [2] 1064.60/297.07 >= [1] x1 + [2] 1064.60/297.07 = [a45(a45(a23(a23(x1))))] 1064.60/297.07 1064.60/297.07 [a23(a23(a56(a56(x1))))] = [1] x1 + [4] 1064.60/297.07 >= [1] x1 + [4] 1064.60/297.07 = [a56(a56(a23(a23(x1))))] 1064.60/297.07 1064.60/297.07 [a34(a34(a34(a34(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a34(a34(a56(a56(x1))))] = [1] x1 + [2] 1064.60/297.07 >= [1] x1 + [2] 1064.60/297.07 = [a56(a56(a34(a34(x1))))] 1064.60/297.07 1064.60/297.07 [a56(a56(a56(a56(x1))))] = [1] x1 + [4] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 1064.60/297.07 We return to the main proof. 1064.60/297.07 1064.60/297.07 We are left with following problem, upon which TcT provides the 1064.60/297.07 certificate YES(O(1),O(n^3)). 1064.60/297.07 1064.60/297.07 Strict Trs: 1064.60/297.07 { a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) 1064.60/297.07 , a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) 1064.60/297.07 , a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) 1064.60/297.07 , a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) 1064.60/297.07 , a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) 1064.60/297.07 , a34(a34(a34(a34(x1)))) -> x1 1064.60/297.07 , a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) } 1064.60/297.07 Obligation: 1064.60/297.07 derivational complexity 1064.60/297.07 Answer: 1064.60/297.07 YES(O(1),O(n^3)) 1064.60/297.07 1064.60/297.07 We use the processor 'matrix interpretation of dimension 1' to 1064.60/297.07 orient following rules strictly. 1064.60/297.07 1064.60/297.07 Trs: { a34(a34(a34(a34(x1)))) -> x1 } 1064.60/297.07 1064.60/297.07 The induced complexity on above rules (modulo remaining rules) is 1064.60/297.07 YES(?,O(n^1)) . These rules are removed from the problem. Note that 1064.60/297.07 no rule is size-increasing. The overall complexity is obtained by 1064.60/297.07 multiplication . 1064.60/297.07 1064.60/297.07 Sub-proof: 1064.60/297.07 ---------- 1064.60/297.07 TcT has computed the following triangular matrix interpretation. 1064.60/297.07 1064.60/297.07 [a12](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 [a23](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 [a34](x1) = [1] x1 + [1] 1064.60/297.07 1064.60/297.07 [a45](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 [a56](x1) = [1] x1 + [0] 1064.60/297.07 1064.60/297.07 The order satisfies the following ordering constraints: 1064.60/297.07 1064.60/297.07 [a12(a12(a34(a34(x1))))] = [1] x1 + [2] 1064.60/297.07 >= [1] x1 + [2] 1064.60/297.07 = [a34(a34(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a12(a12(a45(a45(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [a45(a45(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a12(a12(a56(a56(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [a56(a56(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a23(a23(a45(a45(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [a45(a45(a23(a23(x1))))] 1064.60/297.07 1064.60/297.07 [a23(a23(a56(a56(x1))))] = [1] x1 + [0] 1064.60/297.07 >= [1] x1 + [0] 1064.60/297.07 = [a56(a56(a23(a23(x1))))] 1064.60/297.07 1064.60/297.07 [a34(a34(a34(a34(x1))))] = [1] x1 + [4] 1064.60/297.07 > [1] x1 + [0] 1064.60/297.07 = [x1] 1064.60/297.07 1064.60/297.07 [a34(a34(a56(a56(x1))))] = [1] x1 + [2] 1064.60/297.07 >= [1] x1 + [2] 1064.60/297.07 = [a56(a56(a34(a34(x1))))] 1064.60/297.07 1064.60/297.07 1064.60/297.07 We return to the main proof. 1064.60/297.07 1064.60/297.07 We are left with following problem, upon which TcT provides the 1064.60/297.07 certificate YES(?,O(n^2)). 1064.60/297.07 1064.60/297.07 Strict Trs: 1064.60/297.07 { a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1)))) 1064.60/297.07 , a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1)))) 1064.60/297.07 , a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1)))) 1064.60/297.07 , a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1)))) 1064.60/297.07 , a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1)))) 1064.60/297.07 , a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1)))) } 1064.60/297.07 Obligation: 1064.60/297.07 derivational complexity 1064.60/297.07 Answer: 1064.60/297.07 YES(?,O(n^2)) 1064.60/297.07 1064.60/297.07 TcT has computed the following triangular matrix interpretation. 1064.60/297.07 1064.60/297.07 [a12](x1) = [1 1] x1 + [0] 1064.60/297.07 [0 1] [0] 1064.60/297.07 1064.60/297.07 [a23](x1) = [1 1] x1 + [0] 1064.60/297.07 [0 1] [0] 1064.60/297.07 1064.60/297.07 [a34](x1) = [1 2] x1 + [0] 1064.60/297.07 [0 1] [1] 1064.60/297.07 1064.60/297.07 [a45](x1) = [1 0] x1 + [0] 1064.60/297.07 [0 1] [2] 1064.60/297.07 1064.60/297.07 [a56](x1) = [1 1] x1 + [0] 1064.60/297.07 [0 1] [1] 1064.60/297.07 1064.60/297.07 The order satisfies the following ordering constraints: 1064.60/297.07 1064.60/297.07 [a12(a12(a34(a34(x1))))] = [1 6] x1 + [6] 1064.60/297.07 [0 1] [2] 1064.60/297.07 > [1 6] x1 + [2] 1064.60/297.07 [0 1] [2] 1064.60/297.07 = [a34(a34(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a12(a12(a45(a45(x1))))] = [1 2] x1 + [8] 1064.60/297.07 [0 1] [4] 1064.60/297.07 > [1 2] x1 + [0] 1064.60/297.07 [0 1] [4] 1064.60/297.07 = [a45(a45(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a12(a12(a56(a56(x1))))] = [1 4] x1 + [5] 1064.60/297.07 [0 1] [2] 1064.60/297.07 > [1 4] x1 + [1] 1064.60/297.07 [0 1] [2] 1064.60/297.07 = [a56(a56(a12(a12(x1))))] 1064.60/297.07 1064.60/297.07 [a23(a23(a45(a45(x1))))] = [1 2] x1 + [8] 1064.60/297.07 [0 1] [4] 1064.60/297.07 > [1 2] x1 + [0] 1064.60/297.07 [0 1] [4] 1064.60/297.07 = [a45(a45(a23(a23(x1))))] 1064.60/297.07 1064.60/297.07 [a23(a23(a56(a56(x1))))] = [1 4] x1 + [5] 1064.60/297.07 [0 1] [2] 1064.60/297.07 > [1 4] x1 + [1] 1064.60/297.07 [0 1] [2] 1064.60/297.07 = [a56(a56(a23(a23(x1))))] 1064.60/297.07 1064.60/297.07 [a34(a34(a56(a56(x1))))] = [1 6] x1 + [11] 1064.60/297.07 [0 1] [4] 1064.60/297.07 > [1 6] x1 + [7] 1064.60/297.07 [0 1] [4] 1064.60/297.07 = [a56(a56(a34(a34(x1))))] 1064.60/297.07 1064.60/297.07 1064.60/297.07 Hurray, we answered YES(O(1),O(n^6)) 1065.24/297.59 EOF