YES(O(1),O(n^2)) 172.13/60.06 YES(O(1),O(n^2)) 172.13/60.06 172.13/60.06 We are left with following problem, upon which TcT provides the 172.13/60.06 certificate YES(O(1),O(n^2)). 172.13/60.06 172.13/60.06 Strict Trs: 172.13/60.06 { a(a(x1)) -> b(b(b(x1))) 172.13/60.06 , b(x1) -> c(c(d(x1))) 172.13/60.06 , b(c(x1)) -> c(b(x1)) 172.13/60.06 , b(c(d(x1))) -> a(x1) 172.13/60.06 , c(x1) -> d(d(d(x1))) } 172.13/60.06 Obligation: 172.13/60.06 derivational complexity 172.13/60.06 Answer: 172.13/60.06 YES(O(1),O(n^2)) 172.13/60.06 172.13/60.06 The weightgap principle applies (using the following nonconstant 172.13/60.06 growth matrix-interpretation) 172.13/60.06 172.13/60.06 TcT has computed the following triangular matrix interpretation. 172.13/60.06 Note that the diagonal of the component-wise maxima of 172.13/60.06 interpretation-entries contains no more than 1 non-zero entries. 172.13/60.06 172.13/60.06 [a](x1) = [1] x1 + [2] 172.13/60.06 172.13/60.06 [b](x1) = [1] x1 + [1] 172.13/60.06 172.13/60.06 [c](x1) = [1] x1 + [1] 172.13/60.06 172.13/60.06 [d](x1) = [1] x1 + [2] 172.13/60.06 172.13/60.06 The order satisfies the following ordering constraints: 172.13/60.06 172.13/60.06 [a(a(x1))] = [1] x1 + [4] 172.13/60.06 > [1] x1 + [3] 172.13/60.06 = [b(b(b(x1)))] 172.13/60.06 172.13/60.06 [b(x1)] = [1] x1 + [1] 172.13/60.06 ? [1] x1 + [4] 172.13/60.06 = [c(c(d(x1)))] 172.13/60.06 172.13/60.06 [b(c(x1))] = [1] x1 + [2] 172.13/60.06 >= [1] x1 + [2] 172.13/60.06 = [c(b(x1))] 172.13/60.06 172.13/60.06 [b(c(d(x1)))] = [1] x1 + [4] 172.13/60.06 > [1] x1 + [2] 172.13/60.06 = [a(x1)] 172.13/60.06 172.13/60.06 [c(x1)] = [1] x1 + [1] 172.13/60.06 ? [1] x1 + [6] 172.13/60.06 = [d(d(d(x1)))] 172.13/60.06 172.13/60.06 172.13/60.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 172.13/60.06 172.13/60.06 We are left with following problem, upon which TcT provides the 172.13/60.06 certificate YES(O(1),O(n^2)). 172.13/60.06 172.13/60.06 Strict Trs: 172.13/60.06 { b(x1) -> c(c(d(x1))) 172.13/60.06 , b(c(x1)) -> c(b(x1)) 172.13/60.06 , c(x1) -> d(d(d(x1))) } 172.13/60.06 Weak Trs: 172.13/60.06 { a(a(x1)) -> b(b(b(x1))) 172.13/60.06 , b(c(d(x1))) -> a(x1) } 172.13/60.06 Obligation: 172.13/60.06 derivational complexity 172.13/60.06 Answer: 172.13/60.06 YES(O(1),O(n^2)) 172.13/60.06 172.13/60.06 The weightgap principle applies (using the following nonconstant 172.13/60.06 growth matrix-interpretation) 172.13/60.06 172.13/60.06 TcT has computed the following triangular matrix interpretation. 172.13/60.06 Note that the diagonal of the component-wise maxima of 172.13/60.06 interpretation-entries contains no more than 1 non-zero entries. 172.13/60.06 172.13/60.06 [a](x1) = [1] x1 + [2] 172.13/60.06 172.13/60.06 [b](x1) = [1] x1 + [0] 172.13/60.06 172.13/60.06 [c](x1) = [1] x1 + [2] 172.13/60.06 172.13/60.06 [d](x1) = [1] x1 + [0] 172.13/60.06 172.13/60.06 The order satisfies the following ordering constraints: 172.13/60.06 172.13/60.06 [a(a(x1))] = [1] x1 + [4] 172.13/60.06 > [1] x1 + [0] 172.13/60.06 = [b(b(b(x1)))] 172.13/60.06 172.13/60.06 [b(x1)] = [1] x1 + [0] 172.13/60.06 ? [1] x1 + [4] 172.13/60.06 = [c(c(d(x1)))] 172.13/60.06 172.13/60.06 [b(c(x1))] = [1] x1 + [2] 172.13/60.06 >= [1] x1 + [2] 172.13/60.06 = [c(b(x1))] 172.13/60.06 172.13/60.06 [b(c(d(x1)))] = [1] x1 + [2] 172.13/60.06 >= [1] x1 + [2] 172.13/60.06 = [a(x1)] 172.13/60.06 172.13/60.06 [c(x1)] = [1] x1 + [2] 172.13/60.06 > [1] x1 + [0] 172.13/60.06 = [d(d(d(x1)))] 172.13/60.06 172.13/60.06 172.13/60.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 172.13/60.06 172.13/60.06 We are left with following problem, upon which TcT provides the 172.13/60.06 certificate YES(O(1),O(n^2)). 172.13/60.06 172.13/60.06 Strict Trs: 172.13/60.06 { b(x1) -> c(c(d(x1))) 172.13/60.06 , b(c(x1)) -> c(b(x1)) } 172.13/60.06 Weak Trs: 172.13/60.06 { a(a(x1)) -> b(b(b(x1))) 172.13/60.06 , b(c(d(x1))) -> a(x1) 172.13/60.06 , c(x1) -> d(d(d(x1))) } 172.13/60.06 Obligation: 172.13/60.06 derivational complexity 172.13/60.06 Answer: 172.13/60.06 YES(O(1),O(n^2)) 172.13/60.06 172.13/60.06 We use the processor 'matrix interpretation of dimension 1' to 172.13/60.06 orient following rules strictly. 172.13/60.06 172.13/60.06 Trs: { b(x1) -> c(c(d(x1))) } 172.13/60.06 172.13/60.06 The induced complexity on above rules (modulo remaining rules) is 172.13/60.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 172.13/60.06 component(s). 172.13/60.06 172.13/60.06 Sub-proof: 172.13/60.06 ---------- 172.13/60.06 TcT has computed the following triangular matrix interpretation. 172.13/60.06 172.13/60.06 [a](x1) = [1] x1 + [48] 172.13/60.06 172.13/60.06 [b](x1) = [1] x1 + [32] 172.13/60.06 172.13/60.06 [c](x1) = [1] x1 + [12] 172.13/60.06 172.13/60.06 [d](x1) = [1] x1 + [4] 172.13/60.06 172.13/60.06 The order satisfies the following ordering constraints: 172.13/60.06 172.13/60.06 [a(a(x1))] = [1] x1 + [96] 172.13/60.06 >= [1] x1 + [96] 172.13/60.06 = [b(b(b(x1)))] 172.13/60.06 172.13/60.06 [b(x1)] = [1] x1 + [32] 172.13/60.06 > [1] x1 + [28] 172.13/60.06 = [c(c(d(x1)))] 172.13/60.06 172.13/60.06 [b(c(x1))] = [1] x1 + [44] 172.13/60.06 >= [1] x1 + [44] 172.13/60.06 = [c(b(x1))] 172.13/60.06 172.13/60.06 [b(c(d(x1)))] = [1] x1 + [48] 172.13/60.06 >= [1] x1 + [48] 172.13/60.06 = [a(x1)] 172.13/60.06 172.13/60.06 [c(x1)] = [1] x1 + [12] 172.13/60.06 >= [1] x1 + [12] 172.13/60.06 = [d(d(d(x1)))] 172.13/60.06 172.13/60.06 172.13/60.06 We return to the main proof. 172.13/60.06 172.13/60.06 We are left with following problem, upon which TcT provides the 172.13/60.06 certificate YES(O(1),O(n^2)). 172.13/60.06 172.13/60.06 Strict Trs: { b(c(x1)) -> c(b(x1)) } 172.13/60.06 Weak Trs: 172.13/60.06 { a(a(x1)) -> b(b(b(x1))) 172.13/60.06 , b(x1) -> c(c(d(x1))) 172.13/60.06 , b(c(d(x1))) -> a(x1) 172.13/60.06 , c(x1) -> d(d(d(x1))) } 172.13/60.06 Obligation: 172.13/60.06 derivational complexity 172.13/60.06 Answer: 172.13/60.06 YES(O(1),O(n^2)) 172.13/60.06 172.13/60.06 We use the processor 'matrix interpretation of dimension 2' to 172.13/60.06 orient following rules strictly. 172.13/60.06 172.13/60.06 Trs: { b(c(x1)) -> c(b(x1)) } 172.13/60.06 172.13/60.06 The induced complexity on above rules (modulo remaining rules) is 172.13/60.06 YES(?,O(n^2)) . These rules are moved into the corresponding weak 172.13/60.06 component(s). 172.13/60.06 172.13/60.06 Sub-proof: 172.13/60.06 ---------- 172.13/60.06 TcT has computed the following triangular matrix interpretation. 172.13/60.06 172.13/60.06 [a](x1) = [1 11] x1 + [11] 172.13/60.06 [0 1] [3] 172.13/60.06 172.13/60.06 [b](x1) = [1 7] x1 + [4] 172.13/60.06 [0 1] [2] 172.13/60.06 172.13/60.06 [c](x1) = [1 3] x1 + [0] 172.13/60.06 [0 1] [1] 172.13/60.06 172.13/60.06 [d](x1) = [1 1] x1 + [0] 172.13/60.06 [0 1] [0] 172.13/60.06 172.13/60.06 The order satisfies the following ordering constraints: 172.13/60.06 172.13/60.06 [a(a(x1))] = [1 22] x1 + [55] 172.13/60.06 [0 1] [6] 172.13/60.06 > [1 21] x1 + [54] 172.13/60.06 [0 1] [6] 172.13/60.06 = [b(b(b(x1)))] 172.13/60.06 172.13/60.06 [b(x1)] = [1 7] x1 + [4] 172.13/60.06 [0 1] [2] 172.13/60.06 > [1 7] x1 + [3] 172.13/60.06 [0 1] [2] 172.13/60.06 = [c(c(d(x1)))] 172.13/60.06 172.13/60.06 [b(c(x1))] = [1 10] x1 + [11] 172.13/60.06 [0 1] [3] 172.13/60.06 > [1 10] x1 + [10] 172.13/60.06 [0 1] [3] 172.13/60.06 = [c(b(x1))] 172.13/60.06 172.13/60.06 [b(c(d(x1)))] = [1 11] x1 + [11] 172.13/60.06 [0 1] [3] 172.13/60.06 >= [1 11] x1 + [11] 172.13/60.06 [0 1] [3] 172.13/60.06 = [a(x1)] 172.13/60.06 172.13/60.06 [c(x1)] = [1 3] x1 + [0] 172.13/60.06 [0 1] [1] 172.13/60.06 >= [1 3] x1 + [0] 172.13/60.06 [0 1] [0] 172.13/60.06 = [d(d(d(x1)))] 172.13/60.06 172.13/60.06 172.13/60.06 We return to the main proof. 172.13/60.06 172.13/60.06 We are left with following problem, upon which TcT provides the 172.13/60.06 certificate YES(O(1),O(1)). 172.13/60.06 172.13/60.06 Weak Trs: 172.13/60.06 { a(a(x1)) -> b(b(b(x1))) 172.13/60.06 , b(x1) -> c(c(d(x1))) 172.13/60.06 , b(c(x1)) -> c(b(x1)) 172.13/60.06 , b(c(d(x1))) -> a(x1) 172.13/60.06 , c(x1) -> d(d(d(x1))) } 172.13/60.06 Obligation: 172.13/60.06 derivational complexity 172.13/60.06 Answer: 172.13/60.06 YES(O(1),O(1)) 172.13/60.06 172.13/60.06 Empty rules are trivially bounded 172.13/60.06 172.13/60.06 Hurray, we answered YES(O(1),O(n^2)) 172.13/60.08 EOF