YES(O(1),O(n^2)) 600.61/155.55 YES(O(1),O(n^2)) 600.61/155.55 600.61/155.55 We are left with following problem, upon which TcT provides the 600.61/155.55 certificate YES(O(1),O(n^2)). 600.61/155.55 600.61/155.55 Strict Trs: 600.61/155.55 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.55 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.55 , active(g(X)) -> g(active(X)) 600.61/155.55 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.55 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.55 , g(mark(X)) -> mark(g(X)) 600.61/155.55 , g(ok(X)) -> ok(g(X)) 600.61/155.55 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.55 , proper(g(X)) -> g(proper(X)) 600.61/155.55 , top(mark(X)) -> top(proper(X)) 600.61/155.55 , top(ok(X)) -> top(active(X)) } 600.61/155.55 Obligation: 600.61/155.55 innermost runtime complexity 600.61/155.55 Answer: 600.61/155.55 YES(O(1),O(n^2)) 600.61/155.55 600.61/155.55 We add the following dependency tuples: 600.61/155.55 600.61/155.55 Strict DPs: 600.61/155.55 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.55 , active^#(f(g(X), Y)) -> 600.61/155.55 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.55 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.55 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.55 , f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.55 , g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.55 , g^#(ok(X)) -> c_7(g^#(X)) 600.61/155.55 , proper^#(f(X1, X2)) -> 600.61/155.55 c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.55 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.55 600.61/155.55 and mark the set of starting terms. 600.61/155.55 600.61/155.55 We are left with following problem, upon which TcT provides the 600.61/155.55 certificate YES(O(1),O(n^2)). 600.61/155.55 600.61/155.55 Strict DPs: 600.61/155.55 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.55 , active^#(f(g(X), Y)) -> 600.61/155.55 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.55 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.55 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.55 , f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.55 , g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.55 , g^#(ok(X)) -> c_7(g^#(X)) 600.61/155.55 , proper^#(f(X1, X2)) -> 600.61/155.55 c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.55 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.55 Weak Trs: 600.61/155.55 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.55 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.55 , active(g(X)) -> g(active(X)) 600.61/155.55 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.55 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.55 , g(mark(X)) -> mark(g(X)) 600.61/155.55 , g(ok(X)) -> ok(g(X)) 600.61/155.55 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.55 , proper(g(X)) -> g(proper(X)) 600.61/155.55 , top(mark(X)) -> top(proper(X)) 600.61/155.55 , top(ok(X)) -> top(active(X)) } 600.61/155.55 Obligation: 600.61/155.55 innermost runtime complexity 600.61/155.55 Answer: 600.61/155.55 YES(O(1),O(n^2)) 600.61/155.55 600.61/155.55 We replace rewrite rules by usable rules: 600.61/155.55 600.61/155.55 Weak Usable Rules: 600.61/155.55 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.55 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.55 , active(g(X)) -> g(active(X)) 600.61/155.55 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.55 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.55 , g(mark(X)) -> mark(g(X)) 600.61/155.55 , g(ok(X)) -> ok(g(X)) 600.61/155.55 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.55 , proper(g(X)) -> g(proper(X)) } 600.61/155.55 600.61/155.55 We are left with following problem, upon which TcT provides the 600.61/155.55 certificate YES(O(1),O(n^2)). 600.61/155.55 600.61/155.55 Strict DPs: 600.61/155.55 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.55 , active^#(f(g(X), Y)) -> 600.61/155.55 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.55 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.55 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.55 , f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.55 , g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.55 , g^#(ok(X)) -> c_7(g^#(X)) 600.61/155.55 , proper^#(f(X1, X2)) -> 600.61/155.55 c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.55 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.55 Weak Trs: 600.61/155.55 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.55 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.55 , active(g(X)) -> g(active(X)) 600.61/155.55 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.55 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.55 , g(mark(X)) -> mark(g(X)) 600.61/155.55 , g(ok(X)) -> ok(g(X)) 600.61/155.55 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.55 , proper(g(X)) -> g(proper(X)) } 600.61/155.55 Obligation: 600.61/155.55 innermost runtime complexity 600.61/155.55 Answer: 600.61/155.55 YES(O(1),O(n^2)) 600.61/155.55 600.61/155.55 We use the processor 'matrix interpretation of dimension 2' to 600.61/155.55 orient following rules strictly. 600.61/155.55 600.61/155.55 DPs: 600.61/155.55 { 5: f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.55 , 11: top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.55 Trs: { f(ok(X1), ok(X2)) -> ok(f(X1, X2)) } 600.61/155.55 600.61/155.55 Sub-proof: 600.61/155.55 ---------- 600.61/155.55 The following argument positions are usable: 600.61/155.55 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 3}, Uargs(c_3) = {1, 2}, 600.61/155.55 Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 600.61/155.55 Uargs(c_7) = {1}, Uargs(c_8) = {1, 2, 3}, Uargs(c_9) = {1, 2}, 600.61/155.55 Uargs(c_10) = {1, 2}, Uargs(c_11) = {1, 2} 600.61/155.55 600.61/155.55 TcT has computed the following constructor-based matrix 600.61/155.55 interpretation satisfying not(EDA) and not(IDA(1)). 600.61/155.55 600.61/155.55 [active](x1) = [0 0] x1 + [0] 600.61/155.55 [2 1] [0] 600.61/155.55 600.61/155.55 [f](x1, x2) = [4 0] x1 + [0] 600.61/155.55 [0 4] [0] 600.61/155.55 600.61/155.55 [g](x1) = [1 0] x1 + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 600.61/155.55 [mark](x1) = [0 0] x1 + [0] 600.61/155.55 [1 1] [0] 600.61/155.55 600.61/155.55 [proper](x1) = [0] 600.61/155.55 [0] 600.61/155.55 600.61/155.55 [ok](x1) = [1 1] x1 + [1] 600.61/155.55 [0 0] [0] 600.61/155.55 600.61/155.55 [active^#](x1) = [1 2] x1 + [0] 600.61/155.55 [0 2] [0] 600.61/155.55 600.61/155.55 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 600.61/155.55 [0 0] [0 0] [0] 600.61/155.55 600.61/155.55 [f^#](x1, x2) = [1 1] x1 + [0 0] x2 + [0] 600.61/155.55 [0 0] [0 4] [0] 600.61/155.55 600.61/155.55 [c_2](x1, x2, x3) = [2 0] x1 + [1 0] x3 + [0] 600.61/155.55 [0 0] [0 0] [0] 600.61/155.55 600.61/155.55 [g^#](x1) = [0] 600.61/155.55 [4] 600.61/155.55 600.61/155.55 [c_3](x1, x2) = [2 0] x1 + [1 0] x2 + [0] 600.61/155.55 [0 0] [0 0] [0] 600.61/155.55 600.61/155.55 [c_4](x1) = [1 0] x1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 600.61/155.55 [c_5](x1) = [1 0] x1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 600.61/155.55 [c_6](x1) = [2 0] x1 + [0] 600.61/155.55 [0 0] [3] 600.61/155.55 600.61/155.55 [c_7](x1) = [1 0] x1 + [0] 600.61/155.55 [0 0] [3] 600.61/155.55 600.61/155.55 [proper^#](x1) = [0] 600.61/155.55 [0] 600.61/155.55 600.61/155.55 [c_8](x1, x2, x3) = [4 0] x1 + [4 0] x2 + [2 0] x3 + [0] 600.61/155.55 [0 0] [0 0] [0 0] [0] 600.61/155.55 600.61/155.55 [c_9](x1, x2) = [2 0] x1 + [2 0] x2 + [0] 600.61/155.55 [0 0] [0 0] [0] 600.61/155.55 600.61/155.55 [top^#](x1) = [4 0] x1 + [0] 600.61/155.55 [0 0] [4] 600.61/155.55 600.61/155.55 [c_10](x1, x2) = [1 0] x1 + [4 0] x2 + [0] 600.61/155.55 [0 0] [0 0] [3] 600.61/155.55 600.61/155.55 [c_11](x1, x2) = [1 0] x1 + [2 0] x2 + [3] 600.61/155.55 [0 0] [0 0] [3] 600.61/155.55 600.61/155.55 The order satisfies the following ordering constraints: 600.61/155.55 600.61/155.55 [active(f(X1, X2))] = [0 0] X1 + [0] 600.61/155.55 [8 4] [0] 600.61/155.55 >= [0 0] X1 + [0] 600.61/155.55 [8 4] [0] 600.61/155.55 = [f(active(X1), X2)] 600.61/155.55 600.61/155.55 [active(f(g(X), Y))] = [0 0] X + [0] 600.61/155.55 [8 4] [0] 600.61/155.55 >= [0 0] X + [0] 600.61/155.55 [4 4] [0] 600.61/155.55 = [mark(f(X, f(g(X), Y)))] 600.61/155.55 600.61/155.55 [active(g(X))] = [0 0] X + [0] 600.61/155.55 [2 1] [0] 600.61/155.55 >= [0 0] X + [0] 600.61/155.55 [2 1] [0] 600.61/155.55 = [g(active(X))] 600.61/155.55 600.61/155.55 [f(mark(X1), X2)] = [0 0] X1 + [0] 600.61/155.55 [4 4] [0] 600.61/155.55 >= [0 0] X1 + [0] 600.61/155.55 [4 4] [0] 600.61/155.55 = [mark(f(X1, X2))] 600.61/155.55 600.61/155.55 [f(ok(X1), ok(X2))] = [4 4] X1 + [4] 600.61/155.55 [0 0] [0] 600.61/155.55 > [4 4] X1 + [1] 600.61/155.55 [0 0] [0] 600.61/155.55 = [ok(f(X1, X2))] 600.61/155.55 600.61/155.55 [g(mark(X))] = [0 0] X + [0] 600.61/155.55 [1 1] [0] 600.61/155.55 >= [0 0] X + [0] 600.61/155.55 [1 1] [0] 600.61/155.55 = [mark(g(X))] 600.61/155.55 600.61/155.55 [g(ok(X))] = [1 1] X + [1] 600.61/155.55 [0 0] [0] 600.61/155.55 >= [1 1] X + [1] 600.61/155.55 [0 0] [0] 600.61/155.55 = [ok(g(X))] 600.61/155.55 600.61/155.55 [proper(f(X1, X2))] = [0] 600.61/155.55 [0] 600.61/155.55 >= [0] 600.61/155.55 [0] 600.61/155.55 = [f(proper(X1), proper(X2))] 600.61/155.55 600.61/155.55 [proper(g(X))] = [0] 600.61/155.55 [0] 600.61/155.55 >= [0] 600.61/155.55 [0] 600.61/155.55 = [g(proper(X))] 600.61/155.55 600.61/155.55 [active^#(f(X1, X2))] = [4 8] X1 + [0] 600.61/155.55 [0 8] [0] 600.61/155.55 >= [3 3] X1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_1(f^#(active(X1), X2), active^#(X1))] 600.61/155.55 600.61/155.55 [active^#(f(g(X), Y))] = [4 8] X + [0] 600.61/155.55 [0 8] [0] 600.61/155.55 >= [2 2] X + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X))] 600.61/155.55 600.61/155.55 [active^#(g(X))] = [1 2] X + [0] 600.61/155.55 [0 2] [0] 600.61/155.55 >= [1 2] X + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_3(g^#(active(X)), active^#(X))] 600.61/155.55 600.61/155.55 [f^#(mark(X1), X2)] = [1 1] X1 + [0 0] X2 + [0] 600.61/155.55 [0 0] [0 4] [0] 600.61/155.55 >= [1 1] X1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_4(f^#(X1, X2))] 600.61/155.55 600.61/155.55 [f^#(ok(X1), ok(X2))] = [1 1] X1 + [1] 600.61/155.55 [0 0] [0] 600.61/155.55 > [1 1] X1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_5(f^#(X1, X2))] 600.61/155.55 600.61/155.55 [g^#(mark(X))] = [0] 600.61/155.55 [4] 600.61/155.55 >= [0] 600.61/155.55 [3] 600.61/155.55 = [c_6(g^#(X))] 600.61/155.55 600.61/155.55 [g^#(ok(X))] = [0] 600.61/155.55 [4] 600.61/155.55 >= [0] 600.61/155.55 [3] 600.61/155.55 = [c_7(g^#(X))] 600.61/155.55 600.61/155.55 [proper^#(f(X1, X2))] = [0] 600.61/155.55 [0] 600.61/155.55 >= [0] 600.61/155.55 [0] 600.61/155.55 = [c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2))] 600.61/155.55 600.61/155.55 [proper^#(g(X))] = [0] 600.61/155.55 [0] 600.61/155.55 >= [0] 600.61/155.55 [0] 600.61/155.55 = [c_9(g^#(proper(X)), proper^#(X))] 600.61/155.55 600.61/155.55 [top^#(mark(X))] = [0] 600.61/155.55 [4] 600.61/155.55 >= [0] 600.61/155.55 [3] 600.61/155.55 = [c_10(top^#(proper(X)), proper^#(X))] 600.61/155.55 600.61/155.55 [top^#(ok(X))] = [4 4] X + [4] 600.61/155.55 [0 0] [4] 600.61/155.55 > [2 4] X + [3] 600.61/155.55 [0 0] [3] 600.61/155.55 = [c_11(top^#(active(X)), active^#(X))] 600.61/155.55 600.61/155.55 600.61/155.55 The strictly oriented rules are moved into the weak component. 600.61/155.55 600.61/155.55 We are left with following problem, upon which TcT provides the 600.61/155.55 certificate YES(O(1),O(n^2)). 600.61/155.55 600.61/155.55 Strict DPs: 600.61/155.55 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.55 , active^#(f(g(X), Y)) -> 600.61/155.55 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.55 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.55 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.55 , g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.55 , g^#(ok(X)) -> c_7(g^#(X)) 600.61/155.55 , proper^#(f(X1, X2)) -> 600.61/155.55 c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.55 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) } 600.61/155.55 Weak DPs: 600.61/155.55 { f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.55 , top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.55 Weak Trs: 600.61/155.55 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.55 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.55 , active(g(X)) -> g(active(X)) 600.61/155.55 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.55 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.55 , g(mark(X)) -> mark(g(X)) 600.61/155.55 , g(ok(X)) -> ok(g(X)) 600.61/155.55 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.55 , proper(g(X)) -> g(proper(X)) } 600.61/155.55 Obligation: 600.61/155.55 innermost runtime complexity 600.61/155.55 Answer: 600.61/155.55 YES(O(1),O(n^2)) 600.61/155.55 600.61/155.55 We use the processor 'matrix interpretation of dimension 2' to 600.61/155.55 orient following rules strictly. 600.61/155.55 600.61/155.55 DPs: 600.61/155.55 { 6: g^#(ok(X)) -> c_7(g^#(X)) } 600.61/155.55 600.61/155.55 Sub-proof: 600.61/155.55 ---------- 600.61/155.55 The following argument positions are usable: 600.61/155.55 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 3}, Uargs(c_3) = {1, 2}, 600.61/155.55 Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 600.61/155.55 Uargs(c_7) = {1}, Uargs(c_8) = {1, 2, 3}, Uargs(c_9) = {1, 2}, 600.61/155.55 Uargs(c_10) = {1, 2}, Uargs(c_11) = {1, 2} 600.61/155.55 600.61/155.55 TcT has computed the following constructor-based matrix 600.61/155.55 interpretation satisfying not(EDA) and not(IDA(1)). 600.61/155.55 600.61/155.55 [active](x1) = [0 0] x1 + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 600.61/155.55 [f](x1, x2) = [2 0] x1 + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 600.61/155.55 [g](x1) = [2 0] x1 + [0] 600.61/155.55 [0 2] [0] 600.61/155.55 600.61/155.55 [mark](x1) = [0 0] x1 + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 600.61/155.55 [proper](x1) = [0] 600.61/155.55 [0] 600.61/155.55 600.61/155.55 [ok](x1) = [0 1] x1 + [0] 600.61/155.55 [0 1] [1] 600.61/155.55 600.61/155.55 [active^#](x1) = [0 1] x1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 600.61/155.55 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 600.61/155.55 [0 0] [0 0] [0] 600.61/155.55 600.61/155.55 [f^#](x1, x2) = [0] 600.61/155.55 [0] 600.61/155.55 600.61/155.55 [c_2](x1, x2, x3) = [2 0] x1 + [1 0] x3 + [0] 600.61/155.55 [0 0] [0 0] [0] 600.61/155.55 600.61/155.55 [g^#](x1) = [0 1] x1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 600.61/155.55 [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 600.61/155.55 [0 0] [0 0] [0] 600.61/155.55 600.61/155.55 [c_4](x1) = [4 0] x1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 600.61/155.55 [c_5](x1) = [1 0] x1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 600.61/155.55 [c_6](x1) = [1 0] x1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 600.61/155.55 [c_7](x1) = [1 0] x1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 600.61/155.55 [proper^#](x1) = [0 0] x1 + [0] 600.61/155.55 [0 4] [4] 600.61/155.55 600.61/155.55 [c_8](x1, x2, x3) = [1 0] x1 + [2 0] x2 + [4 0] x3 + [0] 600.61/155.55 [0 0] [0 0] [0 0] [3] 600.61/155.55 600.61/155.55 [c_9](x1, x2) = [1 0] x1 + [2 0] x2 + [0] 600.61/155.55 [0 0] [0 0] [3] 600.61/155.55 600.61/155.55 [top^#](x1) = [1 0] x1 + [0] 600.61/155.55 [7 1] [0] 600.61/155.55 600.61/155.55 [c_10](x1, x2) = [4 0] x1 + [1 0] x2 + [0] 600.61/155.55 [0 0] [0 0] [0] 600.61/155.55 600.61/155.55 [c_11](x1, x2) = [4 0] x1 + [1 0] x2 + [0] 600.61/155.55 [0 0] [0 0] [1] 600.61/155.55 600.61/155.55 The order satisfies the following ordering constraints: 600.61/155.55 600.61/155.55 [active(f(X1, X2))] = [0 0] X1 + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 >= [0 0] X1 + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 = [f(active(X1), X2)] 600.61/155.55 600.61/155.55 [active(f(g(X), Y))] = [0 0] X + [0] 600.61/155.55 [0 2] [0] 600.61/155.55 >= [0 0] X + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 = [mark(f(X, f(g(X), Y)))] 600.61/155.55 600.61/155.55 [active(g(X))] = [0 0] X + [0] 600.61/155.55 [0 2] [0] 600.61/155.55 >= [0 0] X + [0] 600.61/155.55 [0 2] [0] 600.61/155.55 = [g(active(X))] 600.61/155.55 600.61/155.55 [f(mark(X1), X2)] = [0 0] X1 + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 >= [0 0] X1 + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 = [mark(f(X1, X2))] 600.61/155.55 600.61/155.55 [f(ok(X1), ok(X2))] = [0 2] X1 + [0] 600.61/155.55 [0 1] [1] 600.61/155.55 >= [0 1] X1 + [0] 600.61/155.55 [0 1] [1] 600.61/155.55 = [ok(f(X1, X2))] 600.61/155.55 600.61/155.55 [g(mark(X))] = [0 0] X + [0] 600.61/155.55 [0 2] [0] 600.61/155.55 >= [0 0] X + [0] 600.61/155.55 [0 2] [0] 600.61/155.55 = [mark(g(X))] 600.61/155.55 600.61/155.55 [g(ok(X))] = [0 2] X + [0] 600.61/155.55 [0 2] [2] 600.61/155.55 >= [0 2] X + [0] 600.61/155.55 [0 2] [1] 600.61/155.55 = [ok(g(X))] 600.61/155.55 600.61/155.55 [proper(f(X1, X2))] = [0] 600.61/155.55 [0] 600.61/155.55 >= [0] 600.61/155.55 [0] 600.61/155.55 = [f(proper(X1), proper(X2))] 600.61/155.55 600.61/155.55 [proper(g(X))] = [0] 600.61/155.55 [0] 600.61/155.55 >= [0] 600.61/155.55 [0] 600.61/155.55 = [g(proper(X))] 600.61/155.55 600.61/155.55 [active^#(f(X1, X2))] = [0 1] X1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 >= [0 1] X1 + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_1(f^#(active(X1), X2), active^#(X1))] 600.61/155.55 600.61/155.55 [active^#(f(g(X), Y))] = [0 2] X + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 >= [0 1] X + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X))] 600.61/155.55 600.61/155.55 [active^#(g(X))] = [0 2] X + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 >= [0 2] X + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_3(g^#(active(X)), active^#(X))] 600.61/155.55 600.61/155.55 [f^#(mark(X1), X2)] = [0] 600.61/155.55 [0] 600.61/155.55 >= [0] 600.61/155.55 [0] 600.61/155.55 = [c_4(f^#(X1, X2))] 600.61/155.55 600.61/155.55 [f^#(ok(X1), ok(X2))] = [0] 600.61/155.55 [0] 600.61/155.55 >= [0] 600.61/155.55 [0] 600.61/155.55 = [c_5(f^#(X1, X2))] 600.61/155.55 600.61/155.55 [g^#(mark(X))] = [0 1] X + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 >= [0 1] X + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_6(g^#(X))] 600.61/155.55 600.61/155.55 [g^#(ok(X))] = [0 1] X + [1] 600.61/155.55 [0 0] [0] 600.61/155.55 > [0 1] X + [0] 600.61/155.55 [0 0] [0] 600.61/155.55 = [c_7(g^#(X))] 600.61/155.55 600.61/155.55 [proper^#(f(X1, X2))] = [0 0] X1 + [0] 600.61/155.55 [0 4] [4] 600.61/155.55 >= [0] 600.61/155.55 [3] 600.61/155.55 = [c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2))] 600.61/155.55 600.61/155.55 [proper^#(g(X))] = [0 0] X + [0] 600.61/155.55 [0 8] [4] 600.61/155.55 >= [0] 600.61/155.55 [3] 600.61/155.55 = [c_9(g^#(proper(X)), proper^#(X))] 600.61/155.55 600.61/155.55 [top^#(mark(X))] = [0 0] X + [0] 600.61/155.55 [0 1] [0] 600.61/155.55 >= [0] 600.61/155.55 [0] 600.61/155.55 = [c_10(top^#(proper(X)), proper^#(X))] 600.61/155.55 600.61/155.55 [top^#(ok(X))] = [0 1] X + [0] 600.61/155.55 [0 8] [1] 600.61/155.55 >= [0 1] X + [0] 600.61/155.55 [0 0] [1] 600.61/155.55 = [c_11(top^#(active(X)), active^#(X))] 600.61/155.55 600.61/155.55 600.61/155.55 The strictly oriented rules are moved into the weak component. 600.61/155.55 600.61/155.55 We are left with following problem, upon which TcT provides the 600.61/155.55 certificate YES(O(1),O(n^2)). 600.61/155.55 600.61/155.55 Strict DPs: 600.61/155.55 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.55 , active^#(f(g(X), Y)) -> 600.61/155.55 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.55 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.55 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.55 , g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.55 , proper^#(f(X1, X2)) -> 600.61/155.55 c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.55 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) } 600.61/155.55 Weak DPs: 600.61/155.55 { f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.55 , g^#(ok(X)) -> c_7(g^#(X)) 600.61/155.55 , top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.55 Weak Trs: 600.61/155.55 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.55 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.55 , active(g(X)) -> g(active(X)) 600.61/155.55 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.55 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.55 , g(mark(X)) -> mark(g(X)) 600.61/155.55 , g(ok(X)) -> ok(g(X)) 600.61/155.55 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.55 , proper(g(X)) -> g(proper(X)) } 600.61/155.55 Obligation: 600.61/155.55 innermost runtime complexity 600.61/155.55 Answer: 600.61/155.55 YES(O(1),O(n^2)) 600.61/155.55 600.61/155.55 We decompose the input problem according to the dependency graph 600.61/155.55 into the upper component 600.61/155.55 600.61/155.55 { top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.55 600.61/155.55 and lower component 600.61/155.55 600.61/155.55 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.55 , active^#(f(g(X), Y)) -> 600.61/155.55 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.55 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.55 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.55 , f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.55 , g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.55 , g^#(ok(X)) -> c_7(g^#(X)) 600.61/155.55 , proper^#(f(X1, X2)) -> 600.61/155.55 c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.55 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) } 600.61/155.55 600.61/155.55 Further, following extension rules are added to the lower 600.61/155.55 component. 600.61/155.55 600.61/155.55 { top^#(mark(X)) -> proper^#(X) 600.61/155.55 , top^#(mark(X)) -> top^#(proper(X)) 600.61/155.55 , top^#(ok(X)) -> active^#(X) 600.61/155.55 , top^#(ok(X)) -> top^#(active(X)) } 600.61/155.55 600.61/155.55 TcT solves the upper component with certificate YES(O(1),O(n^1)). 600.61/155.55 600.61/155.55 Sub-proof: 600.61/155.55 ---------- 600.61/155.55 We are left with following problem, upon which TcT provides the 600.61/155.55 certificate YES(O(1),O(n^1)). 600.61/155.55 600.61/155.55 Strict DPs: 600.61/155.55 { top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) 600.61/155.55 , top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.55 Weak Trs: 600.61/155.55 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.55 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.55 , active(g(X)) -> g(active(X)) 600.61/155.55 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.55 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.55 , g(mark(X)) -> mark(g(X)) 600.61/155.55 , g(ok(X)) -> ok(g(X)) 600.61/155.55 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.55 , proper(g(X)) -> g(proper(X)) } 600.61/155.55 Obligation: 600.61/155.55 innermost runtime complexity 600.61/155.55 Answer: 600.61/155.55 YES(O(1),O(n^1)) 600.61/155.55 600.61/155.55 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 600.61/155.55 to orient following rules strictly. 600.61/155.55 600.61/155.55 DPs: 600.61/155.55 { 1: top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) 600.61/155.55 , 2: top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.55 600.61/155.55 Sub-proof: 600.61/155.55 ---------- 600.61/155.55 The input was oriented with the instance of 'Small Polynomial Path 600.61/155.55 Order (PS,1-bounded)' as induced by the safe mapping 600.61/155.55 600.61/155.55 safe(active) = {}, safe(f) = {1, 2}, safe(g) = {1}, 600.61/155.55 safe(mark) = {1}, safe(proper) = {}, safe(ok) = {1}, 600.61/155.55 safe(active^#) = {}, safe(proper^#) = {}, safe(top^#) = {}, 600.61/155.55 safe(c_10) = {}, safe(c_11) = {} 600.61/155.55 600.61/155.56 and precedence 600.61/155.56 600.61/155.56 active ~ proper, active ~ top^#, proper ~ top^# . 600.61/155.56 600.61/155.56 Following symbols are considered recursive: 600.61/155.56 600.61/155.56 {active, top^#} 600.61/155.56 600.61/155.56 The recursion depth is 1. 600.61/155.56 600.61/155.56 Further, following argument filtering is employed: 600.61/155.56 600.61/155.56 pi(active) = 1, pi(f) = 1, pi(g) = [1], pi(mark) = [1], 600.61/155.56 pi(proper) = 1, pi(ok) = [1], pi(active^#) = [1], 600.61/155.56 pi(proper^#) = [1], pi(top^#) = [1], pi(c_10) = [1, 2], 600.61/155.56 pi(c_11) = [1, 2] 600.61/155.56 600.61/155.56 Usable defined function symbols are a subset of: 600.61/155.56 600.61/155.56 {active, f, g, proper, active^#, proper^#, top^#} 600.61/155.56 600.61/155.56 For your convenience, here are the satisfied ordering constraints: 600.61/155.56 600.61/155.56 pi(top^#(mark(X))) = top^#(mark(; X);) 600.61/155.56 > c_10(top^#(X;), proper^#(X;);) 600.61/155.56 = pi(c_10(top^#(proper(X)), proper^#(X))) 600.61/155.56 600.61/155.56 pi(top^#(ok(X))) = top^#(ok(; X);) 600.61/155.56 > c_11(top^#(X;), active^#(X;);) 600.61/155.56 = pi(c_11(top^#(active(X)), active^#(X))) 600.61/155.56 600.61/155.56 pi(active(f(X1, X2))) = X1 600.61/155.56 >= X1 600.61/155.56 = pi(f(active(X1), X2)) 600.61/155.56 600.61/155.56 pi(active(f(g(X), Y))) = g(; X) 600.61/155.56 >= mark(; X) 600.61/155.56 = pi(mark(f(X, f(g(X), Y)))) 600.61/155.56 600.61/155.56 pi(active(g(X))) = g(; X) 600.61/155.56 >= g(; X) 600.61/155.56 = pi(g(active(X))) 600.61/155.56 600.61/155.56 pi(f(mark(X1), X2)) = mark(; X1) 600.61/155.56 >= mark(; X1) 600.61/155.56 = pi(mark(f(X1, X2))) 600.61/155.56 600.61/155.56 pi(f(ok(X1), ok(X2))) = ok(; X1) 600.61/155.56 >= ok(; X1) 600.61/155.56 = pi(ok(f(X1, X2))) 600.61/155.56 600.61/155.56 pi(g(mark(X))) = g(; mark(; X)) 600.61/155.56 >= mark(; g(; X)) 600.61/155.56 = pi(mark(g(X))) 600.61/155.56 600.61/155.56 pi(g(ok(X))) = g(; ok(; X)) 600.61/155.56 >= ok(; g(; X)) 600.61/155.56 = pi(ok(g(X))) 600.61/155.56 600.61/155.56 pi(proper(f(X1, X2))) = X1 600.61/155.56 >= X1 600.61/155.56 = pi(f(proper(X1), proper(X2))) 600.61/155.56 600.61/155.56 pi(proper(g(X))) = g(; X) 600.61/155.56 >= g(; X) 600.61/155.56 = pi(g(proper(X))) 600.61/155.56 600.61/155.56 600.61/155.56 The strictly oriented rules are moved into the weak component. 600.61/155.56 600.61/155.56 We are left with following problem, upon which TcT provides the 600.61/155.56 certificate YES(O(1),O(1)). 600.61/155.56 600.61/155.56 Weak DPs: 600.61/155.56 { top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) 600.61/155.56 , top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.56 Weak Trs: 600.61/155.56 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.56 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.56 , active(g(X)) -> g(active(X)) 600.61/155.56 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.56 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.56 , g(mark(X)) -> mark(g(X)) 600.61/155.56 , g(ok(X)) -> ok(g(X)) 600.61/155.56 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.56 , proper(g(X)) -> g(proper(X)) } 600.61/155.56 Obligation: 600.61/155.56 innermost runtime complexity 600.61/155.56 Answer: 600.61/155.56 YES(O(1),O(1)) 600.61/155.56 600.61/155.56 The following weak DPs constitute a sub-graph of the DG that is 600.61/155.56 closed under successors. The DPs are removed. 600.61/155.56 600.61/155.56 { top^#(mark(X)) -> c_10(top^#(proper(X)), proper^#(X)) 600.61/155.56 , top^#(ok(X)) -> c_11(top^#(active(X)), active^#(X)) } 600.61/155.56 600.61/155.56 We are left with following problem, upon which TcT provides the 600.61/155.56 certificate YES(O(1),O(1)). 600.61/155.56 600.61/155.56 Weak Trs: 600.61/155.56 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.56 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.56 , active(g(X)) -> g(active(X)) 600.61/155.56 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.56 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.56 , g(mark(X)) -> mark(g(X)) 600.61/155.56 , g(ok(X)) -> ok(g(X)) 600.61/155.56 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.56 , proper(g(X)) -> g(proper(X)) } 600.61/155.56 Obligation: 600.61/155.56 innermost runtime complexity 600.61/155.56 Answer: 600.61/155.56 YES(O(1),O(1)) 600.61/155.56 600.61/155.56 No rule is usable, rules are removed from the input problem. 600.61/155.56 600.61/155.56 We are left with following problem, upon which TcT provides the 600.61/155.56 certificate YES(O(1),O(1)). 600.61/155.56 600.61/155.56 Rules: Empty 600.61/155.56 Obligation: 600.61/155.56 innermost runtime complexity 600.61/155.56 Answer: 600.61/155.56 YES(O(1),O(1)) 600.61/155.56 600.61/155.56 Empty rules are trivially bounded 600.61/155.56 600.61/155.56 We return to the main proof. 600.61/155.56 600.61/155.56 We are left with following problem, upon which TcT provides the 600.61/155.56 certificate YES(O(1),O(n^1)). 600.61/155.56 600.61/155.56 Strict DPs: 600.61/155.56 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.56 , active^#(f(g(X), Y)) -> 600.61/155.56 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.56 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.56 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.56 , g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.56 , proper^#(f(X1, X2)) -> 600.61/155.56 c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.56 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) } 600.61/155.56 Weak DPs: 600.61/155.56 { f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.56 , g^#(ok(X)) -> c_7(g^#(X)) 600.61/155.56 , top^#(mark(X)) -> proper^#(X) 600.61/155.56 , top^#(mark(X)) -> top^#(proper(X)) 600.61/155.56 , top^#(ok(X)) -> active^#(X) 600.61/155.56 , top^#(ok(X)) -> top^#(active(X)) } 600.61/155.56 Weak Trs: 600.61/155.56 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.56 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.56 , active(g(X)) -> g(active(X)) 600.61/155.56 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.56 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.56 , g(mark(X)) -> mark(g(X)) 600.61/155.56 , g(ok(X)) -> ok(g(X)) 600.61/155.56 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.56 , proper(g(X)) -> g(proper(X)) } 600.61/155.56 Obligation: 600.61/155.56 innermost runtime complexity 600.61/155.56 Answer: 600.61/155.56 YES(O(1),O(n^1)) 600.61/155.56 600.61/155.56 We use the processor 'matrix interpretation of dimension 2' to 600.61/155.56 orient following rules strictly. 600.61/155.56 600.61/155.56 DPs: 600.61/155.56 { 5: g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.56 , 9: g^#(ok(X)) -> c_7(g^#(X)) 600.61/155.56 , 10: top^#(mark(X)) -> proper^#(X) 600.61/155.56 , 11: top^#(mark(X)) -> top^#(proper(X)) 600.61/155.56 , 12: top^#(ok(X)) -> active^#(X) 600.61/155.56 , 13: top^#(ok(X)) -> top^#(active(X)) } 600.61/155.56 Trs: 600.61/155.56 { active(g(X)) -> g(active(X)) 600.61/155.56 , g(mark(X)) -> mark(g(X)) 600.61/155.56 , g(ok(X)) -> ok(g(X)) } 600.61/155.56 600.61/155.56 Sub-proof: 600.61/155.56 ---------- 600.61/155.56 The following argument positions are usable: 600.61/155.56 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 3}, Uargs(c_3) = {1, 2}, 600.61/155.56 Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 600.61/155.56 Uargs(c_7) = {1}, Uargs(c_8) = {1, 2, 3}, Uargs(c_9) = {1, 2} 600.61/155.56 600.61/155.56 TcT has computed the following constructor-based matrix 600.61/155.56 interpretation satisfying not(EDA) and not(IDA(1)). 600.61/155.56 600.61/155.56 [active](x1) = [1 1] x1 + [0] 600.61/155.56 [0 1] [0] 600.61/155.56 600.61/155.56 [f](x1, x2) = [1 0] x1 + [0] 600.61/155.56 [0 1] [0] 600.61/155.56 600.61/155.56 [g](x1) = [4 0] x1 + [0] 600.61/155.56 [0 4] [1] 600.61/155.56 600.61/155.56 [mark](x1) = [1 0] x1 + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [proper](x1) = [0 0] x1 + [0] 600.61/155.56 [0 2] [0] 600.61/155.56 600.61/155.56 [ok](x1) = [1 2] x1 + [1] 600.61/155.56 [0 0] [2] 600.61/155.56 600.61/155.56 [active^#](x1) = [2 1] x1 + [0] 600.61/155.56 [2 0] [0] 600.61/155.56 600.61/155.56 [c_1](x1, x2) = [2 0] x1 + [1 0] x2 + [0] 600.61/155.56 [0 0] [0 0] [0] 600.61/155.56 600.61/155.56 [f^#](x1, x2) = [0 0] x1 + [0] 600.61/155.56 [4 0] [4] 600.61/155.56 600.61/155.56 [c_2](x1, x2, x3) = [1 0] x1 + [1 0] x3 + [1] 600.61/155.56 [0 0] [0 0] [0] 600.61/155.56 600.61/155.56 [g^#](x1) = [2 0] x1 + [0] 600.61/155.56 [4 2] [0] 600.61/155.56 600.61/155.56 [c_3](x1, x2) = [1 0] x1 + [1 1] x2 + [1] 600.61/155.56 [0 0] [0 0] [0] 600.61/155.56 600.61/155.56 [c_4](x1) = [4 0] x1 + [0] 600.61/155.56 [0 0] [7] 600.61/155.56 600.61/155.56 [c_5](x1) = [2 0] x1 + [0] 600.61/155.56 [0 0] [3] 600.61/155.56 600.61/155.56 [c_6](x1) = [1 0] x1 + [1] 600.61/155.56 [0 0] [3] 600.61/155.56 600.61/155.56 [c_7](x1) = [1 0] x1 + [1] 600.61/155.56 [0 0] [7] 600.61/155.56 600.61/155.56 [proper^#](x1) = [0] 600.61/155.56 [4] 600.61/155.56 600.61/155.56 [c_8](x1, x2, x3) = [4 0] x1 + [4 0] x2 + [2 0] x3 + [0] 600.61/155.56 [0 0] [0 0] [0 0] [3] 600.61/155.56 600.61/155.56 [c_9](x1, x2) = [4 0] x1 + [2 0] x2 + [0] 600.61/155.56 [0 0] [0 0] [3] 600.61/155.56 600.61/155.56 [top^#](x1) = [2 0] x1 + [6] 600.61/155.56 [4 0] [4] 600.61/155.56 600.61/155.56 The order satisfies the following ordering constraints: 600.61/155.56 600.61/155.56 [active(f(X1, X2))] = [1 1] X1 + [0] 600.61/155.56 [0 1] [0] 600.61/155.56 >= [1 1] X1 + [0] 600.61/155.56 [0 1] [0] 600.61/155.56 = [f(active(X1), X2)] 600.61/155.56 600.61/155.56 [active(f(g(X), Y))] = [4 4] X + [1] 600.61/155.56 [0 4] [1] 600.61/155.56 >= [1 0] X + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 = [mark(f(X, f(g(X), Y)))] 600.61/155.56 600.61/155.56 [active(g(X))] = [4 4] X + [1] 600.61/155.56 [0 4] [1] 600.61/155.56 > [4 4] X + [0] 600.61/155.56 [0 4] [1] 600.61/155.56 = [g(active(X))] 600.61/155.56 600.61/155.56 [f(mark(X1), X2)] = [1 0] X1 + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 >= [1 0] X1 + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 = [mark(f(X1, X2))] 600.61/155.56 600.61/155.56 [f(ok(X1), ok(X2))] = [1 2] X1 + [1] 600.61/155.56 [0 0] [2] 600.61/155.56 >= [1 2] X1 + [1] 600.61/155.56 [0 0] [2] 600.61/155.56 = [ok(f(X1, X2))] 600.61/155.56 600.61/155.56 [g(mark(X))] = [4 0] X + [4] 600.61/155.56 [0 0] [1] 600.61/155.56 > [4 0] X + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 = [mark(g(X))] 600.61/155.56 600.61/155.56 [g(ok(X))] = [4 8] X + [4] 600.61/155.56 [0 0] [9] 600.61/155.56 > [4 8] X + [3] 600.61/155.56 [0 0] [2] 600.61/155.56 = [ok(g(X))] 600.61/155.56 600.61/155.56 [proper(f(X1, X2))] = [0 0] X1 + [0] 600.61/155.56 [0 2] [0] 600.61/155.56 >= [0 0] X1 + [0] 600.61/155.56 [0 2] [0] 600.61/155.56 = [f(proper(X1), proper(X2))] 600.61/155.56 600.61/155.56 [proper(g(X))] = [0 0] X + [0] 600.61/155.56 [0 8] [2] 600.61/155.56 >= [0 0] X + [0] 600.61/155.56 [0 8] [1] 600.61/155.56 = [g(proper(X))] 600.61/155.56 600.61/155.56 [active^#(f(X1, X2))] = [2 1] X1 + [0] 600.61/155.56 [2 0] [0] 600.61/155.56 >= [2 1] X1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 = [c_1(f^#(active(X1), X2), active^#(X1))] 600.61/155.56 600.61/155.56 [active^#(f(g(X), Y))] = [8 4] X + [1] 600.61/155.56 [8 0] [0] 600.61/155.56 >= [2 0] X + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 = [c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X))] 600.61/155.56 600.61/155.56 [active^#(g(X))] = [8 4] X + [1] 600.61/155.56 [8 0] [0] 600.61/155.56 >= [6 3] X + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 = [c_3(g^#(active(X)), active^#(X))] 600.61/155.56 600.61/155.56 [f^#(mark(X1), X2)] = [0 0] X1 + [0] 600.61/155.56 [4 0] [8] 600.61/155.56 >= [0] 600.61/155.56 [7] 600.61/155.56 = [c_4(f^#(X1, X2))] 600.61/155.56 600.61/155.56 [f^#(ok(X1), ok(X2))] = [0 0] X1 + [0] 600.61/155.56 [4 8] [8] 600.61/155.56 >= [0] 600.61/155.56 [3] 600.61/155.56 = [c_5(f^#(X1, X2))] 600.61/155.56 600.61/155.56 [g^#(mark(X))] = [2 0] X + [2] 600.61/155.56 [4 0] [4] 600.61/155.56 > [2 0] X + [1] 600.61/155.56 [0 0] [3] 600.61/155.56 = [c_6(g^#(X))] 600.61/155.56 600.61/155.56 [g^#(ok(X))] = [2 4] X + [2] 600.61/155.56 [4 8] [8] 600.61/155.56 > [2 0] X + [1] 600.61/155.56 [0 0] [7] 600.61/155.56 = [c_7(g^#(X))] 600.61/155.56 600.61/155.56 [proper^#(f(X1, X2))] = [0] 600.61/155.56 [4] 600.61/155.56 >= [0] 600.61/155.56 [3] 600.61/155.56 = [c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2))] 600.61/155.56 600.61/155.56 [proper^#(g(X))] = [0] 600.61/155.56 [4] 600.61/155.56 >= [0] 600.61/155.56 [3] 600.61/155.56 = [c_9(g^#(proper(X)), proper^#(X))] 600.61/155.56 600.61/155.56 [top^#(mark(X))] = [2 0] X + [8] 600.61/155.56 [4 0] [8] 600.61/155.56 > [0] 600.61/155.56 [4] 600.61/155.56 = [proper^#(X)] 600.61/155.56 600.61/155.56 [top^#(mark(X))] = [2 0] X + [8] 600.61/155.56 [4 0] [8] 600.61/155.56 > [6] 600.61/155.56 [4] 600.61/155.56 = [top^#(proper(X))] 600.61/155.56 600.61/155.56 [top^#(ok(X))] = [2 4] X + [8] 600.61/155.56 [4 8] [8] 600.61/155.56 > [2 1] X + [0] 600.61/155.56 [2 0] [0] 600.61/155.56 = [active^#(X)] 600.61/155.56 600.61/155.56 [top^#(ok(X))] = [2 4] X + [8] 600.61/155.56 [4 8] [8] 600.61/155.56 > [2 2] X + [6] 600.61/155.56 [4 4] [4] 600.61/155.56 = [top^#(active(X))] 600.61/155.56 600.61/155.56 600.61/155.56 The strictly oriented rules are moved into the weak component. 600.61/155.56 600.61/155.56 We are left with following problem, upon which TcT provides the 600.61/155.56 certificate YES(O(1),O(n^1)). 600.61/155.56 600.61/155.56 Strict DPs: 600.61/155.56 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.56 , active^#(f(g(X), Y)) -> 600.61/155.56 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.56 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.56 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.56 , proper^#(f(X1, X2)) -> 600.61/155.56 c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.56 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) } 600.61/155.56 Weak DPs: 600.61/155.56 { f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.56 , g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.56 , g^#(ok(X)) -> c_7(g^#(X)) 600.61/155.56 , top^#(mark(X)) -> proper^#(X) 600.61/155.56 , top^#(mark(X)) -> top^#(proper(X)) 600.61/155.56 , top^#(ok(X)) -> active^#(X) 600.61/155.56 , top^#(ok(X)) -> top^#(active(X)) } 600.61/155.56 Weak Trs: 600.61/155.56 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.56 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.56 , active(g(X)) -> g(active(X)) 600.61/155.56 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.56 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.56 , g(mark(X)) -> mark(g(X)) 600.61/155.56 , g(ok(X)) -> ok(g(X)) 600.61/155.56 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.56 , proper(g(X)) -> g(proper(X)) } 600.61/155.56 Obligation: 600.61/155.56 innermost runtime complexity 600.61/155.56 Answer: 600.61/155.56 YES(O(1),O(n^1)) 600.61/155.56 600.61/155.56 The following weak DPs constitute a sub-graph of the DG that is 600.61/155.56 closed under successors. The DPs are removed. 600.61/155.56 600.61/155.56 { g^#(mark(X)) -> c_6(g^#(X)) 600.61/155.56 , g^#(ok(X)) -> c_7(g^#(X)) } 600.61/155.56 600.61/155.56 We are left with following problem, upon which TcT provides the 600.61/155.56 certificate YES(O(1),O(n^1)). 600.61/155.56 600.61/155.56 Strict DPs: 600.61/155.56 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.56 , active^#(f(g(X), Y)) -> 600.61/155.56 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.56 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.56 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.56 , proper^#(f(X1, X2)) -> 600.61/155.56 c_8(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.56 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) } 600.61/155.56 Weak DPs: 600.61/155.56 { f^#(ok(X1), ok(X2)) -> c_5(f^#(X1, X2)) 600.61/155.56 , top^#(mark(X)) -> proper^#(X) 600.61/155.56 , top^#(mark(X)) -> top^#(proper(X)) 600.61/155.56 , top^#(ok(X)) -> active^#(X) 600.61/155.56 , top^#(ok(X)) -> top^#(active(X)) } 600.61/155.56 Weak Trs: 600.61/155.56 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.56 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.56 , active(g(X)) -> g(active(X)) 600.61/155.56 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.56 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.56 , g(mark(X)) -> mark(g(X)) 600.61/155.56 , g(ok(X)) -> ok(g(X)) 600.61/155.56 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.56 , proper(g(X)) -> g(proper(X)) } 600.61/155.56 Obligation: 600.61/155.56 innermost runtime complexity 600.61/155.56 Answer: 600.61/155.56 YES(O(1),O(n^1)) 600.61/155.56 600.61/155.56 Due to missing edges in the dependency-graph, the right-hand sides 600.61/155.56 of following rules could be simplified: 600.61/155.56 600.61/155.56 { active^#(f(g(X), Y)) -> 600.61/155.56 c_2(f^#(X, f(g(X), Y)), f^#(g(X), Y), g^#(X)) 600.61/155.56 , active^#(g(X)) -> c_3(g^#(active(X)), active^#(X)) 600.61/155.56 , proper^#(g(X)) -> c_9(g^#(proper(X)), proper^#(X)) } 600.61/155.56 600.61/155.56 We are left with following problem, upon which TcT provides the 600.61/155.56 certificate YES(O(1),O(n^1)). 600.61/155.56 600.61/155.56 Strict DPs: 600.61/155.56 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.56 , active^#(f(g(X), Y)) -> c_2(f^#(g(X), Y)) 600.61/155.56 , active^#(g(X)) -> c_3(active^#(X)) 600.61/155.56 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.56 , proper^#(f(X1, X2)) -> 600.61/155.56 c_5(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.56 , proper^#(g(X)) -> c_6(proper^#(X)) } 600.61/155.56 Weak DPs: 600.61/155.56 { f^#(ok(X1), ok(X2)) -> c_7(f^#(X1, X2)) 600.61/155.56 , top^#(mark(X)) -> c_8(proper^#(X)) 600.61/155.56 , top^#(mark(X)) -> c_9(top^#(proper(X))) 600.61/155.56 , top^#(ok(X)) -> c_10(active^#(X)) 600.61/155.56 , top^#(ok(X)) -> c_11(top^#(active(X))) } 600.61/155.56 Weak Trs: 600.61/155.56 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.56 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.56 , active(g(X)) -> g(active(X)) 600.61/155.56 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.56 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.56 , g(mark(X)) -> mark(g(X)) 600.61/155.56 , g(ok(X)) -> ok(g(X)) 600.61/155.56 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.56 , proper(g(X)) -> g(proper(X)) } 600.61/155.56 Obligation: 600.61/155.56 innermost runtime complexity 600.61/155.56 Answer: 600.61/155.56 YES(O(1),O(n^1)) 600.61/155.56 600.61/155.56 We use the processor 'matrix interpretation of dimension 2' to 600.61/155.56 orient following rules strictly. 600.61/155.56 600.61/155.56 DPs: 600.61/155.56 { 2: active^#(f(g(X), Y)) -> c_2(f^#(g(X), Y)) 600.61/155.56 , 3: active^#(g(X)) -> c_3(active^#(X)) 600.61/155.56 , 4: f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.56 , 7: f^#(ok(X1), ok(X2)) -> c_7(f^#(X1, X2)) 600.61/155.56 , 10: top^#(ok(X)) -> c_10(active^#(X)) 600.61/155.56 , 11: top^#(ok(X)) -> c_11(top^#(active(X))) } 600.61/155.56 Trs: 600.61/155.56 { active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.56 , active(g(X)) -> g(active(X)) 600.61/155.56 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.56 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.56 , g(mark(X)) -> mark(g(X)) 600.61/155.56 , g(ok(X)) -> ok(g(X)) } 600.61/155.56 600.61/155.56 Sub-proof: 600.61/155.56 ---------- 600.61/155.56 The following argument positions are usable: 600.61/155.56 Uargs(c_1) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 600.61/155.56 Uargs(c_5) = {1, 2, 3}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, 600.61/155.56 Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1}, 600.61/155.56 Uargs(c_11) = {1} 600.61/155.56 600.61/155.56 TcT has computed the following constructor-based matrix 600.61/155.56 interpretation satisfying not(EDA) and not(IDA(1)). 600.61/155.56 600.61/155.56 [active](x1) = [1 1] x1 + [0] 600.61/155.56 [0 2] [0] 600.61/155.56 600.61/155.56 [f](x1, x2) = [2 0] x1 + [0] 600.61/155.56 [0 2] [0] 600.61/155.56 600.61/155.56 [g](x1) = [2 0] x1 + [0] 600.61/155.56 [0 2] [2] 600.61/155.56 600.61/155.56 [mark](x1) = [1 0] x1 + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [proper](x1) = [0 0] x1 + [0] 600.61/155.56 [0 1] [0] 600.61/155.56 600.61/155.56 [ok](x1) = [1 1] x1 + [4] 600.61/155.56 [0 0] [4] 600.61/155.56 600.61/155.56 [active^#](x1) = [1 2] x1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_1](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.56 [0 0] [0 0] [0] 600.61/155.56 600.61/155.56 [f^#](x1, x2) = [1 0] x1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_2](x1, x2, x3) = [7 7] x1 + [7 7] x2 + [7 7] x3 + [0] 600.61/155.56 [0 0] [0 0] [0 0] [0] 600.61/155.56 600.61/155.56 [g^#](x1) = [7 7] x1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_3](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.56 [0 0] [0 0] [0] 600.61/155.56 600.61/155.56 [c_4](x1) = [7 7] x1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_5](x1) = [7 7] x1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_6](x1) = [7 7] x1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_7](x1) = [7 7] x1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [proper^#](x1) = [0 0] x1 + [0] 600.61/155.56 [4 0] [4] 600.61/155.56 600.61/155.56 [c_8](x1, x2, x3) = [7 7] x1 + [7 7] x2 + [7 7] x3 + [0] 600.61/155.56 [0 0] [0 0] [0 0] [0] 600.61/155.56 600.61/155.56 [c_9](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.56 [0 0] [0 0] [0] 600.61/155.56 600.61/155.56 [top^#](x1) = [2 0] x1 + [0] 600.61/155.56 [0 2] [0] 600.61/155.56 600.61/155.56 [c] = [0] 600.61/155.56 [0] 600.61/155.56 600.61/155.56 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 600.61/155.56 [0 0] [0 0] [0] 600.61/155.56 600.61/155.56 [c_2](x1) = [3] 600.61/155.56 [0] 600.61/155.56 600.61/155.56 [c_3](x1) = [1 0] x1 + [3] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_4](x1) = [1 0] x1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_5](x1, x2, x3) = [2 0] x1 + [2 0] x2 + [2 0] x3 + [0] 600.61/155.56 [0 0] [0 0] [0 0] [3] 600.61/155.56 600.61/155.56 [c_6](x1) = [4 0] x1 + [0] 600.61/155.56 [0 0] [3] 600.61/155.56 600.61/155.56 [c_7](x1) = [1 0] x1 + [3] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_8](x1) = [2 0] x1 + [2] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_9](x1) = [4 0] x1 + [2] 600.61/155.56 [0 0] [0] 600.61/155.56 600.61/155.56 [c_10](x1) = [1 0] x1 + [7] 600.61/155.56 [0 0] [7] 600.61/155.56 600.61/155.56 [c_11](x1) = [1 0] x1 + [7] 600.61/155.56 [0 0] [7] 600.61/155.56 600.61/155.56 The order satisfies the following ordering constraints: 600.61/155.56 600.61/155.56 [active(f(X1, X2))] = [2 2] X1 + [0] 600.61/155.56 [0 4] [0] 600.61/155.56 >= [2 2] X1 + [0] 600.61/155.56 [0 4] [0] 600.61/155.56 = [f(active(X1), X2)] 600.61/155.56 600.61/155.56 [active(f(g(X), Y))] = [4 4] X + [4] 600.61/155.56 [0 8] [8] 600.61/155.56 > [2 0] X + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 = [mark(f(X, f(g(X), Y)))] 600.61/155.56 600.61/155.56 [active(g(X))] = [2 2] X + [2] 600.61/155.56 [0 4] [4] 600.61/155.56 > [2 2] X + [0] 600.61/155.56 [0 4] [2] 600.61/155.56 = [g(active(X))] 600.61/155.56 600.61/155.56 [f(mark(X1), X2)] = [2 0] X1 + [2] 600.61/155.56 [0 0] [0] 600.61/155.56 > [2 0] X1 + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 = [mark(f(X1, X2))] 600.61/155.56 600.61/155.56 [f(ok(X1), ok(X2))] = [2 2] X1 + [8] 600.61/155.56 [0 0] [8] 600.61/155.56 > [2 2] X1 + [4] 600.61/155.56 [0 0] [4] 600.61/155.56 = [ok(f(X1, X2))] 600.61/155.56 600.61/155.56 [g(mark(X))] = [2 0] X + [2] 600.61/155.56 [0 0] [2] 600.61/155.56 > [2 0] X + [1] 600.61/155.56 [0 0] [0] 600.61/155.56 = [mark(g(X))] 600.61/155.56 600.61/155.56 [g(ok(X))] = [2 2] X + [8] 600.61/155.56 [0 0] [10] 600.61/155.56 > [2 2] X + [6] 600.61/155.56 [0 0] [4] 600.61/155.56 = [ok(g(X))] 600.61/155.56 600.61/155.56 [proper(f(X1, X2))] = [0 0] X1 + [0] 600.61/155.56 [0 2] [0] 600.61/155.56 >= [0 0] X1 + [0] 600.61/155.56 [0 2] [0] 600.61/155.56 = [f(proper(X1), proper(X2))] 600.61/155.56 600.61/155.56 [proper(g(X))] = [0 0] X + [0] 600.61/155.56 [0 2] [2] 600.61/155.56 >= [0 0] X + [0] 600.61/155.56 [0 2] [2] 600.61/155.56 = [g(proper(X))] 600.61/155.56 600.61/155.56 [active^#(f(X1, X2))] = [2 4] X1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 >= [2 3] X1 + [0] 600.61/155.56 [0 0] [0] 600.61/155.56 = [c_1(f^#(active(X1), X2), active^#(X1))] 600.61/155.56 600.61/155.56 [active^#(f(g(X), Y))] = [4 8] X + [8] 600.61/155.56 [0 0] [0] 600.61/155.56 > [3] 600.61/155.56 [0] 600.61/155.56 = [c_2(f^#(g(X), Y))] 600.61/155.56 600.61/155.57 [active^#(g(X))] = [2 4] X + [4] 600.61/155.57 [0 0] [0] 600.61/155.57 > [1 2] X + [3] 600.61/155.57 [0 0] [0] 600.61/155.57 = [c_3(active^#(X))] 600.61/155.57 600.61/155.57 [f^#(mark(X1), X2)] = [1 0] X1 + [1] 600.61/155.57 [0 0] [0] 600.61/155.57 > [1 0] X1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 = [c_4(f^#(X1, X2))] 600.61/155.57 600.61/155.57 [f^#(ok(X1), ok(X2))] = [1 1] X1 + [4] 600.61/155.57 [0 0] [0] 600.61/155.57 > [1 0] X1 + [3] 600.61/155.57 [0 0] [0] 600.61/155.57 = [c_7(f^#(X1, X2))] 600.61/155.57 600.61/155.57 [proper^#(f(X1, X2))] = [0 0] X1 + [0] 600.61/155.57 [8 0] [4] 600.61/155.57 >= [0] 600.61/155.57 [3] 600.61/155.57 = [c_5(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2))] 600.61/155.57 600.61/155.57 [proper^#(g(X))] = [0 0] X + [0] 600.61/155.57 [8 0] [4] 600.61/155.57 >= [0] 600.61/155.57 [3] 600.61/155.57 = [c_6(proper^#(X))] 600.61/155.57 600.61/155.57 [top^#(mark(X))] = [2 0] X + [2] 600.61/155.57 [0 0] [0] 600.61/155.57 >= [2] 600.61/155.57 [0] 600.61/155.57 = [c_8(proper^#(X))] 600.61/155.57 600.61/155.57 [top^#(mark(X))] = [2 0] X + [2] 600.61/155.57 [0 0] [0] 600.61/155.57 >= [2] 600.61/155.57 [0] 600.61/155.57 = [c_9(top^#(proper(X)))] 600.61/155.57 600.61/155.57 [top^#(ok(X))] = [2 2] X + [8] 600.61/155.57 [0 0] [8] 600.61/155.57 > [1 2] X + [7] 600.61/155.57 [0 0] [7] 600.61/155.57 = [c_10(active^#(X))] 600.61/155.57 600.61/155.57 [top^#(ok(X))] = [2 2] X + [8] 600.61/155.57 [0 0] [8] 600.61/155.57 > [2 2] X + [7] 600.61/155.57 [0 0] [7] 600.61/155.57 = [c_11(top^#(active(X)))] 600.61/155.57 600.61/155.57 600.61/155.57 The strictly oriented rules are moved into the weak component. 600.61/155.57 600.61/155.57 We are left with following problem, upon which TcT provides the 600.61/155.57 certificate YES(O(1),O(n^1)). 600.61/155.57 600.61/155.57 Strict DPs: 600.61/155.57 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.57 , proper^#(f(X1, X2)) -> 600.61/155.57 c_5(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.57 , proper^#(g(X)) -> c_6(proper^#(X)) } 600.61/155.57 Weak DPs: 600.61/155.57 { active^#(f(g(X), Y)) -> c_2(f^#(g(X), Y)) 600.61/155.57 , active^#(g(X)) -> c_3(active^#(X)) 600.61/155.57 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.57 , f^#(ok(X1), ok(X2)) -> c_7(f^#(X1, X2)) 600.61/155.57 , top^#(mark(X)) -> c_8(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_9(top^#(proper(X))) 600.61/155.57 , top^#(ok(X)) -> c_10(active^#(X)) 600.61/155.57 , top^#(ok(X)) -> c_11(top^#(active(X))) } 600.61/155.57 Weak Trs: 600.61/155.57 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.57 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.57 , active(g(X)) -> g(active(X)) 600.61/155.57 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.57 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.57 , g(mark(X)) -> mark(g(X)) 600.61/155.57 , g(ok(X)) -> ok(g(X)) 600.61/155.57 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.57 , proper(g(X)) -> g(proper(X)) } 600.61/155.57 Obligation: 600.61/155.57 innermost runtime complexity 600.61/155.57 Answer: 600.61/155.57 YES(O(1),O(n^1)) 600.61/155.57 600.61/155.57 The following weak DPs constitute a sub-graph of the DG that is 600.61/155.57 closed under successors. The DPs are removed. 600.61/155.57 600.61/155.57 { active^#(f(g(X), Y)) -> c_2(f^#(g(X), Y)) 600.61/155.57 , f^#(mark(X1), X2) -> c_4(f^#(X1, X2)) 600.61/155.57 , f^#(ok(X1), ok(X2)) -> c_7(f^#(X1, X2)) } 600.61/155.57 600.61/155.57 We are left with following problem, upon which TcT provides the 600.61/155.57 certificate YES(O(1),O(n^1)). 600.61/155.57 600.61/155.57 Strict DPs: 600.61/155.57 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.57 , proper^#(f(X1, X2)) -> 600.61/155.57 c_5(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) 600.61/155.57 , proper^#(g(X)) -> c_6(proper^#(X)) } 600.61/155.57 Weak DPs: 600.61/155.57 { active^#(g(X)) -> c_3(active^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_8(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_9(top^#(proper(X))) 600.61/155.57 , top^#(ok(X)) -> c_10(active^#(X)) 600.61/155.57 , top^#(ok(X)) -> c_11(top^#(active(X))) } 600.61/155.57 Weak Trs: 600.61/155.57 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.57 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.57 , active(g(X)) -> g(active(X)) 600.61/155.57 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.57 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.57 , g(mark(X)) -> mark(g(X)) 600.61/155.57 , g(ok(X)) -> ok(g(X)) 600.61/155.57 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.57 , proper(g(X)) -> g(proper(X)) } 600.61/155.57 Obligation: 600.61/155.57 innermost runtime complexity 600.61/155.57 Answer: 600.61/155.57 YES(O(1),O(n^1)) 600.61/155.57 600.61/155.57 Due to missing edges in the dependency-graph, the right-hand sides 600.61/155.57 of following rules could be simplified: 600.61/155.57 600.61/155.57 { active^#(f(X1, X2)) -> c_1(f^#(active(X1), X2), active^#(X1)) 600.61/155.57 , proper^#(f(X1, X2)) -> 600.61/155.57 c_5(f^#(proper(X1), proper(X2)), proper^#(X1), proper^#(X2)) } 600.61/155.57 600.61/155.57 We are left with following problem, upon which TcT provides the 600.61/155.57 certificate YES(O(1),O(n^1)). 600.61/155.57 600.61/155.57 Strict DPs: 600.61/155.57 { active^#(f(X1, X2)) -> c_1(active^#(X1)) 600.61/155.57 , proper^#(f(X1, X2)) -> c_2(proper^#(X1), proper^#(X2)) 600.61/155.57 , proper^#(g(X)) -> c_3(proper^#(X)) } 600.61/155.57 Weak DPs: 600.61/155.57 { active^#(g(X)) -> c_4(active^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_5(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_6(top^#(proper(X))) 600.61/155.57 , top^#(ok(X)) -> c_7(active^#(X)) 600.61/155.57 , top^#(ok(X)) -> c_8(top^#(active(X))) } 600.61/155.57 Weak Trs: 600.61/155.57 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.57 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.57 , active(g(X)) -> g(active(X)) 600.61/155.57 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.57 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.57 , g(mark(X)) -> mark(g(X)) 600.61/155.57 , g(ok(X)) -> ok(g(X)) 600.61/155.57 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.57 , proper(g(X)) -> g(proper(X)) } 600.61/155.57 Obligation: 600.61/155.57 innermost runtime complexity 600.61/155.57 Answer: 600.61/155.57 YES(O(1),O(n^1)) 600.61/155.57 600.61/155.57 We use the processor 'matrix interpretation of dimension 1' to 600.61/155.57 orient following rules strictly. 600.61/155.57 600.61/155.57 DPs: 600.61/155.57 { 1: active^#(f(X1, X2)) -> c_1(active^#(X1)) 600.61/155.57 , 5: top^#(mark(X)) -> c_5(proper^#(X)) } 600.61/155.57 Trs: { active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) } 600.61/155.57 600.61/155.57 Sub-proof: 600.61/155.57 ---------- 600.61/155.57 The following argument positions are usable: 600.61/155.57 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 600.61/155.57 Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 600.61/155.57 Uargs(c_7) = {1}, Uargs(c_8) = {1} 600.61/155.57 600.61/155.57 TcT has computed the following constructor-based matrix 600.61/155.57 interpretation satisfying not(EDA). 600.61/155.57 600.61/155.57 [active](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 [f](x1, x2) = [1] x1 + [1] 600.61/155.57 600.61/155.57 [g](x1) = [2] x1 + [1] 600.61/155.57 600.61/155.57 [mark](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 [proper](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 [ok](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 [active^#](x1) = [1] x1 + [1] 600.61/155.57 600.61/155.57 [c_1](x1, x2) = [7] x1 + [7] x2 + [0] 600.61/155.57 600.61/155.57 [f^#](x1, x2) = [7] x1 + [7] x2 + [0] 600.61/155.57 600.61/155.57 [c_2](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 600.61/155.57 600.61/155.57 [g^#](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_3](x1, x2) = [7] x1 + [7] x2 + [0] 600.61/155.57 600.61/155.57 [c_4](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_5](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_6](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_7](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [proper^#](x1) = [0] 600.61/155.57 600.61/155.57 [c_8](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 600.61/155.57 600.61/155.57 [c_9](x1, x2) = [7] x1 + [7] x2 + [0] 600.61/155.57 600.61/155.57 [top^#](x1) = [1] x1 + [1] 600.61/155.57 600.61/155.57 [c] = [0] 600.61/155.57 600.61/155.57 [c_1](x1, x2) = [7] x1 + [7] x2 + [0] 600.61/155.57 600.61/155.57 [c_2](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_3](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_4](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_5](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 600.61/155.57 600.61/155.57 [c_6](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_7](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_8](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_9](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_10](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c_11](x1) = [7] x1 + [0] 600.61/155.57 600.61/155.57 [c] = [0] 600.61/155.57 600.61/155.57 [c_1](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 [c_2](x1, x2) = [1] x1 + [2] x2 + [0] 600.61/155.57 600.61/155.57 [c_3](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 [c_4](x1) = [2] x1 + [0] 600.61/155.57 600.61/155.57 [c_5](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 [c_6](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 [c_7](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 [c_8](x1) = [1] x1 + [0] 600.61/155.57 600.61/155.57 The order satisfies the following ordering constraints: 600.61/155.57 600.61/155.57 [active(f(X1, X2))] = [1] X1 + [1] 600.61/155.57 >= [1] X1 + [1] 600.61/155.57 = [f(active(X1), X2)] 600.61/155.57 600.61/155.57 [active(f(g(X), Y))] = [2] X + [2] 600.61/155.57 > [1] X + [1] 600.61/155.57 = [mark(f(X, f(g(X), Y)))] 600.61/155.57 600.61/155.57 [active(g(X))] = [2] X + [1] 600.61/155.57 >= [2] X + [1] 600.61/155.57 = [g(active(X))] 600.61/155.57 600.61/155.57 [f(mark(X1), X2)] = [1] X1 + [1] 600.61/155.57 >= [1] X1 + [1] 600.61/155.57 = [mark(f(X1, X2))] 600.61/155.57 600.61/155.57 [f(ok(X1), ok(X2))] = [1] X1 + [1] 600.61/155.57 >= [1] X1 + [1] 600.61/155.57 = [ok(f(X1, X2))] 600.61/155.57 600.61/155.57 [g(mark(X))] = [2] X + [1] 600.61/155.57 >= [2] X + [1] 600.61/155.57 = [mark(g(X))] 600.61/155.57 600.61/155.57 [g(ok(X))] = [2] X + [1] 600.61/155.57 >= [2] X + [1] 600.61/155.57 = [ok(g(X))] 600.61/155.57 600.61/155.57 [proper(f(X1, X2))] = [1] X1 + [1] 600.61/155.57 >= [1] X1 + [1] 600.61/155.57 = [f(proper(X1), proper(X2))] 600.61/155.57 600.61/155.57 [proper(g(X))] = [2] X + [1] 600.61/155.57 >= [2] X + [1] 600.61/155.57 = [g(proper(X))] 600.61/155.57 600.61/155.57 [active^#(f(X1, X2))] = [1] X1 + [2] 600.61/155.57 > [1] X1 + [1] 600.61/155.57 = [c_1(active^#(X1))] 600.61/155.57 600.61/155.57 [active^#(g(X))] = [2] X + [2] 600.61/155.57 >= [2] X + [2] 600.61/155.57 = [c_4(active^#(X))] 600.61/155.57 600.61/155.57 [proper^#(f(X1, X2))] = [0] 600.61/155.57 >= [0] 600.61/155.57 = [c_2(proper^#(X1), proper^#(X2))] 600.61/155.57 600.61/155.57 [proper^#(g(X))] = [0] 600.61/155.57 >= [0] 600.61/155.57 = [c_3(proper^#(X))] 600.61/155.57 600.61/155.57 [top^#(mark(X))] = [1] X + [1] 600.61/155.57 > [0] 600.61/155.57 = [c_5(proper^#(X))] 600.61/155.57 600.61/155.57 [top^#(mark(X))] = [1] X + [1] 600.61/155.57 >= [1] X + [1] 600.61/155.57 = [c_6(top^#(proper(X)))] 600.61/155.57 600.61/155.57 [top^#(ok(X))] = [1] X + [1] 600.61/155.57 >= [1] X + [1] 600.61/155.57 = [c_7(active^#(X))] 600.61/155.57 600.61/155.57 [top^#(ok(X))] = [1] X + [1] 600.61/155.57 >= [1] X + [1] 600.61/155.57 = [c_8(top^#(active(X)))] 600.61/155.57 600.61/155.57 600.61/155.57 The strictly oriented rules are moved into the weak component. 600.61/155.57 600.61/155.57 We are left with following problem, upon which TcT provides the 600.61/155.57 certificate YES(O(1),O(n^1)). 600.61/155.57 600.61/155.57 Strict DPs: 600.61/155.57 { proper^#(f(X1, X2)) -> c_2(proper^#(X1), proper^#(X2)) 600.61/155.57 , proper^#(g(X)) -> c_3(proper^#(X)) } 600.61/155.57 Weak DPs: 600.61/155.57 { active^#(f(X1, X2)) -> c_1(active^#(X1)) 600.61/155.57 , active^#(g(X)) -> c_4(active^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_5(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_6(top^#(proper(X))) 600.61/155.57 , top^#(ok(X)) -> c_7(active^#(X)) 600.61/155.57 , top^#(ok(X)) -> c_8(top^#(active(X))) } 600.61/155.57 Weak Trs: 600.61/155.57 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.57 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.57 , active(g(X)) -> g(active(X)) 600.61/155.57 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.57 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.57 , g(mark(X)) -> mark(g(X)) 600.61/155.57 , g(ok(X)) -> ok(g(X)) 600.61/155.57 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.57 , proper(g(X)) -> g(proper(X)) } 600.61/155.57 Obligation: 600.61/155.57 innermost runtime complexity 600.61/155.57 Answer: 600.61/155.57 YES(O(1),O(n^1)) 600.61/155.57 600.61/155.57 The following weak DPs constitute a sub-graph of the DG that is 600.61/155.57 closed under successors. The DPs are removed. 600.61/155.57 600.61/155.57 { active^#(f(X1, X2)) -> c_1(active^#(X1)) 600.61/155.57 , active^#(g(X)) -> c_4(active^#(X)) 600.61/155.57 , top^#(ok(X)) -> c_7(active^#(X)) } 600.61/155.57 600.61/155.57 We are left with following problem, upon which TcT provides the 600.61/155.57 certificate YES(O(1),O(n^1)). 600.61/155.57 600.61/155.57 Strict DPs: 600.61/155.57 { proper^#(f(X1, X2)) -> c_2(proper^#(X1), proper^#(X2)) 600.61/155.57 , proper^#(g(X)) -> c_3(proper^#(X)) } 600.61/155.57 Weak DPs: 600.61/155.57 { top^#(mark(X)) -> c_5(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_6(top^#(proper(X))) 600.61/155.57 , top^#(ok(X)) -> c_8(top^#(active(X))) } 600.61/155.57 Weak Trs: 600.61/155.57 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.57 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.57 , active(g(X)) -> g(active(X)) 600.61/155.57 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.57 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.57 , g(mark(X)) -> mark(g(X)) 600.61/155.57 , g(ok(X)) -> ok(g(X)) 600.61/155.57 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.57 , proper(g(X)) -> g(proper(X)) } 600.61/155.57 Obligation: 600.61/155.57 innermost runtime complexity 600.61/155.57 Answer: 600.61/155.57 YES(O(1),O(n^1)) 600.61/155.57 600.61/155.57 We use the processor 'matrix interpretation of dimension 2' to 600.61/155.57 orient following rules strictly. 600.61/155.57 600.61/155.57 DPs: 600.61/155.57 { 2: proper^#(g(X)) -> c_3(proper^#(X)) 600.61/155.57 , 5: top^#(ok(X)) -> c_8(top^#(active(X))) } 600.61/155.57 Trs: 600.61/155.57 { f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.57 , g(ok(X)) -> ok(g(X)) } 600.61/155.57 600.61/155.57 Sub-proof: 600.61/155.57 ---------- 600.61/155.57 The following argument positions are usable: 600.61/155.57 Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_5) = {1}, 600.61/155.57 Uargs(c_6) = {1}, Uargs(c_8) = {1} 600.61/155.57 600.61/155.57 TcT has computed the following constructor-based matrix 600.61/155.57 interpretation satisfying not(EDA) and not(IDA(1)). 600.61/155.57 600.61/155.57 [active](x1) = [1 0] x1 + [0] 600.61/155.57 [0 2] [0] 600.61/155.57 600.61/155.57 [f](x1, x2) = [2 0] x1 + [1 0] x2 + [0] 600.61/155.57 [0 2] [0 1] [0] 600.61/155.57 600.61/155.57 [g](x1) = [4 0] x1 + [0] 600.61/155.57 [0 2] [1] 600.61/155.57 600.61/155.57 [mark](x1) = [0 0] x1 + [0] 600.61/155.57 [0 1] [0] 600.61/155.57 600.61/155.57 [proper](x1) = [0 0] x1 + [0] 600.61/155.57 [0 1] [0] 600.61/155.57 600.61/155.57 [ok](x1) = [1 2] x1 + [2] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [active^#](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_1](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [f^#](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_2](x1, x2, x3) = [7 7] x1 + [7 7] x2 + [7 7] x3 + [0] 600.61/155.57 [0 0] [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [g^#](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_3](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_4](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_5](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_6](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_7](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [proper^#](x1) = [0 1] x1 + [0] 600.61/155.57 [1 4] [0] 600.61/155.57 600.61/155.57 [c_8](x1, x2, x3) = [7 7] x1 + [7 7] x2 + [7 7] x3 + [0] 600.61/155.57 [0 0] [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_9](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [top^#](x1) = [4 4] x1 + [0] 600.61/155.57 [4 0] [4] 600.61/155.57 600.61/155.57 [c] = [0] 600.61/155.57 [0] 600.61/155.57 600.61/155.57 [c_1](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_2](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_3](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_4](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_5](x1, x2, x3) = [7 7] x1 + [7 7] x2 + [7 7] x3 + [0] 600.61/155.57 [0 0] [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_6](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_7](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_8](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_9](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_10](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_11](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c] = [0] 600.61/155.57 [0] 600.61/155.57 600.61/155.57 [c_1](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_3](x1) = [1 0] x1 + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 600.61/155.57 [c_4](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_5](x1) = [2 0] x1 + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 600.61/155.57 [c_6](x1) = [1 0] x1 + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 600.61/155.57 [c_7](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_8](x1) = [1 0] x1 + [7] 600.61/155.57 [0 0] [3] 600.61/155.57 600.61/155.57 The order satisfies the following ordering constraints: 600.61/155.57 600.61/155.57 [active(f(X1, X2))] = [2 0] X1 + [1 0] X2 + [0] 600.61/155.57 [0 4] [0 2] [0] 600.61/155.57 >= [2 0] X1 + [1 0] X2 + [0] 600.61/155.57 [0 4] [0 1] [0] 600.61/155.57 = [f(active(X1), X2)] 600.61/155.57 600.61/155.57 [active(f(g(X), Y))] = [8 0] X + [1 0] Y + [0] 600.61/155.57 [0 8] [0 2] [4] 600.61/155.57 >= [0 0] X + [0 0] Y + [0] 600.61/155.57 [0 6] [0 1] [2] 600.61/155.57 = [mark(f(X, f(g(X), Y)))] 600.61/155.57 600.61/155.57 [active(g(X))] = [4 0] X + [0] 600.61/155.57 [0 4] [2] 600.61/155.57 >= [4 0] X + [0] 600.61/155.57 [0 4] [1] 600.61/155.57 = [g(active(X))] 600.61/155.57 600.61/155.57 [f(mark(X1), X2)] = [0 0] X1 + [1 0] X2 + [0] 600.61/155.57 [0 2] [0 1] [0] 600.61/155.57 >= [0 0] X1 + [0 0] X2 + [0] 600.61/155.57 [0 2] [0 1] [0] 600.61/155.57 = [mark(f(X1, X2))] 600.61/155.57 600.61/155.57 [f(ok(X1), ok(X2))] = [2 4] X1 + [1 2] X2 + [6] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 > [2 4] X1 + [1 2] X2 + [2] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 = [ok(f(X1, X2))] 600.61/155.57 600.61/155.57 [g(mark(X))] = [0 0] X + [0] 600.61/155.57 [0 2] [1] 600.61/155.57 >= [0 0] X + [0] 600.61/155.57 [0 2] [1] 600.61/155.57 = [mark(g(X))] 600.61/155.57 600.61/155.57 [g(ok(X))] = [4 8] X + [8] 600.61/155.57 [0 0] [1] 600.61/155.57 > [4 4] X + [4] 600.61/155.57 [0 0] [0] 600.61/155.57 = [ok(g(X))] 600.61/155.57 600.61/155.57 [proper(f(X1, X2))] = [0 0] X1 + [0 0] X2 + [0] 600.61/155.57 [0 2] [0 1] [0] 600.61/155.57 >= [0 0] X1 + [0 0] X2 + [0] 600.61/155.57 [0 2] [0 1] [0] 600.61/155.57 = [f(proper(X1), proper(X2))] 600.61/155.57 600.61/155.57 [proper(g(X))] = [0 0] X + [0] 600.61/155.57 [0 2] [1] 600.61/155.57 >= [0 0] X + [0] 600.61/155.57 [0 2] [1] 600.61/155.57 = [g(proper(X))] 600.61/155.57 600.61/155.57 [proper^#(f(X1, X2))] = [0 2] X1 + [0 1] X2 + [0] 600.61/155.57 [2 8] [1 4] [0] 600.61/155.57 >= [0 1] X1 + [0 1] X2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 = [c_2(proper^#(X1), proper^#(X2))] 600.61/155.57 600.61/155.57 [proper^#(g(X))] = [0 2] X + [1] 600.61/155.57 [4 8] [4] 600.61/155.57 > [0 1] X + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 = [c_3(proper^#(X))] 600.61/155.57 600.61/155.57 [top^#(mark(X))] = [0 4] X + [0] 600.61/155.57 [0 0] [4] 600.61/155.57 >= [0 2] X + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 = [c_5(proper^#(X))] 600.61/155.57 600.61/155.57 [top^#(mark(X))] = [0 4] X + [0] 600.61/155.57 [0 0] [4] 600.61/155.57 >= [0 4] X + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 = [c_6(top^#(proper(X)))] 600.61/155.57 600.61/155.57 [top^#(ok(X))] = [4 8] X + [8] 600.61/155.57 [4 8] [12] 600.61/155.57 > [4 8] X + [7] 600.61/155.57 [0 0] [3] 600.61/155.57 = [c_8(top^#(active(X)))] 600.61/155.57 600.61/155.57 600.61/155.57 The strictly oriented rules are moved into the weak component. 600.61/155.57 600.61/155.57 We are left with following problem, upon which TcT provides the 600.61/155.57 certificate YES(O(1),O(n^1)). 600.61/155.57 600.61/155.57 Strict DPs: 600.61/155.57 { proper^#(f(X1, X2)) -> c_2(proper^#(X1), proper^#(X2)) } 600.61/155.57 Weak DPs: 600.61/155.57 { proper^#(g(X)) -> c_3(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_5(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_6(top^#(proper(X))) 600.61/155.57 , top^#(ok(X)) -> c_8(top^#(active(X))) } 600.61/155.57 Weak Trs: 600.61/155.57 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.57 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.57 , active(g(X)) -> g(active(X)) 600.61/155.57 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.57 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.57 , g(mark(X)) -> mark(g(X)) 600.61/155.57 , g(ok(X)) -> ok(g(X)) 600.61/155.57 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.57 , proper(g(X)) -> g(proper(X)) } 600.61/155.57 Obligation: 600.61/155.57 innermost runtime complexity 600.61/155.57 Answer: 600.61/155.57 YES(O(1),O(n^1)) 600.61/155.57 600.61/155.57 We use the processor 'matrix interpretation of dimension 2' to 600.61/155.57 orient following rules strictly. 600.61/155.57 600.61/155.57 DPs: 600.61/155.57 { 1: proper^#(f(X1, X2)) -> c_2(proper^#(X1), proper^#(X2)) 600.61/155.57 , 5: top^#(ok(X)) -> c_8(top^#(active(X))) } 600.61/155.57 Trs: 600.61/155.57 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.57 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.57 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) } 600.61/155.57 600.61/155.57 Sub-proof: 600.61/155.57 ---------- 600.61/155.57 The following argument positions are usable: 600.61/155.57 Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_5) = {1}, 600.61/155.57 Uargs(c_6) = {1}, Uargs(c_8) = {1} 600.61/155.57 600.61/155.57 TcT has computed the following constructor-based matrix 600.61/155.57 interpretation satisfying not(EDA) and not(IDA(1)). 600.61/155.57 600.61/155.57 [active](x1) = [4 0] x1 + [0] 600.61/155.57 [0 1] [0] 600.61/155.57 600.61/155.57 [f](x1, x2) = [1 0] x1 + [2 0] x2 + [2] 600.61/155.57 [0 3] [0 2] [0] 600.61/155.57 600.61/155.57 [g](x1) = [1 0] x1 + [0] 600.61/155.57 [0 3] [0] 600.61/155.57 600.61/155.57 [mark](x1) = [1 0] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [proper](x1) = [1 0] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [ok](x1) = [0 0] x1 + [0] 600.61/155.57 [1 1] [1] 600.61/155.57 600.61/155.57 [active^#](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_1](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [f^#](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_2](x1, x2, x3) = [7 7] x1 + [7 7] x2 + [7 7] x3 + [0] 600.61/155.57 [0 0] [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [g^#](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_3](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_4](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_5](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_6](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_7](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [proper^#](x1) = [1 0] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_8](x1, x2, x3) = [7 7] x1 + [7 7] x2 + [7 7] x3 + [0] 600.61/155.57 [0 0] [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_9](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [top^#](x1) = [1 4] x1 + [0] 600.61/155.57 [4 1] [7] 600.61/155.57 600.61/155.57 [c] = [0] 600.61/155.57 [0] 600.61/155.57 600.61/155.57 [c_1](x1, x2) = [7 7] x1 + [7 7] x2 + [0] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_2](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_3](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_4](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_5](x1, x2, x3) = [7 7] x1 + [7 7] x2 + [7 7] x3 + [0] 600.61/155.57 [0 0] [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_6](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_7](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_8](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_9](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_10](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_11](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c] = [0] 600.61/155.57 [0] 600.61/155.57 600.61/155.57 [c_1](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_2](x1, x2) = [1 0] x1 + [2 0] x2 + [1] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 600.61/155.57 [c_3](x1) = [1 0] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_4](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_5](x1) = [1 0] x1 + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 600.61/155.57 [c_6](x1) = [1 0] x1 + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 600.61/155.57 [c_7](x1) = [7 7] x1 + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 600.61/155.57 [c_8](x1) = [1 0] x1 + [3] 600.61/155.57 [0 0] [3] 600.61/155.57 600.61/155.57 The order satisfies the following ordering constraints: 600.61/155.57 600.61/155.57 [active(f(X1, X2))] = [4 0] X1 + [8 0] X2 + [8] 600.61/155.57 [0 3] [0 2] [0] 600.61/155.57 > [4 0] X1 + [2 0] X2 + [2] 600.61/155.57 [0 3] [0 2] [0] 600.61/155.57 = [f(active(X1), X2)] 600.61/155.57 600.61/155.57 [active(f(g(X), Y))] = [4 0] X + [8 0] Y + [8] 600.61/155.57 [0 9] [0 2] [0] 600.61/155.57 > [3 0] X + [4 0] Y + [6] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 = [mark(f(X, f(g(X), Y)))] 600.61/155.57 600.61/155.57 [active(g(X))] = [4 0] X + [0] 600.61/155.57 [0 3] [0] 600.61/155.57 >= [4 0] X + [0] 600.61/155.57 [0 3] [0] 600.61/155.57 = [g(active(X))] 600.61/155.57 600.61/155.57 [f(mark(X1), X2)] = [1 0] X1 + [2 0] X2 + [2] 600.61/155.57 [0 0] [0 2] [0] 600.61/155.57 >= [1 0] X1 + [2 0] X2 + [2] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 = [mark(f(X1, X2))] 600.61/155.57 600.61/155.57 [f(ok(X1), ok(X2))] = [0 0] X1 + [0 0] X2 + [2] 600.61/155.57 [3 3] [2 2] [5] 600.61/155.57 > [0 0] X1 + [0 0] X2 + [0] 600.61/155.57 [1 3] [2 2] [3] 600.61/155.57 = [ok(f(X1, X2))] 600.61/155.57 600.61/155.57 [g(mark(X))] = [1 0] X + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 >= [1 0] X + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 = [mark(g(X))] 600.61/155.57 600.61/155.57 [g(ok(X))] = [0 0] X + [0] 600.61/155.57 [3 3] [3] 600.61/155.57 >= [0 0] X + [0] 600.61/155.57 [1 3] [1] 600.61/155.57 = [ok(g(X))] 600.61/155.57 600.61/155.57 [proper(f(X1, X2))] = [1 0] X1 + [2 0] X2 + [2] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 >= [1 0] X1 + [2 0] X2 + [2] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 = [f(proper(X1), proper(X2))] 600.61/155.57 600.61/155.57 [proper(g(X))] = [1 0] X + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 >= [1 0] X + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 = [g(proper(X))] 600.61/155.57 600.61/155.57 [proper^#(f(X1, X2))] = [1 0] X1 + [2 0] X2 + [2] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 > [1 0] X1 + [2 0] X2 + [1] 600.61/155.57 [0 0] [0 0] [0] 600.61/155.57 = [c_2(proper^#(X1), proper^#(X2))] 600.61/155.57 600.61/155.57 [proper^#(g(X))] = [1 0] X + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 >= [1 0] X + [0] 600.61/155.57 [0 0] [0] 600.61/155.57 = [c_3(proper^#(X))] 600.61/155.57 600.61/155.57 [top^#(mark(X))] = [1 0] X + [0] 600.61/155.57 [4 0] [7] 600.61/155.57 >= [1 0] X + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 = [c_5(proper^#(X))] 600.61/155.57 600.61/155.57 [top^#(mark(X))] = [1 0] X + [0] 600.61/155.57 [4 0] [7] 600.61/155.57 >= [1 0] X + [0] 600.61/155.57 [0 0] [3] 600.61/155.57 = [c_6(top^#(proper(X)))] 600.61/155.57 600.61/155.57 [top^#(ok(X))] = [4 4] X + [4] 600.61/155.57 [1 1] [8] 600.61/155.57 > [4 4] X + [3] 600.61/155.57 [0 0] [3] 600.61/155.57 = [c_8(top^#(active(X)))] 600.61/155.57 600.61/155.57 600.61/155.57 The strictly oriented rules are moved into the weak component. 600.61/155.57 600.61/155.57 We are left with following problem, upon which TcT provides the 600.61/155.57 certificate YES(O(1),O(1)). 600.61/155.57 600.61/155.57 Weak DPs: 600.61/155.57 { proper^#(f(X1, X2)) -> c_2(proper^#(X1), proper^#(X2)) 600.61/155.57 , proper^#(g(X)) -> c_3(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_5(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_6(top^#(proper(X))) 600.61/155.57 , top^#(ok(X)) -> c_8(top^#(active(X))) } 600.61/155.57 Weak Trs: 600.61/155.57 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.57 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.57 , active(g(X)) -> g(active(X)) 600.61/155.57 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.57 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.57 , g(mark(X)) -> mark(g(X)) 600.61/155.57 , g(ok(X)) -> ok(g(X)) 600.61/155.57 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.57 , proper(g(X)) -> g(proper(X)) } 600.61/155.57 Obligation: 600.61/155.57 innermost runtime complexity 600.61/155.57 Answer: 600.61/155.57 YES(O(1),O(1)) 600.61/155.57 600.61/155.57 The following weak DPs constitute a sub-graph of the DG that is 600.61/155.57 closed under successors. The DPs are removed. 600.61/155.57 600.61/155.57 { proper^#(f(X1, X2)) -> c_2(proper^#(X1), proper^#(X2)) 600.61/155.57 , proper^#(g(X)) -> c_3(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_5(proper^#(X)) 600.61/155.57 , top^#(mark(X)) -> c_6(top^#(proper(X))) 600.61/155.57 , top^#(ok(X)) -> c_8(top^#(active(X))) } 600.61/155.57 600.61/155.57 We are left with following problem, upon which TcT provides the 600.61/155.57 certificate YES(O(1),O(1)). 600.61/155.57 600.61/155.57 Weak Trs: 600.61/155.57 { active(f(X1, X2)) -> f(active(X1), X2) 600.61/155.57 , active(f(g(X), Y)) -> mark(f(X, f(g(X), Y))) 600.61/155.57 , active(g(X)) -> g(active(X)) 600.61/155.57 , f(mark(X1), X2) -> mark(f(X1, X2)) 600.61/155.57 , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) 600.61/155.57 , g(mark(X)) -> mark(g(X)) 600.61/155.57 , g(ok(X)) -> ok(g(X)) 600.61/155.57 , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) 600.61/155.57 , proper(g(X)) -> g(proper(X)) } 600.61/155.57 Obligation: 600.61/155.57 innermost runtime complexity 600.61/155.57 Answer: 600.61/155.57 YES(O(1),O(1)) 600.61/155.57 600.61/155.57 No rule is usable, rules are removed from the input problem. 600.61/155.57 600.61/155.57 We are left with following problem, upon which TcT provides the 600.61/155.57 certificate YES(O(1),O(1)). 600.61/155.57 600.61/155.57 Rules: Empty 600.61/155.57 Obligation: 600.61/155.57 innermost runtime complexity 600.61/155.57 Answer: 600.61/155.57 YES(O(1),O(1)) 600.61/155.57 600.61/155.57 Empty rules are trivially bounded 600.61/155.57 600.61/155.57 Hurray, we answered YES(O(1),O(n^2)) 600.61/155.59 EOF