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