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