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