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