YES(O(1),O(n^2)) 189.39/60.87 YES(O(1),O(n^2)) 189.39/60.87 189.39/60.87 We are left with following problem, upon which TcT provides the 189.39/60.87 certificate YES(O(1),O(n^2)). 189.39/60.87 189.39/60.87 Strict Trs: 189.39/60.87 { active(f(X)) -> f(active(X)) 189.39/60.87 , active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.87 , active(c(X)) -> mark(d(X)) 189.39/60.87 , active(h(X)) -> mark(c(d(X))) 189.39/60.87 , active(h(X)) -> h(active(X)) 189.39/60.87 , f(mark(X)) -> mark(f(X)) 189.39/60.87 , f(ok(X)) -> ok(f(X)) 189.39/60.87 , c(ok(X)) -> ok(c(X)) 189.39/60.87 , g(ok(X)) -> ok(g(X)) 189.39/60.87 , d(ok(X)) -> ok(d(X)) 189.39/60.87 , h(mark(X)) -> mark(h(X)) 189.39/60.87 , h(ok(X)) -> ok(h(X)) 189.39/60.87 , proper(f(X)) -> f(proper(X)) 189.39/60.87 , proper(c(X)) -> c(proper(X)) 189.39/60.87 , proper(g(X)) -> g(proper(X)) 189.39/60.87 , proper(d(X)) -> d(proper(X)) 189.39/60.87 , proper(h(X)) -> h(proper(X)) 189.39/60.87 , top(mark(X)) -> top(proper(X)) 189.39/60.87 , top(ok(X)) -> top(active(X)) } 189.39/60.87 Obligation: 189.39/60.87 derivational complexity 189.39/60.87 Answer: 189.39/60.87 YES(O(1),O(n^2)) 189.39/60.87 189.39/60.87 We use the processor 'matrix interpretation of dimension 1' to 189.39/60.87 orient following rules strictly. 189.39/60.87 189.39/60.87 Trs: 189.39/60.87 { active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.87 , active(c(X)) -> mark(d(X)) 189.39/60.87 , active(h(X)) -> mark(c(d(X))) } 189.39/60.87 189.39/60.87 The induced complexity on above rules (modulo remaining rules) is 189.39/60.87 YES(?,O(n^1)) . These rules are moved into the corresponding weak 189.39/60.87 component(s). 189.39/60.87 189.39/60.87 Sub-proof: 189.39/60.87 ---------- 189.39/60.87 TcT has computed the following triangular matrix interpretation. 189.39/60.87 189.39/60.87 [active](x1) = [1] x1 + [1] 189.39/60.87 189.39/60.87 [f](x1) = [1] x1 + [0] 189.39/60.87 189.39/60.87 [mark](x1) = [1] x1 + [0] 189.39/60.87 189.39/60.87 [c](x1) = [1] x1 + [0] 189.39/60.87 189.39/60.87 [g](x1) = [1] x1 + [0] 189.39/60.87 189.39/60.87 [d](x1) = [1] x1 + [0] 189.39/60.87 189.39/60.87 [h](x1) = [1] x1 + [0] 189.39/60.87 189.39/60.87 [proper](x1) = [1] x1 + [0] 189.39/60.87 189.39/60.87 [ok](x1) = [1] x1 + [1] 189.39/60.87 189.39/60.87 [top](x1) = [1] x1 + [0] 189.39/60.87 189.39/60.87 The order satisfies the following ordering constraints: 189.39/60.87 189.39/60.87 [active(f(X))] = [1] X + [1] 189.39/60.87 >= [1] X + [1] 189.39/60.87 = [f(active(X))] 189.39/60.88 189.39/60.88 [active(f(f(X)))] = [1] X + [1] 189.39/60.88 > [1] X + [0] 189.39/60.88 = [mark(c(f(g(f(X)))))] 189.39/60.88 189.39/60.88 [active(c(X))] = [1] X + [1] 189.39/60.88 > [1] X + [0] 189.39/60.88 = [mark(d(X))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1] X + [1] 189.39/60.88 > [1] X + [0] 189.39/60.88 = [mark(c(d(X)))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [h(active(X))] 189.39/60.88 189.39/60.88 [f(mark(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [mark(f(X))] 189.39/60.88 189.39/60.88 [f(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(f(X))] 189.39/60.88 189.39/60.88 [c(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(c(X))] 189.39/60.88 189.39/60.88 [g(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(g(X))] 189.39/60.88 189.39/60.88 [d(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(d(X))] 189.39/60.88 189.39/60.88 [h(mark(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [mark(h(X))] 189.39/60.88 189.39/60.88 [h(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(h(X))] 189.39/60.88 189.39/60.88 [proper(f(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [f(proper(X))] 189.39/60.88 189.39/60.88 [proper(c(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [c(proper(X))] 189.39/60.88 189.39/60.88 [proper(g(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [g(proper(X))] 189.39/60.88 189.39/60.88 [proper(d(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [d(proper(X))] 189.39/60.88 189.39/60.88 [proper(h(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [h(proper(X))] 189.39/60.88 189.39/60.88 [top(mark(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [top(proper(X))] 189.39/60.88 189.39/60.88 [top(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [top(active(X))] 189.39/60.88 189.39/60.88 189.39/60.88 We return to the main proof. 189.39/60.88 189.39/60.88 We are left with following problem, upon which TcT provides the 189.39/60.88 certificate YES(O(1),O(n^2)). 189.39/60.88 189.39/60.88 Strict Trs: 189.39/60.88 { active(f(X)) -> f(active(X)) 189.39/60.88 , active(h(X)) -> h(active(X)) 189.39/60.88 , f(mark(X)) -> mark(f(X)) 189.39/60.88 , f(ok(X)) -> ok(f(X)) 189.39/60.88 , c(ok(X)) -> ok(c(X)) 189.39/60.88 , g(ok(X)) -> ok(g(X)) 189.39/60.88 , d(ok(X)) -> ok(d(X)) 189.39/60.88 , h(mark(X)) -> mark(h(X)) 189.39/60.88 , h(ok(X)) -> ok(h(X)) 189.39/60.88 , proper(f(X)) -> f(proper(X)) 189.39/60.88 , proper(c(X)) -> c(proper(X)) 189.39/60.88 , proper(g(X)) -> g(proper(X)) 189.39/60.88 , proper(d(X)) -> d(proper(X)) 189.39/60.88 , proper(h(X)) -> h(proper(X)) 189.39/60.88 , top(mark(X)) -> top(proper(X)) 189.39/60.88 , top(ok(X)) -> top(active(X)) } 189.39/60.88 Weak Trs: 189.39/60.88 { active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.88 , active(c(X)) -> mark(d(X)) 189.39/60.88 , active(h(X)) -> mark(c(d(X))) } 189.39/60.88 Obligation: 189.39/60.88 derivational complexity 189.39/60.88 Answer: 189.39/60.88 YES(O(1),O(n^2)) 189.39/60.88 189.39/60.88 We use the processor 'matrix interpretation of dimension 1' to 189.39/60.88 orient following rules strictly. 189.39/60.88 189.39/60.88 Trs: { top(ok(X)) -> top(active(X)) } 189.39/60.88 189.39/60.88 The induced complexity on above rules (modulo remaining rules) is 189.39/60.88 YES(?,O(n^1)) . These rules are moved into the corresponding weak 189.39/60.88 component(s). 189.39/60.88 189.39/60.88 Sub-proof: 189.39/60.88 ---------- 189.39/60.88 TcT has computed the following triangular matrix interpretation. 189.39/60.88 189.39/60.88 [active](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [f](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [mark](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [c](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [g](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [d](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [h](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [proper](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [ok](x1) = [1] x1 + [1] 189.39/60.88 189.39/60.88 [top](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 The order satisfies the following ordering constraints: 189.39/60.88 189.39/60.88 [active(f(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [f(active(X))] 189.39/60.88 189.39/60.88 [active(f(f(X)))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [mark(c(f(g(f(X)))))] 189.39/60.88 189.39/60.88 [active(c(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [mark(d(X))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [mark(c(d(X)))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [h(active(X))] 189.39/60.88 189.39/60.88 [f(mark(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [mark(f(X))] 189.39/60.88 189.39/60.88 [f(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(f(X))] 189.39/60.88 189.39/60.88 [c(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(c(X))] 189.39/60.88 189.39/60.88 [g(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(g(X))] 189.39/60.88 189.39/60.88 [d(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(d(X))] 189.39/60.88 189.39/60.88 [h(mark(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [mark(h(X))] 189.39/60.88 189.39/60.88 [h(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(h(X))] 189.39/60.88 189.39/60.88 [proper(f(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [f(proper(X))] 189.39/60.88 189.39/60.88 [proper(c(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [c(proper(X))] 189.39/60.88 189.39/60.88 [proper(g(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [g(proper(X))] 189.39/60.88 189.39/60.88 [proper(d(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [d(proper(X))] 189.39/60.88 189.39/60.88 [proper(h(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [h(proper(X))] 189.39/60.88 189.39/60.88 [top(mark(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [top(proper(X))] 189.39/60.88 189.39/60.88 [top(ok(X))] = [1] X + [1] 189.39/60.88 > [1] X + [0] 189.39/60.88 = [top(active(X))] 189.39/60.88 189.39/60.88 189.39/60.88 We return to the main proof. 189.39/60.88 189.39/60.88 We are left with following problem, upon which TcT provides the 189.39/60.88 certificate YES(O(1),O(n^2)). 189.39/60.88 189.39/60.88 Strict Trs: 189.39/60.88 { active(f(X)) -> f(active(X)) 189.39/60.88 , active(h(X)) -> h(active(X)) 189.39/60.88 , f(mark(X)) -> mark(f(X)) 189.39/60.88 , f(ok(X)) -> ok(f(X)) 189.39/60.88 , c(ok(X)) -> ok(c(X)) 189.39/60.88 , g(ok(X)) -> ok(g(X)) 189.39/60.88 , d(ok(X)) -> ok(d(X)) 189.39/60.88 , h(mark(X)) -> mark(h(X)) 189.39/60.88 , h(ok(X)) -> ok(h(X)) 189.39/60.88 , proper(f(X)) -> f(proper(X)) 189.39/60.88 , proper(c(X)) -> c(proper(X)) 189.39/60.88 , proper(g(X)) -> g(proper(X)) 189.39/60.88 , proper(d(X)) -> d(proper(X)) 189.39/60.88 , proper(h(X)) -> h(proper(X)) 189.39/60.88 , top(mark(X)) -> top(proper(X)) } 189.39/60.88 Weak Trs: 189.39/60.88 { active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.88 , active(c(X)) -> mark(d(X)) 189.39/60.88 , active(h(X)) -> mark(c(d(X))) 189.39/60.88 , top(ok(X)) -> top(active(X)) } 189.39/60.88 Obligation: 189.39/60.88 derivational complexity 189.39/60.88 Answer: 189.39/60.88 YES(O(1),O(n^2)) 189.39/60.88 189.39/60.88 We use the processor 'matrix interpretation of dimension 1' to 189.39/60.88 orient following rules strictly. 189.39/60.88 189.39/60.88 Trs: { top(mark(X)) -> top(proper(X)) } 189.39/60.88 189.39/60.88 The induced complexity on above rules (modulo remaining rules) is 189.39/60.88 YES(?,O(n^1)) . These rules are moved into the corresponding weak 189.39/60.88 component(s). 189.39/60.88 189.39/60.88 Sub-proof: 189.39/60.88 ---------- 189.39/60.88 TcT has computed the following triangular matrix interpretation. 189.39/60.88 189.39/60.88 [active](x1) = [1] x1 + [1] 189.39/60.88 189.39/60.88 [f](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [mark](x1) = [1] x1 + [1] 189.39/60.88 189.39/60.88 [c](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [g](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [d](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [h](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [proper](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 [ok](x1) = [1] x1 + [1] 189.39/60.88 189.39/60.88 [top](x1) = [1] x1 + [0] 189.39/60.88 189.39/60.88 The order satisfies the following ordering constraints: 189.39/60.88 189.39/60.88 [active(f(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [f(active(X))] 189.39/60.88 189.39/60.88 [active(f(f(X)))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [mark(c(f(g(f(X)))))] 189.39/60.88 189.39/60.88 [active(c(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [mark(d(X))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [mark(c(d(X)))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [h(active(X))] 189.39/60.88 189.39/60.88 [f(mark(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [mark(f(X))] 189.39/60.88 189.39/60.88 [f(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(f(X))] 189.39/60.88 189.39/60.88 [c(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(c(X))] 189.39/60.88 189.39/60.88 [g(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(g(X))] 189.39/60.88 189.39/60.88 [d(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(d(X))] 189.39/60.88 189.39/60.88 [h(mark(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [mark(h(X))] 189.39/60.88 189.39/60.88 [h(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [ok(h(X))] 189.39/60.88 189.39/60.88 [proper(f(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [f(proper(X))] 189.39/60.88 189.39/60.88 [proper(c(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [c(proper(X))] 189.39/60.88 189.39/60.88 [proper(g(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [g(proper(X))] 189.39/60.88 189.39/60.88 [proper(d(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [d(proper(X))] 189.39/60.88 189.39/60.88 [proper(h(X))] = [1] X + [0] 189.39/60.88 >= [1] X + [0] 189.39/60.88 = [h(proper(X))] 189.39/60.88 189.39/60.88 [top(mark(X))] = [1] X + [1] 189.39/60.88 > [1] X + [0] 189.39/60.88 = [top(proper(X))] 189.39/60.88 189.39/60.88 [top(ok(X))] = [1] X + [1] 189.39/60.88 >= [1] X + [1] 189.39/60.88 = [top(active(X))] 189.39/60.88 189.39/60.88 189.39/60.88 We return to the main proof. 189.39/60.88 189.39/60.88 We are left with following problem, upon which TcT provides the 189.39/60.88 certificate YES(O(1),O(n^2)). 189.39/60.88 189.39/60.88 Strict Trs: 189.39/60.88 { active(f(X)) -> f(active(X)) 189.39/60.88 , active(h(X)) -> h(active(X)) 189.39/60.88 , f(mark(X)) -> mark(f(X)) 189.39/60.88 , f(ok(X)) -> ok(f(X)) 189.39/60.88 , c(ok(X)) -> ok(c(X)) 189.39/60.88 , g(ok(X)) -> ok(g(X)) 189.39/60.88 , d(ok(X)) -> ok(d(X)) 189.39/60.88 , h(mark(X)) -> mark(h(X)) 189.39/60.88 , h(ok(X)) -> ok(h(X)) 189.39/60.88 , proper(f(X)) -> f(proper(X)) 189.39/60.88 , proper(c(X)) -> c(proper(X)) 189.39/60.88 , proper(g(X)) -> g(proper(X)) 189.39/60.88 , proper(d(X)) -> d(proper(X)) 189.39/60.88 , proper(h(X)) -> h(proper(X)) } 189.39/60.88 Weak Trs: 189.39/60.88 { active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.88 , active(c(X)) -> mark(d(X)) 189.39/60.88 , active(h(X)) -> mark(c(d(X))) 189.39/60.88 , top(mark(X)) -> top(proper(X)) 189.39/60.88 , top(ok(X)) -> top(active(X)) } 189.39/60.88 Obligation: 189.39/60.88 derivational complexity 189.39/60.88 Answer: 189.39/60.88 YES(O(1),O(n^2)) 189.39/60.88 189.39/60.88 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.88 orient following rules strictly. 189.39/60.88 189.39/60.88 Trs: 189.39/60.88 { c(ok(X)) -> ok(c(X)) 189.39/60.88 , d(ok(X)) -> ok(d(X)) 189.39/60.88 , h(ok(X)) -> ok(h(X)) } 189.39/60.88 189.39/60.88 The induced complexity on above rules (modulo remaining rules) is 189.39/60.88 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.88 component(s). 189.39/60.88 189.39/60.88 Sub-proof: 189.39/60.88 ---------- 189.39/60.88 TcT has computed the following triangular matrix interpretation. 189.39/60.88 189.39/60.88 [active](x1) = [1 2] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [f](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [mark](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [c](x1) = [1 2] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [g](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [d](x1) = [1 2] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [h](x1) = [1 2] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [proper](x1) = [1 0] x1 + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 189.39/60.88 [ok](x1) = [1 2] x1 + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 189.39/60.88 [top](x1) = [1 2] x1 + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 189.39/60.88 The order satisfies the following ordering constraints: 189.39/60.88 189.39/60.88 [active(f(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [f(active(X))] 189.39/60.88 189.39/60.88 [active(f(f(X)))] = [1 2] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(c(f(g(f(X)))))] 189.39/60.88 189.39/60.88 [active(c(X))] = [1 4] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(d(X))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1 4] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 4] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(c(d(X)))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1 4] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 4] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [h(active(X))] 189.39/60.88 189.39/60.88 [f(mark(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(f(X))] 189.39/60.88 189.39/60.88 [f(ok(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(f(X))] 189.39/60.88 189.39/60.88 [c(ok(X))] = [1 4] X + [4] 189.39/60.88 [0 1] [2] 189.39/60.88 > [1 4] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(c(X))] 189.39/60.88 189.39/60.88 [g(ok(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(g(X))] 189.39/60.88 189.39/60.88 [d(ok(X))] = [1 4] X + [4] 189.39/60.88 [0 1] [2] 189.39/60.88 > [1 4] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(d(X))] 189.39/60.88 189.39/60.88 [h(mark(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(h(X))] 189.39/60.88 189.39/60.88 [h(ok(X))] = [1 4] X + [4] 189.39/60.88 [0 1] [2] 189.39/60.88 > [1 4] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(h(X))] 189.39/60.88 189.39/60.88 [proper(f(X))] = [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [f(proper(X))] 189.39/60.88 189.39/60.88 [proper(c(X))] = [1 2] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [c(proper(X))] 189.39/60.88 189.39/60.88 [proper(g(X))] = [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [g(proper(X))] 189.39/60.88 189.39/60.88 [proper(d(X))] = [1 2] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [d(proper(X))] 189.39/60.88 189.39/60.88 [proper(h(X))] = [1 2] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [h(proper(X))] 189.39/60.88 189.39/60.88 [top(mark(X))] = [1 2] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [top(proper(X))] 189.39/60.88 189.39/60.88 [top(ok(X))] = [1 4] X + [4] 189.39/60.88 [0 0] [0] 189.39/60.88 > [1 4] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [top(active(X))] 189.39/60.88 189.39/60.88 189.39/60.88 We return to the main proof. 189.39/60.88 189.39/60.88 We are left with following problem, upon which TcT provides the 189.39/60.88 certificate YES(O(1),O(n^2)). 189.39/60.88 189.39/60.88 Strict Trs: 189.39/60.88 { active(f(X)) -> f(active(X)) 189.39/60.88 , active(h(X)) -> h(active(X)) 189.39/60.88 , f(mark(X)) -> mark(f(X)) 189.39/60.88 , f(ok(X)) -> ok(f(X)) 189.39/60.88 , g(ok(X)) -> ok(g(X)) 189.39/60.88 , h(mark(X)) -> mark(h(X)) 189.39/60.88 , proper(f(X)) -> f(proper(X)) 189.39/60.88 , proper(c(X)) -> c(proper(X)) 189.39/60.88 , proper(g(X)) -> g(proper(X)) 189.39/60.88 , proper(d(X)) -> d(proper(X)) 189.39/60.88 , proper(h(X)) -> h(proper(X)) } 189.39/60.88 Weak Trs: 189.39/60.88 { active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.88 , active(c(X)) -> mark(d(X)) 189.39/60.88 , active(h(X)) -> mark(c(d(X))) 189.39/60.88 , c(ok(X)) -> ok(c(X)) 189.39/60.88 , d(ok(X)) -> ok(d(X)) 189.39/60.88 , h(ok(X)) -> ok(h(X)) 189.39/60.88 , top(mark(X)) -> top(proper(X)) 189.39/60.88 , top(ok(X)) -> top(active(X)) } 189.39/60.88 Obligation: 189.39/60.88 derivational complexity 189.39/60.88 Answer: 189.39/60.88 YES(O(1),O(n^2)) 189.39/60.88 189.39/60.88 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.88 orient following rules strictly. 189.39/60.88 189.39/60.88 Trs: 189.39/60.88 { f(ok(X)) -> ok(f(X)) 189.39/60.88 , g(ok(X)) -> ok(g(X)) } 189.39/60.88 189.39/60.88 The induced complexity on above rules (modulo remaining rules) is 189.39/60.88 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.88 component(s). 189.39/60.88 189.39/60.88 Sub-proof: 189.39/60.88 ---------- 189.39/60.88 TcT has computed the following triangular matrix interpretation. 189.39/60.88 189.39/60.88 [active](x1) = [1 1] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [f](x1) = [1 1] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [mark](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [c](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [g](x1) = [1 1] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [d](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [h](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [proper](x1) = [1 0] x1 + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 189.39/60.88 [ok](x1) = [1 2] x1 + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 189.39/60.88 [top](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 189.39/60.88 The order satisfies the following ordering constraints: 189.39/60.88 189.39/60.88 [active(f(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [f(active(X))] 189.39/60.88 189.39/60.88 [active(f(f(X)))] = [1 3] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 3] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(c(f(g(f(X)))))] 189.39/60.88 189.39/60.88 [active(c(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(d(X))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(c(d(X)))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [h(active(X))] 189.39/60.88 189.39/60.88 [f(mark(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(f(X))] 189.39/60.88 189.39/60.88 [f(ok(X))] = [1 3] X + [4] 189.39/60.88 [0 1] [2] 189.39/60.88 > [1 3] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(f(X))] 189.39/60.88 189.39/60.88 [c(ok(X))] = [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(c(X))] 189.39/60.88 189.39/60.88 [g(ok(X))] = [1 3] X + [4] 189.39/60.88 [0 1] [2] 189.39/60.88 > [1 3] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(g(X))] 189.39/60.88 189.39/60.88 [d(ok(X))] = [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(d(X))] 189.39/60.88 189.39/60.88 [h(mark(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(h(X))] 189.39/60.88 189.39/60.88 [h(ok(X))] = [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(h(X))] 189.39/60.88 189.39/60.88 [proper(f(X))] = [1 1] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [f(proper(X))] 189.39/60.88 189.39/60.88 [proper(c(X))] = [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [c(proper(X))] 189.39/60.88 189.39/60.88 [proper(g(X))] = [1 1] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [g(proper(X))] 189.39/60.88 189.39/60.88 [proper(d(X))] = [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [d(proper(X))] 189.39/60.88 189.39/60.88 [proper(h(X))] = [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [h(proper(X))] 189.39/60.88 189.39/60.88 [top(mark(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [2] 189.39/60.88 = [top(proper(X))] 189.39/60.88 189.39/60.88 [top(ok(X))] = [1 2] X + [2] 189.39/60.88 [0 1] [4] 189.39/60.88 > [1 1] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [top(active(X))] 189.39/60.88 189.39/60.88 189.39/60.88 We return to the main proof. 189.39/60.88 189.39/60.88 We are left with following problem, upon which TcT provides the 189.39/60.88 certificate YES(O(1),O(n^2)). 189.39/60.88 189.39/60.88 Strict Trs: 189.39/60.88 { active(f(X)) -> f(active(X)) 189.39/60.88 , active(h(X)) -> h(active(X)) 189.39/60.88 , f(mark(X)) -> mark(f(X)) 189.39/60.88 , h(mark(X)) -> mark(h(X)) 189.39/60.88 , proper(f(X)) -> f(proper(X)) 189.39/60.88 , proper(c(X)) -> c(proper(X)) 189.39/60.88 , proper(g(X)) -> g(proper(X)) 189.39/60.88 , proper(d(X)) -> d(proper(X)) 189.39/60.88 , proper(h(X)) -> h(proper(X)) } 189.39/60.88 Weak Trs: 189.39/60.88 { active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.88 , active(c(X)) -> mark(d(X)) 189.39/60.88 , active(h(X)) -> mark(c(d(X))) 189.39/60.88 , f(ok(X)) -> ok(f(X)) 189.39/60.88 , c(ok(X)) -> ok(c(X)) 189.39/60.88 , g(ok(X)) -> ok(g(X)) 189.39/60.88 , d(ok(X)) -> ok(d(X)) 189.39/60.88 , h(ok(X)) -> ok(h(X)) 189.39/60.88 , top(mark(X)) -> top(proper(X)) 189.39/60.88 , top(ok(X)) -> top(active(X)) } 189.39/60.88 Obligation: 189.39/60.88 derivational complexity 189.39/60.88 Answer: 189.39/60.88 YES(O(1),O(n^2)) 189.39/60.88 189.39/60.88 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.88 orient following rules strictly. 189.39/60.88 189.39/60.88 Trs: { active(h(X)) -> h(active(X)) } 189.39/60.88 189.39/60.88 The induced complexity on above rules (modulo remaining rules) is 189.39/60.88 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.88 component(s). 189.39/60.88 189.39/60.88 Sub-proof: 189.39/60.88 ---------- 189.39/60.88 TcT has computed the following triangular matrix interpretation. 189.39/60.88 189.39/60.88 [active](x1) = [1 1] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [f](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [mark](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [c](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [g](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [d](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [h](x1) = [1 2] x1 + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 189.39/60.88 [proper](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [ok](x1) = [1 1] x1 + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 189.39/60.88 [top](x1) = [1 0] x1 + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 189.39/60.88 The order satisfies the following ordering constraints: 189.39/60.88 189.39/60.88 [active(f(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [f(active(X))] 189.39/60.88 189.39/60.88 [active(f(f(X)))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(c(f(g(f(X)))))] 189.39/60.88 189.39/60.88 [active(c(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(d(X))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1 3] X + [4] 189.39/60.88 [0 1] [2] 189.39/60.88 > [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(c(d(X)))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1 3] X + [4] 189.39/60.88 [0 1] [2] 189.39/60.88 > [1 3] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 = [h(active(X))] 189.39/60.88 189.39/60.88 [f(mark(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(f(X))] 189.39/60.88 189.39/60.88 [f(ok(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 >= [1 1] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 = [ok(f(X))] 189.39/60.88 189.39/60.88 [c(ok(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 >= [1 1] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 = [ok(c(X))] 189.39/60.88 189.39/60.88 [g(ok(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 >= [1 1] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 = [ok(g(X))] 189.39/60.88 189.39/60.88 [d(ok(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 >= [1 1] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 = [ok(d(X))] 189.39/60.88 189.39/60.88 [h(mark(X))] = [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 = [mark(h(X))] 189.39/60.88 189.39/60.88 [h(ok(X))] = [1 3] X + [4] 189.39/60.88 [0 1] [3] 189.39/60.88 >= [1 3] X + [4] 189.39/60.88 [0 1] [3] 189.39/60.88 = [ok(h(X))] 189.39/60.88 189.39/60.88 [proper(f(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [f(proper(X))] 189.39/60.88 189.39/60.88 [proper(c(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [c(proper(X))] 189.39/60.88 189.39/60.88 [proper(g(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [g(proper(X))] 189.39/60.88 189.39/60.88 [proper(d(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [d(proper(X))] 189.39/60.88 189.39/60.88 [proper(h(X))] = [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 = [h(proper(X))] 189.39/60.88 189.39/60.88 [top(mark(X))] = [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [top(proper(X))] 189.39/60.88 189.39/60.88 [top(ok(X))] = [1 1] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 1] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [top(active(X))] 189.39/60.88 189.39/60.88 189.39/60.88 We return to the main proof. 189.39/60.88 189.39/60.88 We are left with following problem, upon which TcT provides the 189.39/60.88 certificate YES(O(1),O(n^2)). 189.39/60.88 189.39/60.88 Strict Trs: 189.39/60.88 { active(f(X)) -> f(active(X)) 189.39/60.88 , f(mark(X)) -> mark(f(X)) 189.39/60.88 , h(mark(X)) -> mark(h(X)) 189.39/60.88 , proper(f(X)) -> f(proper(X)) 189.39/60.88 , proper(c(X)) -> c(proper(X)) 189.39/60.88 , proper(g(X)) -> g(proper(X)) 189.39/60.88 , proper(d(X)) -> d(proper(X)) 189.39/60.88 , proper(h(X)) -> h(proper(X)) } 189.39/60.88 Weak Trs: 189.39/60.88 { active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.88 , active(c(X)) -> mark(d(X)) 189.39/60.88 , active(h(X)) -> mark(c(d(X))) 189.39/60.88 , active(h(X)) -> h(active(X)) 189.39/60.88 , f(ok(X)) -> ok(f(X)) 189.39/60.88 , c(ok(X)) -> ok(c(X)) 189.39/60.88 , g(ok(X)) -> ok(g(X)) 189.39/60.88 , d(ok(X)) -> ok(d(X)) 189.39/60.88 , h(ok(X)) -> ok(h(X)) 189.39/60.88 , top(mark(X)) -> top(proper(X)) 189.39/60.88 , top(ok(X)) -> top(active(X)) } 189.39/60.88 Obligation: 189.39/60.88 derivational complexity 189.39/60.88 Answer: 189.39/60.88 YES(O(1),O(n^2)) 189.39/60.88 189.39/60.88 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.88 orient following rules strictly. 189.39/60.88 189.39/60.88 Trs: { active(f(X)) -> f(active(X)) } 189.39/60.88 189.39/60.88 The induced complexity on above rules (modulo remaining rules) is 189.39/60.88 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.88 component(s). 189.39/60.88 189.39/60.88 Sub-proof: 189.39/60.88 ---------- 189.39/60.88 TcT has computed the following triangular matrix interpretation. 189.39/60.88 189.39/60.88 [active](x1) = [1 1] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [f](x1) = [1 2] x1 + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 189.39/60.88 [mark](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [c](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [g](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [d](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [h](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [proper](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [ok](x1) = [1 2] x1 + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 189.39/60.88 [top](x1) = [1 2] x1 + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 189.39/60.88 The order satisfies the following ordering constraints: 189.39/60.88 189.39/60.88 [active(f(X))] = [1 3] X + [1] 189.39/60.88 [0 1] [1] 189.39/60.88 > [1 3] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 = [f(active(X))] 189.39/60.88 189.39/60.88 [active(f(f(X)))] = [1 5] X + [4] 189.39/60.88 [0 1] [2] 189.39/60.88 > [1 4] X + [2] 189.39/60.88 [0 1] [2] 189.39/60.88 = [mark(c(f(g(f(X)))))] 189.39/60.88 189.39/60.88 [active(c(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(d(X))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(c(d(X)))] 189.39/60.88 189.39/60.88 [active(h(X))] = [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 1] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [h(active(X))] 189.39/60.88 189.39/60.88 [f(mark(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 = [mark(f(X))] 189.39/60.88 189.39/60.88 [f(ok(X))] = [1 4] X + [4] 189.39/60.88 [0 1] [3] 189.39/60.88 > [1 4] X + [2] 189.39/60.88 [0 1] [3] 189.39/60.88 = [ok(f(X))] 189.39/60.88 189.39/60.88 [c(ok(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(c(X))] 189.39/60.88 189.39/60.88 [g(ok(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(g(X))] 189.39/60.88 189.39/60.88 [d(ok(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(d(X))] 189.39/60.88 189.39/60.88 [h(mark(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [mark(h(X))] 189.39/60.88 189.39/60.88 [h(ok(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 = [ok(h(X))] 189.39/60.88 189.39/60.88 [proper(f(X))] = [1 2] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 1] [1] 189.39/60.88 = [f(proper(X))] 189.39/60.88 189.39/60.88 [proper(c(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [c(proper(X))] 189.39/60.88 189.39/60.88 [proper(g(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [g(proper(X))] 189.39/60.88 189.39/60.88 [proper(d(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [d(proper(X))] 189.39/60.88 189.39/60.88 [proper(h(X))] = [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 >= [1 0] X + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 = [h(proper(X))] 189.39/60.88 189.39/60.88 [top(mark(X))] = [1 2] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 >= [1 2] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [top(proper(X))] 189.39/60.88 189.39/60.88 [top(ok(X))] = [1 4] X + [4] 189.39/60.88 [0 0] [0] 189.39/60.88 > [1 3] X + [0] 189.39/60.88 [0 0] [0] 189.39/60.88 = [top(active(X))] 189.39/60.88 189.39/60.88 189.39/60.88 We return to the main proof. 189.39/60.88 189.39/60.88 We are left with following problem, upon which TcT provides the 189.39/60.88 certificate YES(O(1),O(n^2)). 189.39/60.88 189.39/60.88 Strict Trs: 189.39/60.88 { f(mark(X)) -> mark(f(X)) 189.39/60.88 , h(mark(X)) -> mark(h(X)) 189.39/60.88 , proper(f(X)) -> f(proper(X)) 189.39/60.88 , proper(c(X)) -> c(proper(X)) 189.39/60.88 , proper(g(X)) -> g(proper(X)) 189.39/60.88 , proper(d(X)) -> d(proper(X)) 189.39/60.88 , proper(h(X)) -> h(proper(X)) } 189.39/60.88 Weak Trs: 189.39/60.88 { active(f(X)) -> f(active(X)) 189.39/60.88 , active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.88 , active(c(X)) -> mark(d(X)) 189.39/60.88 , active(h(X)) -> mark(c(d(X))) 189.39/60.88 , active(h(X)) -> h(active(X)) 189.39/60.88 , f(ok(X)) -> ok(f(X)) 189.39/60.88 , c(ok(X)) -> ok(c(X)) 189.39/60.88 , g(ok(X)) -> ok(g(X)) 189.39/60.88 , d(ok(X)) -> ok(d(X)) 189.39/60.88 , h(ok(X)) -> ok(h(X)) 189.39/60.88 , top(mark(X)) -> top(proper(X)) 189.39/60.88 , top(ok(X)) -> top(active(X)) } 189.39/60.88 Obligation: 189.39/60.88 derivational complexity 189.39/60.88 Answer: 189.39/60.88 YES(O(1),O(n^2)) 189.39/60.88 189.39/60.88 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.88 orient following rules strictly. 189.39/60.88 189.39/60.88 Trs: { proper(h(X)) -> h(proper(X)) } 189.39/60.88 189.39/60.88 The induced complexity on above rules (modulo remaining rules) is 189.39/60.88 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.88 component(s). 189.39/60.88 189.39/60.88 Sub-proof: 189.39/60.88 ---------- 189.39/60.88 TcT has computed the following triangular matrix interpretation. 189.39/60.88 189.39/60.88 [active](x1) = [1 2] x1 + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 189.39/60.88 [f](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [mark](x1) = [1 2] x1 + [0] 189.39/60.88 [0 1] [2] 189.39/60.88 189.39/60.88 [c](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [g](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [d](x1) = [1 0] x1 + [0] 189.39/60.88 [0 1] [0] 189.39/60.88 189.39/60.88 [h](x1) = [1 2] x1 + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 189.39/60.89 [proper](x1) = [1 2] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [ok](x1) = [1 2] x1 + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 189.39/60.89 [top](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 The order satisfies the following ordering constraints: 189.39/60.89 189.39/60.89 [active(f(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [f(active(X))] 189.39/60.89 189.39/60.89 [active(f(f(X)))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [mark(c(f(g(f(X)))))] 189.39/60.89 189.39/60.89 [active(c(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [mark(d(X))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 4] X + [4] 189.39/60.89 [0 1] [4] 189.39/60.89 > [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [mark(c(d(X)))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 4] X + [4] 189.39/60.89 [0 1] [4] 189.39/60.89 >= [1 4] X + [4] 189.39/60.89 [0 1] [4] 189.39/60.89 = [h(active(X))] 189.39/60.89 189.39/60.89 [f(mark(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [mark(f(X))] 189.39/60.89 189.39/60.89 [f(ok(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(f(X))] 189.39/60.89 189.39/60.89 [c(ok(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(c(X))] 189.39/60.89 189.39/60.89 [g(ok(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(g(X))] 189.39/60.89 189.39/60.89 [d(ok(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(d(X))] 189.39/60.89 189.39/60.89 [h(mark(X))] = [1 4] X + [4] 189.39/60.89 [0 1] [4] 189.39/60.89 >= [1 4] X + [4] 189.39/60.89 [0 1] [4] 189.39/60.89 = [mark(h(X))] 189.39/60.89 189.39/60.89 [h(ok(X))] = [1 4] X + [4] 189.39/60.89 [0 1] [4] 189.39/60.89 >= [1 4] X + [4] 189.39/60.89 [0 1] [4] 189.39/60.89 = [ok(h(X))] 189.39/60.89 189.39/60.89 [proper(f(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [f(proper(X))] 189.39/60.89 189.39/60.89 [proper(c(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [c(proper(X))] 189.39/60.89 189.39/60.89 [proper(g(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [g(proper(X))] 189.39/60.89 189.39/60.89 [proper(d(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [d(proper(X))] 189.39/60.89 189.39/60.89 [proper(h(X))] = [1 4] X + [4] 189.39/60.89 [0 1] [2] 189.39/60.89 > [1 4] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [h(proper(X))] 189.39/60.89 189.39/60.89 [top(mark(X))] = [1 2] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(proper(X))] 189.39/60.89 189.39/60.89 [top(ok(X))] = [1 2] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(active(X))] 189.39/60.89 189.39/60.89 189.39/60.89 We return to the main proof. 189.39/60.89 189.39/60.89 We are left with following problem, upon which TcT provides the 189.39/60.89 certificate YES(O(1),O(n^2)). 189.39/60.89 189.39/60.89 Strict Trs: 189.39/60.89 { f(mark(X)) -> mark(f(X)) 189.39/60.89 , h(mark(X)) -> mark(h(X)) 189.39/60.89 , proper(f(X)) -> f(proper(X)) 189.39/60.89 , proper(c(X)) -> c(proper(X)) 189.39/60.89 , proper(g(X)) -> g(proper(X)) 189.39/60.89 , proper(d(X)) -> d(proper(X)) } 189.39/60.89 Weak Trs: 189.39/60.89 { active(f(X)) -> f(active(X)) 189.39/60.89 , active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.89 , active(c(X)) -> mark(d(X)) 189.39/60.89 , active(h(X)) -> mark(c(d(X))) 189.39/60.89 , active(h(X)) -> h(active(X)) 189.39/60.89 , f(ok(X)) -> ok(f(X)) 189.39/60.89 , c(ok(X)) -> ok(c(X)) 189.39/60.89 , g(ok(X)) -> ok(g(X)) 189.39/60.89 , d(ok(X)) -> ok(d(X)) 189.39/60.89 , h(ok(X)) -> ok(h(X)) 189.39/60.89 , proper(h(X)) -> h(proper(X)) 189.39/60.89 , top(mark(X)) -> top(proper(X)) 189.39/60.89 , top(ok(X)) -> top(active(X)) } 189.39/60.89 Obligation: 189.39/60.89 derivational complexity 189.39/60.89 Answer: 189.39/60.89 YES(O(1),O(n^2)) 189.39/60.89 189.39/60.89 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.89 orient following rules strictly. 189.39/60.89 189.39/60.89 Trs: { proper(g(X)) -> g(proper(X)) } 189.39/60.89 189.39/60.89 The induced complexity on above rules (modulo remaining rules) is 189.39/60.89 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.89 component(s). 189.39/60.89 189.39/60.89 Sub-proof: 189.39/60.89 ---------- 189.39/60.89 TcT has computed the following triangular matrix interpretation. 189.39/60.89 189.39/60.89 [active](x1) = [1 2] x1 + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 [f](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [mark](x1) = [1 1] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 [c](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [g](x1) = [1 1] x1 + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 189.39/60.89 [d](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [h](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [proper](x1) = [1 1] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [ok](x1) = [1 2] x1 + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 189.39/60.89 [top](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 The order satisfies the following ordering constraints: 189.39/60.89 189.39/60.89 [active(f(X))] = [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 = [f(active(X))] 189.39/60.89 189.39/60.89 [active(f(f(X)))] = [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 = [mark(c(f(g(f(X)))))] 189.39/60.89 189.39/60.89 [active(c(X))] = [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 > [1 1] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [mark(d(X))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 > [1 1] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [mark(c(d(X)))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 = [h(active(X))] 189.39/60.89 189.39/60.89 [f(mark(X))] = [1 1] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [mark(f(X))] 189.39/60.89 189.39/60.89 [f(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(f(X))] 189.39/60.89 189.39/60.89 [c(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(c(X))] 189.39/60.89 189.39/60.89 [g(ok(X))] = [1 3] X + [3] 189.39/60.89 [0 1] [3] 189.39/60.89 >= [1 3] X + [3] 189.39/60.89 [0 1] [3] 189.39/60.89 = [ok(g(X))] 189.39/60.89 189.39/60.89 [d(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(d(X))] 189.39/60.89 189.39/60.89 [h(mark(X))] = [1 1] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [mark(h(X))] 189.39/60.89 189.39/60.89 [h(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(h(X))] 189.39/60.89 189.39/60.89 [proper(f(X))] = [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [f(proper(X))] 189.39/60.89 189.39/60.89 [proper(c(X))] = [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [c(proper(X))] 189.39/60.89 189.39/60.89 [proper(g(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [1] 189.39/60.89 > [1 2] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [g(proper(X))] 189.39/60.89 189.39/60.89 [proper(d(X))] = [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [d(proper(X))] 189.39/60.89 189.39/60.89 [proper(h(X))] = [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [h(proper(X))] 189.39/60.89 189.39/60.89 [top(mark(X))] = [1 1] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(proper(X))] 189.39/60.89 189.39/60.89 [top(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(active(X))] 189.39/60.89 189.39/60.89 189.39/60.89 We return to the main proof. 189.39/60.89 189.39/60.89 We are left with following problem, upon which TcT provides the 189.39/60.89 certificate YES(O(1),O(n^2)). 189.39/60.89 189.39/60.89 Strict Trs: 189.39/60.89 { f(mark(X)) -> mark(f(X)) 189.39/60.89 , h(mark(X)) -> mark(h(X)) 189.39/60.89 , proper(f(X)) -> f(proper(X)) 189.39/60.89 , proper(c(X)) -> c(proper(X)) 189.39/60.89 , proper(d(X)) -> d(proper(X)) } 189.39/60.89 Weak Trs: 189.39/60.89 { active(f(X)) -> f(active(X)) 189.39/60.89 , active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.89 , active(c(X)) -> mark(d(X)) 189.39/60.89 , active(h(X)) -> mark(c(d(X))) 189.39/60.89 , active(h(X)) -> h(active(X)) 189.39/60.89 , f(ok(X)) -> ok(f(X)) 189.39/60.89 , c(ok(X)) -> ok(c(X)) 189.39/60.89 , g(ok(X)) -> ok(g(X)) 189.39/60.89 , d(ok(X)) -> ok(d(X)) 189.39/60.89 , h(ok(X)) -> ok(h(X)) 189.39/60.89 , proper(g(X)) -> g(proper(X)) 189.39/60.89 , proper(h(X)) -> h(proper(X)) 189.39/60.89 , top(mark(X)) -> top(proper(X)) 189.39/60.89 , top(ok(X)) -> top(active(X)) } 189.39/60.89 Obligation: 189.39/60.89 derivational complexity 189.39/60.89 Answer: 189.39/60.89 YES(O(1),O(n^2)) 189.39/60.89 189.39/60.89 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.89 orient following rules strictly. 189.39/60.89 189.39/60.89 Trs: { f(mark(X)) -> mark(f(X)) } 189.39/60.89 189.39/60.89 The induced complexity on above rules (modulo remaining rules) is 189.39/60.89 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.89 component(s). 189.39/60.89 189.39/60.89 Sub-proof: 189.39/60.89 ---------- 189.39/60.89 TcT has computed the following triangular matrix interpretation. 189.39/60.89 189.39/60.89 [active](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [f](x1) = [1 1] x1 + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 189.39/60.89 [mark](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 189.39/60.89 [c](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 189.39/60.89 [g](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 [d](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 [h](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 189.39/60.89 [proper](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [ok](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [top](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 The order satisfies the following ordering constraints: 189.39/60.89 189.39/60.89 [active(f(X))] = [1 1] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [f(active(X))] 189.39/60.89 189.39/60.89 [active(f(f(X)))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 > [1 1] X + [0] 189.39/60.89 [0 0] [2] 189.39/60.89 = [mark(c(f(g(f(X)))))] 189.39/60.89 189.39/60.89 [active(c(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 = [mark(d(X))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [2] 189.39/60.89 = [mark(c(d(X)))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [h(active(X))] 189.39/60.89 189.39/60.89 [f(mark(X))] = [1 1] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 > [1 1] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [mark(f(X))] 189.39/60.89 189.39/60.89 [f(ok(X))] = [1 1] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [ok(f(X))] 189.39/60.89 189.39/60.89 [c(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 = [ok(c(X))] 189.39/60.89 189.39/60.89 [g(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [ok(g(X))] 189.39/60.89 189.39/60.89 [d(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [ok(d(X))] 189.39/60.89 189.39/60.89 [h(mark(X))] = [1 0] X + [0] 189.39/60.89 [0 1] [3] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 1] [3] 189.39/60.89 = [mark(h(X))] 189.39/60.89 189.39/60.89 [h(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(h(X))] 189.39/60.89 189.39/60.89 [proper(f(X))] = [1 1] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [f(proper(X))] 189.39/60.89 189.39/60.89 [proper(c(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 = [c(proper(X))] 189.39/60.89 189.39/60.89 [proper(g(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [g(proper(X))] 189.39/60.89 189.39/60.89 [proper(d(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [d(proper(X))] 189.39/60.89 189.39/60.89 [proper(h(X))] = [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [h(proper(X))] 189.39/60.89 189.39/60.89 [top(mark(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(proper(X))] 189.39/60.89 189.39/60.89 [top(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(active(X))] 189.39/60.89 189.39/60.89 189.39/60.89 We return to the main proof. 189.39/60.89 189.39/60.89 We are left with following problem, upon which TcT provides the 189.39/60.89 certificate YES(O(1),O(n^2)). 189.39/60.89 189.39/60.89 Strict Trs: 189.39/60.89 { h(mark(X)) -> mark(h(X)) 189.39/60.89 , proper(f(X)) -> f(proper(X)) 189.39/60.89 , proper(c(X)) -> c(proper(X)) 189.39/60.89 , proper(d(X)) -> d(proper(X)) } 189.39/60.89 Weak Trs: 189.39/60.89 { active(f(X)) -> f(active(X)) 189.39/60.89 , active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.89 , active(c(X)) -> mark(d(X)) 189.39/60.89 , active(h(X)) -> mark(c(d(X))) 189.39/60.89 , active(h(X)) -> h(active(X)) 189.39/60.89 , f(mark(X)) -> mark(f(X)) 189.39/60.89 , f(ok(X)) -> ok(f(X)) 189.39/60.89 , c(ok(X)) -> ok(c(X)) 189.39/60.89 , g(ok(X)) -> ok(g(X)) 189.39/60.89 , d(ok(X)) -> ok(d(X)) 189.39/60.89 , h(ok(X)) -> ok(h(X)) 189.39/60.89 , proper(g(X)) -> g(proper(X)) 189.39/60.89 , proper(h(X)) -> h(proper(X)) 189.39/60.89 , top(mark(X)) -> top(proper(X)) 189.39/60.89 , top(ok(X)) -> top(active(X)) } 189.39/60.89 Obligation: 189.39/60.89 derivational complexity 189.39/60.89 Answer: 189.39/60.89 YES(O(1),O(n^2)) 189.39/60.89 189.39/60.89 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.89 orient following rules strictly. 189.39/60.89 189.39/60.89 Trs: { h(mark(X)) -> mark(h(X)) } 189.39/60.89 189.39/60.89 The induced complexity on above rules (modulo remaining rules) is 189.39/60.89 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.89 component(s). 189.39/60.89 189.39/60.89 Sub-proof: 189.39/60.89 ---------- 189.39/60.89 TcT has computed the following triangular matrix interpretation. 189.39/60.89 189.39/60.89 [active](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [f](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 189.39/60.89 [mark](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 189.39/60.89 [c](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 189.39/60.89 [g](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 [d](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 [h](x1) = [1 2] x1 + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 189.39/60.89 [proper](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [ok](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [top](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 The order satisfies the following ordering constraints: 189.39/60.89 189.39/60.89 [active(f(X))] = [1 0] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [f(active(X))] 189.39/60.89 189.39/60.89 [active(f(f(X)))] = [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [2] 189.39/60.89 = [mark(c(f(g(f(X)))))] 189.39/60.89 189.39/60.89 [active(c(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 = [mark(d(X))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [2] 189.39/60.89 = [mark(c(d(X)))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [h(active(X))] 189.39/60.89 189.39/60.89 [f(mark(X))] = [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [mark(f(X))] 189.39/60.89 189.39/60.89 [f(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [ok(f(X))] 189.39/60.89 189.39/60.89 [c(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 = [ok(c(X))] 189.39/60.89 189.39/60.89 [g(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [ok(g(X))] 189.39/60.89 189.39/60.89 [d(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [ok(d(X))] 189.39/60.89 189.39/60.89 [h(mark(X))] = [1 2] X + [2] 189.39/60.89 [0 1] [3] 189.39/60.89 > [1 2] X + [0] 189.39/60.89 [0 1] [3] 189.39/60.89 = [mark(h(X))] 189.39/60.89 189.39/60.89 [h(ok(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(h(X))] 189.39/60.89 189.39/60.89 [proper(f(X))] = [1 0] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [f(proper(X))] 189.39/60.89 189.39/60.89 [proper(c(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [1] 189.39/60.89 = [c(proper(X))] 189.39/60.89 189.39/60.89 [proper(g(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [g(proper(X))] 189.39/60.89 189.39/60.89 [proper(d(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [d(proper(X))] 189.39/60.89 189.39/60.89 [proper(h(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [h(proper(X))] 189.39/60.89 189.39/60.89 [top(mark(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(proper(X))] 189.39/60.89 189.39/60.89 [top(ok(X))] = [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 0] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(active(X))] 189.39/60.89 189.39/60.89 189.39/60.89 We return to the main proof. 189.39/60.89 189.39/60.89 We are left with following problem, upon which TcT provides the 189.39/60.89 certificate YES(O(1),O(n^2)). 189.39/60.89 189.39/60.89 Strict Trs: 189.39/60.89 { proper(f(X)) -> f(proper(X)) 189.39/60.89 , proper(c(X)) -> c(proper(X)) 189.39/60.89 , proper(d(X)) -> d(proper(X)) } 189.39/60.89 Weak Trs: 189.39/60.89 { active(f(X)) -> f(active(X)) 189.39/60.89 , active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.89 , active(c(X)) -> mark(d(X)) 189.39/60.89 , active(h(X)) -> mark(c(d(X))) 189.39/60.89 , active(h(X)) -> h(active(X)) 189.39/60.89 , f(mark(X)) -> mark(f(X)) 189.39/60.89 , f(ok(X)) -> ok(f(X)) 189.39/60.89 , c(ok(X)) -> ok(c(X)) 189.39/60.89 , g(ok(X)) -> ok(g(X)) 189.39/60.89 , d(ok(X)) -> ok(d(X)) 189.39/60.89 , h(mark(X)) -> mark(h(X)) 189.39/60.89 , h(ok(X)) -> ok(h(X)) 189.39/60.89 , proper(g(X)) -> g(proper(X)) 189.39/60.89 , proper(h(X)) -> h(proper(X)) 189.39/60.89 , top(mark(X)) -> top(proper(X)) 189.39/60.89 , top(ok(X)) -> top(active(X)) } 189.39/60.89 Obligation: 189.39/60.89 derivational complexity 189.39/60.89 Answer: 189.39/60.89 YES(O(1),O(n^2)) 189.39/60.89 189.39/60.89 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.89 orient following rules strictly. 189.39/60.89 189.39/60.89 Trs: { proper(f(X)) -> f(proper(X)) } 189.39/60.89 189.39/60.89 The induced complexity on above rules (modulo remaining rules) is 189.39/60.89 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.89 component(s). 189.39/60.89 189.39/60.89 Sub-proof: 189.39/60.89 ---------- 189.39/60.89 TcT has computed the following triangular matrix interpretation. 189.39/60.89 189.39/60.89 [active](x1) = [1 2] x1 + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 189.39/60.89 [f](x1) = [1 1] x1 + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 189.39/60.89 [mark](x1) = [1 2] x1 + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 189.39/60.89 [c](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [g](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [d](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [h](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [proper](x1) = [1 2] x1 + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 189.39/60.89 [ok](x1) = [1 2] x1 + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 189.39/60.89 [top](x1) = [1 0] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 The order satisfies the following ordering constraints: 189.39/60.89 189.39/60.89 [active(f(X))] = [1 3] X + [3] 189.39/60.89 [0 1] [3] 189.39/60.89 >= [1 3] X + [3] 189.39/60.89 [0 1] [3] 189.39/60.89 = [f(active(X))] 189.39/60.89 189.39/60.89 [active(f(f(X)))] = [1 4] X + [6] 189.39/60.89 [0 1] [4] 189.39/60.89 > [1 4] X + [5] 189.39/60.89 [0 1] [4] 189.39/60.89 = [mark(c(f(g(f(X)))))] 189.39/60.89 189.39/60.89 [active(c(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 > [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [mark(d(X))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 > [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [mark(c(d(X)))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [h(active(X))] 189.39/60.89 189.39/60.89 [f(mark(X))] = [1 3] X + [2] 189.39/60.89 [0 1] [3] 189.39/60.89 >= [1 3] X + [2] 189.39/60.89 [0 1] [3] 189.39/60.89 = [mark(f(X))] 189.39/60.89 189.39/60.89 [f(ok(X))] = [1 3] X + [3] 189.39/60.89 [0 1] [3] 189.39/60.89 >= [1 3] X + [3] 189.39/60.89 [0 1] [3] 189.39/60.89 = [ok(f(X))] 189.39/60.89 189.39/60.89 [c(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(c(X))] 189.39/60.89 189.39/60.89 [g(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(g(X))] 189.39/60.89 189.39/60.89 [d(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(d(X))] 189.39/60.89 189.39/60.89 [h(mark(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [mark(h(X))] 189.39/60.89 189.39/60.89 [h(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(h(X))] 189.39/60.89 189.39/60.89 [proper(f(X))] = [1 3] X + [2] 189.39/60.89 [0 1] [2] 189.39/60.89 > [1 3] X + [1] 189.39/60.89 [0 1] [2] 189.39/60.89 = [f(proper(X))] 189.39/60.89 189.39/60.89 [proper(c(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [c(proper(X))] 189.39/60.89 189.39/60.89 [proper(g(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [g(proper(X))] 189.39/60.89 189.39/60.89 [proper(d(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [d(proper(X))] 189.39/60.89 189.39/60.89 [proper(h(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 = [h(proper(X))] 189.39/60.89 189.39/60.89 [top(mark(X))] = [1 2] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(proper(X))] 189.39/60.89 189.39/60.89 [top(ok(X))] = [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 >= [1 2] X + [1] 189.39/60.89 [0 0] [0] 189.39/60.89 = [top(active(X))] 189.39/60.89 189.39/60.89 189.39/60.89 We return to the main proof. 189.39/60.89 189.39/60.89 We are left with following problem, upon which TcT provides the 189.39/60.89 certificate YES(O(1),O(n^2)). 189.39/60.89 189.39/60.89 Strict Trs: 189.39/60.89 { proper(c(X)) -> c(proper(X)) 189.39/60.89 , proper(d(X)) -> d(proper(X)) } 189.39/60.89 Weak Trs: 189.39/60.89 { active(f(X)) -> f(active(X)) 189.39/60.89 , active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.89 , active(c(X)) -> mark(d(X)) 189.39/60.89 , active(h(X)) -> mark(c(d(X))) 189.39/60.89 , active(h(X)) -> h(active(X)) 189.39/60.89 , f(mark(X)) -> mark(f(X)) 189.39/60.89 , f(ok(X)) -> ok(f(X)) 189.39/60.89 , c(ok(X)) -> ok(c(X)) 189.39/60.89 , g(ok(X)) -> ok(g(X)) 189.39/60.89 , d(ok(X)) -> ok(d(X)) 189.39/60.89 , h(mark(X)) -> mark(h(X)) 189.39/60.89 , h(ok(X)) -> ok(h(X)) 189.39/60.89 , proper(f(X)) -> f(proper(X)) 189.39/60.89 , proper(g(X)) -> g(proper(X)) 189.39/60.89 , proper(h(X)) -> h(proper(X)) 189.39/60.89 , top(mark(X)) -> top(proper(X)) 189.39/60.89 , top(ok(X)) -> top(active(X)) } 189.39/60.89 Obligation: 189.39/60.89 derivational complexity 189.39/60.89 Answer: 189.39/60.89 YES(O(1),O(n^2)) 189.39/60.89 189.39/60.89 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.89 orient following rules strictly. 189.39/60.89 189.39/60.89 Trs: { proper(d(X)) -> d(proper(X)) } 189.39/60.89 189.39/60.89 The induced complexity on above rules (modulo remaining rules) is 189.39/60.89 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.89 component(s). 189.39/60.89 189.39/60.89 Sub-proof: 189.39/60.89 ---------- 189.39/60.89 TcT has computed the following triangular matrix interpretation. 189.39/60.89 189.39/60.89 [active](x1) = [1 2] x1 + [2] 189.39/60.89 [0 1] [1] 189.39/60.89 189.39/60.89 [f](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [mark](x1) = [1 1] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [c](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [g](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [d](x1) = [1 1] x1 + [0] 189.39/60.89 [0 1] [1] 189.39/60.89 189.39/60.89 [h](x1) = [1 0] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [proper](x1) = [1 1] x1 + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 189.39/60.89 [ok](x1) = [1 2] x1 + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 189.39/60.89 [top](x1) = [1 2] x1 + [0] 189.39/60.89 [0 0] [0] 189.39/60.89 189.39/60.89 The order satisfies the following ordering constraints: 189.39/60.89 189.39/60.89 [active(f(X))] = [1 2] X + [2] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 2] X + [2] 189.39/60.89 [0 1] [1] 189.39/60.89 = [f(active(X))] 189.39/60.89 189.39/60.89 [active(f(f(X)))] = [1 2] X + [2] 189.39/60.89 [0 1] [1] 189.39/60.89 > [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [mark(c(f(g(f(X)))))] 189.39/60.89 189.39/60.89 [active(c(X))] = [1 2] X + [2] 189.39/60.89 [0 1] [1] 189.39/60.89 > [1 2] X + [1] 189.39/60.89 [0 1] [1] 189.39/60.89 = [mark(d(X))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 2] X + [2] 189.39/60.89 [0 1] [1] 189.39/60.89 > [1 2] X + [1] 189.39/60.89 [0 1] [1] 189.39/60.89 = [mark(c(d(X)))] 189.39/60.89 189.39/60.89 [active(h(X))] = [1 2] X + [2] 189.39/60.89 [0 1] [1] 189.39/60.89 >= [1 2] X + [2] 189.39/60.89 [0 1] [1] 189.39/60.89 = [h(active(X))] 189.39/60.89 189.39/60.89 [f(mark(X))] = [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [mark(f(X))] 189.39/60.89 189.39/60.89 [f(ok(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(f(X))] 189.39/60.89 189.39/60.89 [c(ok(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(c(X))] 189.39/60.89 189.39/60.89 [g(ok(X))] = [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 >= [1 2] X + [0] 189.39/60.89 [0 1] [2] 189.39/60.89 = [ok(g(X))] 189.39/60.89 189.39/60.89 [d(ok(X))] = [1 3] X + [2] 189.39/60.89 [0 1] [3] 189.39/60.89 >= [1 3] X + [2] 189.39/60.89 [0 1] [3] 189.39/60.89 = [ok(d(X))] 189.39/60.89 189.39/60.89 [h(mark(X))] = [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 >= [1 1] X + [0] 189.39/60.89 [0 1] [0] 189.39/60.89 = [mark(h(X))] 189.39/60.89 189.39/60.89 [h(ok(X))] = [1 2] X + [0] 189.39/60.90 [0 1] [2] 189.39/60.90 >= [1 2] X + [0] 189.39/60.90 [0 1] [2] 189.39/60.90 = [ok(h(X))] 189.39/60.90 189.39/60.90 [proper(f(X))] = [1 1] X + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 >= [1 1] X + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 = [f(proper(X))] 189.39/60.90 189.39/60.90 [proper(c(X))] = [1 1] X + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 >= [1 1] X + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 = [c(proper(X))] 189.39/60.90 189.39/60.90 [proper(g(X))] = [1 1] X + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 >= [1 1] X + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 = [g(proper(X))] 189.39/60.90 189.39/60.90 [proper(d(X))] = [1 2] X + [1] 189.39/60.90 [0 1] [1] 189.39/60.90 > [1 2] X + [0] 189.39/60.90 [0 1] [1] 189.39/60.90 = [d(proper(X))] 189.39/60.90 189.39/60.90 [proper(h(X))] = [1 1] X + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 >= [1 1] X + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 = [h(proper(X))] 189.39/60.90 189.39/60.90 [top(mark(X))] = [1 3] X + [0] 189.39/60.90 [0 0] [0] 189.39/60.90 >= [1 3] X + [0] 189.39/60.90 [0 0] [0] 189.39/60.90 = [top(proper(X))] 189.39/60.90 189.39/60.90 [top(ok(X))] = [1 4] X + [4] 189.39/60.90 [0 0] [0] 189.39/60.90 >= [1 4] X + [4] 189.39/60.90 [0 0] [0] 189.39/60.90 = [top(active(X))] 189.39/60.90 189.39/60.90 189.39/60.90 We return to the main proof. 189.39/60.90 189.39/60.90 We are left with following problem, upon which TcT provides the 189.39/60.90 certificate YES(O(1),O(n^2)). 189.39/60.90 189.39/60.90 Strict Trs: { proper(c(X)) -> c(proper(X)) } 189.39/60.90 Weak Trs: 189.39/60.90 { active(f(X)) -> f(active(X)) 189.39/60.90 , active(f(f(X))) -> mark(c(f(g(f(X))))) 189.39/60.90 , active(c(X)) -> mark(d(X)) 189.39/60.90 , active(h(X)) -> mark(c(d(X))) 189.39/60.90 , active(h(X)) -> h(active(X)) 189.39/60.90 , f(mark(X)) -> mark(f(X)) 189.39/60.90 , f(ok(X)) -> ok(f(X)) 189.39/60.90 , c(ok(X)) -> ok(c(X)) 189.39/60.90 , g(ok(X)) -> ok(g(X)) 189.39/60.90 , d(ok(X)) -> ok(d(X)) 189.39/60.90 , h(mark(X)) -> mark(h(X)) 189.39/60.90 , h(ok(X)) -> ok(h(X)) 189.39/60.90 , proper(f(X)) -> f(proper(X)) 189.39/60.90 , proper(g(X)) -> g(proper(X)) 189.39/60.90 , proper(d(X)) -> d(proper(X)) 189.39/60.90 , proper(h(X)) -> h(proper(X)) 189.39/60.90 , top(mark(X)) -> top(proper(X)) 189.39/60.90 , top(ok(X)) -> top(active(X)) } 189.39/60.90 Obligation: 189.39/60.90 derivational complexity 189.39/60.90 Answer: 189.39/60.90 YES(O(1),O(n^2)) 189.39/60.90 189.39/60.90 We use the processor 'matrix interpretation of dimension 2' to 189.39/60.90 orient following rules strictly. 189.39/60.90 189.39/60.90 Trs: { proper(c(X)) -> c(proper(X)) } 189.39/60.90 189.39/60.90 The induced complexity on above rules (modulo remaining rules) is 189.39/60.90 YES(?,O(n^2)) . These rules are moved into the corresponding weak 189.39/60.90 component(s). 189.39/60.90 189.39/60.90 Sub-proof: 189.39/60.90 ---------- 189.39/60.90 TcT has computed the following triangular matrix interpretation. 189.39/60.90 189.39/60.90 [active](x1) = [1 2] x1 + [1] 189.39/60.90 [0 0] [0] 189.39/60.90 189.39/60.90 [f](x1) = [1 0] x1 + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 189.39/60.90 [mark](x1) = [1 1] x1 + [0] 189.39/60.90 [0 0] [0] 189.39/60.90 189.39/60.90 [c](x1) = [1 1] x1 + [0] 189.39/60.90 [0 1] [1] 189.39/60.90 189.39/60.90 [g](x1) = [1 0] x1 + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 189.39/60.90 [d](x1) = [1 0] x1 + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 189.39/60.90 [h](x1) = [1 0] x1 + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 189.39/60.90 [proper](x1) = [1 1] x1 + [0] 189.39/60.90 [0 1] [0] 189.39/60.90 189.39/60.90 [ok](x1) = [1 2] x1 + [1] 189.39/60.90 [0 1] [2] 189.39/60.90 189.39/60.90 [top](x1) = [1 0] x1 + [0] 189.39/60.90 [0 0] [0] 189.39/60.90 189.39/60.90 The order satisfies the following ordering constraints: 189.39/60.90 189.39/60.90 [active(f(X))] = [1 2] X + [1] 189.39/60.90 [0 0] [0] 189.39/60.90 >= [1 2] X + [1] 189.39/60.90 [0 0] [0] 189.39/60.90 = [f(active(X))] 189.39/60.90 189.39/60.90 [active(f(f(X)))] = [1 2] X + [1] 189.39/60.90 [0 0] [0] 189.39/60.90 >= [1 2] X + [1] 189.39/60.90 [0 0] [0] 189.39/60.90 = [mark(c(f(g(f(X)))))] 189.39/60.90 189.39/60.90 [active(c(X))] = [1 3] X + [3] 189.39/60.90 [0 0] [0] 189.39/60.90 > [1 1] X + [0] 189.39/60.90 [0 0] [0] 189.39/60.90 = [mark(d(X))] 189.39/60.90 189.39/60.90 [active(h(X))] = [1 2] X + [1] 189.39/60.90 [0 0] [0] 189.39/60.90 >= [1 2] X + [1] 189.39/60.90 [0 0] [0] 189.39/60.90 = [mark(c(d(X)))] 189.39/60.90 189.39/60.90 [active(h(X))] = [1 2] X + [1] 189.39/60.90 [0 0] [0] 189.39/60.90 >= [1 2] X + [1] 189.39/60.90 [0 0] [0] 189.39/60.90 = [h(active(X))] 189.39/60.90 189.39/60.90 [f(mark(X))] = [1 1] X + [0] 189.39/60.90 [0 0] [0] 189.39/60.90 >= [1 1] X + [0] 189.39/60.90 [0 0] [0] 189.39/60.90 = [mark(f(X))] 189.39/60.90 189.39/60.90 [f(ok(X))] = [1 2] X + [1] 189.39/60.90 [0 1] [2] 189.39/60.90 >= [1 2] X + [1] 189.39/60.90 [0 1] [2] 189.39/60.90 = [ok(f(X))] 189.39/60.90 189.39/60.90 [c(ok(X))] = [1 3] X + [3] 189.39/60.90 [0 1] [3] 189.39/60.90 >= [1 3] X + [3] 189.39/60.90 [0 1] [3] 189.39/60.90 = [ok(c(X))] 189.39/60.90 189.39/60.90 [g(ok(X))] = [1 2] X + [1] 189.39/60.90 [0 1] [2] 189.39/60.90 >= [1 2] X + [1] 189.39/60.90 [0 1] [2] 189.39/60.90 = [ok(g(X))] 189.39/60.90 189.39/60.90 [d(ok(X))] = [1 2] X + [1] 189.39/60.90 [0 1] [2] 189.54/60.90 >= [1 2] X + [1] 189.54/60.90 [0 1] [2] 189.54/60.90 = [ok(d(X))] 189.54/60.90 189.54/60.90 [h(mark(X))] = [1 1] X + [0] 189.54/60.90 [0 0] [0] 189.54/60.90 >= [1 1] X + [0] 189.54/60.90 [0 0] [0] 189.54/60.90 = [mark(h(X))] 189.54/60.90 189.54/60.90 [h(ok(X))] = [1 2] X + [1] 189.54/60.90 [0 1] [2] 189.54/60.90 >= [1 2] X + [1] 189.54/60.90 [0 1] [2] 189.54/60.90 = [ok(h(X))] 189.54/60.90 189.54/60.90 [proper(f(X))] = [1 1] X + [0] 189.54/60.90 [0 1] [0] 189.54/60.90 >= [1 1] X + [0] 189.54/60.90 [0 1] [0] 189.54/60.90 = [f(proper(X))] 189.54/60.90 189.54/60.90 [proper(c(X))] = [1 2] X + [1] 189.54/60.90 [0 1] [1] 189.54/60.90 > [1 2] X + [0] 189.54/60.90 [0 1] [1] 189.54/60.90 = [c(proper(X))] 189.54/60.90 189.54/60.90 [proper(g(X))] = [1 1] X + [0] 189.54/60.90 [0 1] [0] 189.54/60.90 >= [1 1] X + [0] 189.54/60.90 [0 1] [0] 189.54/60.90 = [g(proper(X))] 189.54/60.90 189.54/60.90 [proper(d(X))] = [1 1] X + [0] 189.54/60.90 [0 1] [0] 189.54/60.90 >= [1 1] X + [0] 189.54/60.90 [0 1] [0] 189.54/60.90 = [d(proper(X))] 189.54/60.90 189.54/60.90 [proper(h(X))] = [1 1] X + [0] 189.54/60.90 [0 1] [0] 189.54/60.90 >= [1 1] X + [0] 189.54/60.90 [0 1] [0] 189.54/60.90 = [h(proper(X))] 189.54/60.90 189.54/60.90 [top(mark(X))] = [1 1] X + [0] 189.54/60.90 [0 0] [0] 189.54/60.90 >= [1 1] X + [0] 189.54/60.90 [0 0] [0] 189.54/60.90 = [top(proper(X))] 189.54/60.90 189.54/60.90 [top(ok(X))] = [1 2] X + [1] 189.54/60.90 [0 0] [0] 189.54/60.90 >= [1 2] X + [1] 189.54/60.90 [0 0] [0] 189.54/60.90 = [top(active(X))] 189.54/60.90 189.54/60.90 189.54/60.90 We return to the main proof. 189.54/60.90 189.54/60.90 We are left with following problem, upon which TcT provides the 189.54/60.90 certificate YES(O(1),O(1)). 189.54/60.90 189.54/60.90 Weak Trs: 189.54/60.90 { active(f(X)) -> f(active(X)) 189.54/60.90 , active(f(f(X))) -> mark(c(f(g(f(X))))) 189.54/60.90 , active(c(X)) -> mark(d(X)) 189.54/60.90 , active(h(X)) -> mark(c(d(X))) 189.54/60.90 , active(h(X)) -> h(active(X)) 189.54/60.90 , f(mark(X)) -> mark(f(X)) 189.54/60.90 , f(ok(X)) -> ok(f(X)) 189.54/60.90 , c(ok(X)) -> ok(c(X)) 189.54/60.90 , g(ok(X)) -> ok(g(X)) 189.54/60.90 , d(ok(X)) -> ok(d(X)) 189.54/60.90 , h(mark(X)) -> mark(h(X)) 189.54/60.90 , h(ok(X)) -> ok(h(X)) 189.54/60.90 , proper(f(X)) -> f(proper(X)) 189.54/60.90 , proper(c(X)) -> c(proper(X)) 189.54/60.90 , proper(g(X)) -> g(proper(X)) 189.54/60.90 , proper(d(X)) -> d(proper(X)) 189.54/60.90 , proper(h(X)) -> h(proper(X)) 189.54/60.90 , top(mark(X)) -> top(proper(X)) 189.54/60.90 , top(ok(X)) -> top(active(X)) } 189.54/60.90 Obligation: 189.54/60.90 derivational complexity 189.54/60.90 Answer: 189.54/60.90 YES(O(1),O(1)) 189.54/60.90 189.54/60.90 Empty rules are trivially bounded 189.54/60.90 189.54/60.90 Hurray, we answered YES(O(1),O(n^2)) 189.54/60.91 EOF