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