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