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