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