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