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