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