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