We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d())
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Obligation:
runtime complexity
Answer:
YES(?,O(n^1))
We add the following weak dependency pairs:
Strict DPs:
{ active^#(g(X)) -> c_1(h^#(X))
, active^#(h(d())) -> c_2(g^#(c()))
, active^#(c()) -> c_3()
, h^#(ok(X)) -> c_5(h^#(X))
, g^#(ok(X)) -> c_4(g^#(X))
, proper^#(g(X)) -> c_6(g^#(proper(X)))
, proper^#(h(X)) -> c_7(h^#(proper(X)))
, proper^#(c()) -> c_8()
, proper^#(d()) -> c_9()
, top^#(mark(X)) -> c_10(top^#(proper(X)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ active^#(g(X)) -> c_1(h^#(X))
, active^#(h(d())) -> c_2(g^#(c()))
, active^#(c()) -> c_3()
, h^#(ok(X)) -> c_5(h^#(X))
, g^#(ok(X)) -> c_4(g^#(X))
, proper^#(g(X)) -> c_6(g^#(proper(X)))
, proper^#(h(X)) -> c_7(h^#(proper(X)))
, proper^#(c()) -> c_8()
, proper^#(d()) -> c_9()
, top^#(mark(X)) -> c_10(top^#(proper(X)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d())
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Obligation:
runtime complexity
Answer:
YES(?,O(n^1))
We replace rewrite rules by usable rules:
Strict Usable Rules:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ active^#(g(X)) -> c_1(h^#(X))
, active^#(h(d())) -> c_2(g^#(c()))
, active^#(c()) -> c_3()
, h^#(ok(X)) -> c_5(h^#(X))
, g^#(ok(X)) -> c_4(g^#(X))
, proper^#(g(X)) -> c_6(g^#(proper(X)))
, proper^#(h(X)) -> c_7(h^#(proper(X)))
, proper^#(c()) -> c_8()
, proper^#(d()) -> c_9()
, top^#(mark(X)) -> c_10(top^#(proper(X)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(?,O(n^1))
Consider the dependency graph:
1: active^#(g(X)) -> c_1(h^#(X)) -->_1 h^#(ok(X)) -> c_5(h^#(X)) :4
2: active^#(h(d())) -> c_2(g^#(c()))
3: active^#(c()) -> c_3()
4: h^#(ok(X)) -> c_5(h^#(X)) -->_1 h^#(ok(X)) -> c_5(h^#(X)) :4
5: g^#(ok(X)) -> c_4(g^#(X)) -->_1 g^#(ok(X)) -> c_4(g^#(X)) :5
6: proper^#(g(X)) -> c_6(g^#(proper(X)))
-->_1 g^#(ok(X)) -> c_4(g^#(X)) :5
7: proper^#(h(X)) -> c_7(h^#(proper(X)))
-->_1 h^#(ok(X)) -> c_5(h^#(X)) :4
8: proper^#(c()) -> c_8()
9: proper^#(d()) -> c_9()
10: top^#(mark(X)) -> c_10(top^#(proper(X)))
-->_1 top^#(ok(X)) -> c_11(top^#(active(X))) :11
-->_1 top^#(mark(X)) -> c_10(top^#(proper(X))) :10
11: top^#(ok(X)) -> c_11(top^#(active(X)))
-->_1 top^#(ok(X)) -> c_11(top^#(active(X))) :11
-->_1 top^#(mark(X)) -> c_10(top^#(proper(X))) :10
Only the nodes {3,4,5,8,9,10,11} are reachable from nodes
{3,4,5,8,9,10,11} that start derivation from marked basic terms.
The nodes not reachable are removed from the problem.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ active^#(c()) -> c_3()
, h^#(ok(X)) -> c_5(h^#(X))
, g^#(ok(X)) -> c_4(g^#(X))
, proper^#(c()) -> c_8()
, proper^#(d()) -> c_9()
, top^#(mark(X)) -> c_10(top^#(proper(X)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(?,O(n^1))
We estimate the number of application of {1,4,5} by applications of
Pre({1,4,5}) = {}. Here rules are labeled as follows:
DPs:
{ 1: active^#(c()) -> c_3()
, 2: h^#(ok(X)) -> c_5(h^#(X))
, 3: g^#(ok(X)) -> c_4(g^#(X))
, 4: proper^#(c()) -> c_8()
, 5: proper^#(d()) -> c_9()
, 6: top^#(mark(X)) -> c_10(top^#(proper(X)))
, 7: top^#(ok(X)) -> c_11(top^#(active(X))) }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ h^#(ok(X)) -> c_5(h^#(X))
, g^#(ok(X)) -> c_4(g^#(X))
, top^#(mark(X)) -> c_10(top^#(proper(X)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Weak DPs:
{ active^#(c()) -> c_3()
, proper^#(c()) -> c_8()
, proper^#(d()) -> c_9() }
Obligation:
runtime complexity
Answer:
YES(?,O(n^1))
We employ 'linear path analysis' using the following approximated
dependency graph:
->{1} [ YES(O(1),O(n^1)) ]
->{2} [ YES(O(1),O(n^1)) ]
->{3,4} [ YES(O(1),O(n^1)) ]
->{5} [ YES(O(1),O(1)) ]
->{6} [ YES(O(1),O(1)) ]
->{7} [ YES(O(1),O(1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: h^#(ok(X)) -> c_5(h^#(X))
, 2: g^#(ok(X)) -> c_4(g^#(X))
, 3: top^#(mark(X)) -> c_10(top^#(proper(X)))
, 4: top^#(ok(X)) -> c_11(top^#(active(X))) }
Weak DPs:
{ 5: active^#(c()) -> c_3()
, 6: proper^#(c()) -> c_8()
, 7: proper^#(d()) -> c_9() }
* Path {1}: YES(O(1),O(n^1))
--------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { h^#(ok(X)) -> c_5(h^#(X)) }
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^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(n^1)).
Strict DPs: { h^#(ok(X)) -> c_5(h^#(X)) }
Obligation:
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: h^#(ok(X)) -> c_5(h^#(X)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_5) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[ok](x1) = [1] x1 + [2]
[h^#](x1) = [4] x1 + [0]
[c_5](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[h^#(ok(X))] = [4] X + [8]
> [4] X + [1]
= [c_5(h^#(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: { h^#(ok(X)) -> c_5(h^#(X)) }
Obligation:
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.
{ h^#(ok(X)) -> c_5(h^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
* Path {2}: YES(O(1),O(n^1))
--------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { g^#(ok(X)) -> c_4(g^#(X)) }
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^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(n^1)).
Strict DPs: { g^#(ok(X)) -> c_4(g^#(X)) }
Obligation:
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: g^#(ok(X)) -> c_4(g^#(X)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_4) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[ok](x1) = [1] x1 + [2]
[g^#](x1) = [4] x1 + [0]
[c_4](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[g^#(ok(X))] = [4] X + [8]
> [4] X + [1]
= [c_4(g^#(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: { g^#(ok(X)) -> c_4(g^#(X)) }
Obligation:
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.
{ g^#(ok(X)) -> c_4(g^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
* Path {3,4}: YES(O(1),O(n^1))
----------------------------
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)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[active](x1) = [1] x1 + [1]
[g](x1) = [1] x1 + [0]
[mark](x1) = [1] x1 + [0]
[h](x1) = [1] x1 + [0]
[c] = [0]
[d] = [0]
[proper](x1) = [1] x1 + [0]
[ok](x1) = [1] x1 + [0]
[top^#](x1) = [1] x1 + [0]
[c_10](x1) = [1] x1 + [0]
[c_11](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[active(g(X))] = [1] X + [1]
> [1] X + [0]
= [mark(h(X))]
[active(h(d()))] = [1]
> [0]
= [mark(g(c()))]
[active(c())] = [1]
> [0]
= [mark(d())]
[g(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(g(X))]
[h(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(h(X))]
[proper(g(X))] = [1] X + [0]
>= [1] X + [0]
= [g(proper(X))]
[proper(h(X))] = [1] X + [0]
>= [1] X + [0]
= [h(proper(X))]
[proper(c())] = [0]
>= [0]
= [ok(c())]
[proper(d())] = [0]
>= [0]
= [ok(d())]
[top^#(mark(X))] = [1] X + [0]
>= [1] X + [0]
= [c_10(top^#(proper(X)))]
[top^#(ok(X))] = [1] X + [0]
? [1] X + [1]
= [c_11(top^#(active(X)))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
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)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Strict Trs:
{ g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Weak Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[active](x1) = [1] x1 + [5]
[g](x1) = [1] x1 + [0]
[mark](x1) = [1] x1 + [1]
[h](x1) = [1] x1 + [0]
[c] = [0]
[d] = [1]
[proper](x1) = [1] x1 + [0]
[ok](x1) = [1] x1 + [0]
[top^#](x1) = [1] x1 + [3]
[c_10](x1) = [1] x1 + [0]
[c_11](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[active(g(X))] = [1] X + [5]
> [1] X + [1]
= [mark(h(X))]
[active(h(d()))] = [6]
> [1]
= [mark(g(c()))]
[active(c())] = [5]
> [2]
= [mark(d())]
[g(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(g(X))]
[h(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(h(X))]
[proper(g(X))] = [1] X + [0]
>= [1] X + [0]
= [g(proper(X))]
[proper(h(X))] = [1] X + [0]
>= [1] X + [0]
= [h(proper(X))]
[proper(c())] = [0]
>= [0]
= [ok(c())]
[proper(d())] = [1]
>= [1]
= [ok(d())]
[top^#(mark(X))] = [1] X + [4]
> [1] X + [3]
= [c_10(top^#(proper(X)))]
[top^#(ok(X))] = [1] X + [3]
? [1] X + [8]
= [c_11(top^#(active(X)))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { top^#(ok(X)) -> c_11(top^#(active(X))) }
Strict Trs:
{ g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Weak DPs: { top^#(mark(X)) -> c_10(top^#(proper(X))) }
Weak Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[active](x1) = [1] x1 + [4]
[g](x1) = [1] x1 + [0]
[mark](x1) = [1] x1 + [1]
[h](x1) = [1] x1 + [0]
[c] = [0]
[d] = [0]
[proper](x1) = [1] x1 + [1]
[ok](x1) = [1] x1 + [0]
[top^#](x1) = [1] x1 + [4]
[c_10](x1) = [1] x1 + [0]
[c_11](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[active(g(X))] = [1] X + [4]
> [1] X + [1]
= [mark(h(X))]
[active(h(d()))] = [4]
> [1]
= [mark(g(c()))]
[active(c())] = [4]
> [1]
= [mark(d())]
[g(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(g(X))]
[h(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(h(X))]
[proper(g(X))] = [1] X + [1]
>= [1] X + [1]
= [g(proper(X))]
[proper(h(X))] = [1] X + [1]
>= [1] X + [1]
= [h(proper(X))]
[proper(c())] = [1]
> [0]
= [ok(c())]
[proper(d())] = [1]
> [0]
= [ok(d())]
[top^#(mark(X))] = [1] X + [5]
>= [1] X + [5]
= [c_10(top^#(proper(X)))]
[top^#(ok(X))] = [1] X + [4]
? [1] X + [8]
= [c_11(top^#(active(X)))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { top^#(ok(X)) -> c_11(top^#(active(X))) }
Strict Trs:
{ g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs: { top^#(mark(X)) -> c_10(top^#(proper(X))) }
Weak Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[active](x1) = [1 7] x1 + [0]
[0 0] [1]
[g](x1) = [1 0] x1 + [0]
[0 1] [2]
[mark](x1) = [1 4] x1 + [2]
[0 0] [1]
[h](x1) = [1 7] x1 + [1]
[0 0] [2]
[c] = [3]
[0]
[d] = [0]
[0]
[proper](x1) = [1 0] x1 + [0]
[0 1] [2]
[ok](x1) = [1 7] x1 + [0]
[0 0] [2]
[top^#](x1) = [1 2] x1 + [7]
[0 0] [0]
[c_10](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_11](x1) = [1 0] x1 + [0]
[0 1] [0]
The order satisfies the following ordering constraints:
[active(g(X))] = [1 7] X + [14]
[0 0] [1]
> [1 7] X + [11]
[0 0] [1]
= [mark(h(X))]
[active(h(d()))] = [15]
[1]
> [13]
[1]
= [mark(g(c()))]
[active(c())] = [3]
[1]
> [2]
[1]
= [mark(d())]
[g(ok(X))] = [1 7] X + [0]
[0 0] [4]
? [1 7] X + [14]
[0 0] [2]
= [ok(g(X))]
[h(ok(X))] = [1 7] X + [15]
[0 0] [2]
>= [1 7] X + [15]
[0 0] [2]
= [ok(h(X))]
[proper(g(X))] = [1 0] X + [0]
[0 1] [4]
>= [1 0] X + [0]
[0 1] [4]
= [g(proper(X))]
[proper(h(X))] = [1 7] X + [1]
[0 0] [4]
? [1 7] X + [15]
[0 0] [2]
= [h(proper(X))]
[proper(c())] = [3]
[2]
>= [3]
[2]
= [ok(c())]
[proper(d())] = [0]
[2]
>= [0]
[2]
= [ok(d())]
[top^#(mark(X))] = [1 4] X + [11]
[0 0] [0]
>= [1 2] X + [11]
[0 0] [0]
= [c_10(top^#(proper(X)))]
[top^#(ok(X))] = [1 7] X + [11]
[0 0] [0]
> [1 7] X + [9]
[0 0] [0]
= [c_11(top^#(active(X)))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_10(top^#(proper(X)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Weak Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs: { proper(g(X)) -> g(proper(X)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[active](x1) = [1 1] x1 + [4]
[0 0] [2]
[g](x1) = [1 7] x1 + [0]
[0 3] [2]
[mark](x1) = [1 3] x1 + [4]
[0 0] [2]
[h](x1) = [1 6] x1 + [2]
[0 1] [0]
[c] = [3]
[0]
[d] = [0]
[1]
[proper](x1) = [1 2] x1 + [6]
[0 1] [0]
[ok](x1) = [1 0] x1 + [6]
[0 1] [0]
[top^#](x1) = [1 1] x1 + [1]
[0 0] [0]
[c_10](x1) = [1 1] x1 + [0]
[0 0] [0]
[c_11](x1) = [1 0] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(g(X))] = [1 10] X + [6]
[0 0] [2]
>= [1 9] X + [6]
[0 0] [2]
= [mark(h(X))]
[active(h(d()))] = [13]
[2]
>= [13]
[2]
= [mark(g(c()))]
[active(c())] = [7]
[2]
>= [7]
[2]
= [mark(d())]
[g(ok(X))] = [1 7] X + [6]
[0 3] [2]
>= [1 7] X + [6]
[0 3] [2]
= [ok(g(X))]
[h(ok(X))] = [1 6] X + [8]
[0 1] [0]
>= [1 6] X + [8]
[0 1] [0]
= [ok(h(X))]
[proper(g(X))] = [1 13] X + [10]
[0 3] [2]
> [1 9] X + [6]
[0 3] [2]
= [g(proper(X))]
[proper(h(X))] = [1 8] X + [8]
[0 1] [0]
>= [1 8] X + [8]
[0 1] [0]
= [h(proper(X))]
[proper(c())] = [9]
[0]
>= [9]
[0]
= [ok(c())]
[proper(d())] = [8]
[1]
> [6]
[1]
= [ok(d())]
[top^#(mark(X))] = [1 3] X + [7]
[0 0] [0]
>= [1 3] X + [7]
[0 0] [0]
= [c_10(top^#(proper(X)))]
[top^#(ok(X))] = [1 1] X + [7]
[0 0] [0]
>= [1 1] X + [7]
[0 0] [0]
= [c_11(top^#(active(X)))]
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 Trs:
{ g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_10(top^#(proper(X)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Weak Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, proper(g(X)) -> g(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs: { proper(h(X)) -> h(proper(X)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[active](x1) = [1 0] x1 + [6]
[0 0] [1]
[g](x1) = [1 7] x1 + [7]
[0 1] [0]
[mark](x1) = [1 1] x1 + [6]
[0 0] [1]
[h](x1) = [1 4] x1 + [1]
[0 2] [6]
[c] = [2]
[0]
[d] = [0]
[2]
[proper](x1) = [1 1] x1 + [6]
[0 1] [0]
[ok](x1) = [1 0] x1 + [6]
[0 1] [0]
[top^#](x1) = [1 0] x1 + [5]
[0 0] [0]
[c_10](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_11](x1) = [1 0] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(g(X))] = [1 7] X + [13]
[0 0] [1]
>= [1 6] X + [13]
[0 0] [1]
= [mark(h(X))]
[active(h(d()))] = [15]
[1]
>= [15]
[1]
= [mark(g(c()))]
[active(c())] = [8]
[1]
>= [8]
[1]
= [mark(d())]
[g(ok(X))] = [1 7] X + [13]
[0 1] [0]
>= [1 7] X + [13]
[0 1] [0]
= [ok(g(X))]
[h(ok(X))] = [1 4] X + [7]
[0 2] [6]
>= [1 4] X + [7]
[0 2] [6]
= [ok(h(X))]
[proper(g(X))] = [1 8] X + [13]
[0 1] [0]
>= [1 8] X + [13]
[0 1] [0]
= [g(proper(X))]
[proper(h(X))] = [1 6] X + [13]
[0 2] [6]
> [1 5] X + [7]
[0 2] [6]
= [h(proper(X))]
[proper(c())] = [8]
[0]
>= [8]
[0]
= [ok(c())]
[proper(d())] = [8]
[2]
> [6]
[2]
= [ok(d())]
[top^#(mark(X))] = [1 1] X + [11]
[0 0] [0]
>= [1 1] X + [11]
[0 0] [0]
= [c_10(top^#(proper(X)))]
[top^#(ok(X))] = [1 0] X + [11]
[0 0] [0]
>= [1 0] X + [11]
[0 0] [0]
= [c_11(top^#(active(X)))]
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 Trs:
{ g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_10(top^#(proper(X)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Weak Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs: { g(ok(X)) -> ok(g(X)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[active](x1) = [1 0] x1 + [2]
[0 0] [0]
[g](x1) = [2 7] x1 + [1]
[0 4] [1]
[mark](x1) = [1 2] x1 + [2]
[0 0] [0]
[h](x1) = [1 5] x1 + [1]
[0 1] [0]
[c] = [4]
[0]
[d] = [0]
[2]
[proper](x1) = [1 2] x1 + [2]
[0 1] [0]
[ok](x1) = [1 0] x1 + [2]
[0 1] [0]
[top^#](x1) = [1 0] x1 + [6]
[1 1] [4]
[c_10](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_11](x1) = [1 0] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(g(X))] = [2 7] X + [3]
[0 0] [0]
>= [1 7] X + [3]
[0 0] [0]
= [mark(h(X))]
[active(h(d()))] = [13]
[0]
>= [13]
[0]
= [mark(g(c()))]
[active(c())] = [6]
[0]
>= [6]
[0]
= [mark(d())]
[g(ok(X))] = [2 7] X + [5]
[0 4] [1]
> [2 7] X + [3]
[0 4] [1]
= [ok(g(X))]
[h(ok(X))] = [1 5] X + [3]
[0 1] [0]
>= [1 5] X + [3]
[0 1] [0]
= [ok(h(X))]
[proper(g(X))] = [2 15] X + [5]
[0 4] [1]
>= [2 11] X + [5]
[0 4] [1]
= [g(proper(X))]
[proper(h(X))] = [1 7] X + [3]
[0 1] [0]
>= [1 7] X + [3]
[0 1] [0]
= [h(proper(X))]
[proper(c())] = [6]
[0]
>= [6]
[0]
= [ok(c())]
[proper(d())] = [6]
[2]
> [2]
[2]
= [ok(d())]
[top^#(mark(X))] = [1 2] X + [8]
[1 2] [6]
>= [1 2] X + [8]
[0 0] [0]
= [c_10(top^#(proper(X)))]
[top^#(ok(X))] = [1 0] X + [8]
[1 1] [6]
>= [1 0] X + [8]
[0 0] [0]
= [c_11(top^#(active(X)))]
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 Trs: { h(ok(X)) -> ok(h(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_10(top^#(proper(X)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Weak Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs: { h(ok(X)) -> ok(h(X)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[active](x1) = [1 1] x1 + [0]
[0 0] [1]
[g](x1) = [2 7] x1 + [0]
[0 4] [2]
[mark](x1) = [1 2] x1 + [0]
[0 0] [1]
[h](x1) = [2 5] x1 + [0]
[0 3] [1]
[c] = [4]
[0]
[d] = [2]
[1]
[proper](x1) = [1 1] x1 + [1]
[0 1] [0]
[ok](x1) = [1 0] x1 + [1]
[0 1] [0]
[top^#](x1) = [4 4] x1 + [3]
[1 0] [4]
[c_10](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_11](x1) = [1 0] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(g(X))] = [2 11] X + [2]
[0 0] [1]
>= [2 11] X + [2]
[0 0] [1]
= [mark(h(X))]
[active(h(d()))] = [13]
[1]
> [12]
[1]
= [mark(g(c()))]
[active(c())] = [4]
[1]
>= [4]
[1]
= [mark(d())]
[g(ok(X))] = [2 7] X + [2]
[0 4] [2]
> [2 7] X + [1]
[0 4] [2]
= [ok(g(X))]
[h(ok(X))] = [2 5] X + [2]
[0 3] [1]
> [2 5] X + [1]
[0 3] [1]
= [ok(h(X))]
[proper(g(X))] = [2 11] X + [3]
[0 4] [2]
> [2 9] X + [2]
[0 4] [2]
= [g(proper(X))]
[proper(h(X))] = [2 8] X + [2]
[0 3] [1]
>= [2 7] X + [2]
[0 3] [1]
= [h(proper(X))]
[proper(c())] = [5]
[0]
>= [5]
[0]
= [ok(c())]
[proper(d())] = [4]
[1]
> [3]
[1]
= [ok(d())]
[top^#(mark(X))] = [4 8] X + [7]
[1 2] [4]
>= [4 8] X + [7]
[0 0] [0]
= [c_10(top^#(proper(X)))]
[top^#(ok(X))] = [4 4] X + [7]
[1 0] [5]
>= [4 4] X + [7]
[0 0] [0]
= [c_11(top^#(active(X)))]
We return to the main proof.
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)))
, top^#(ok(X)) -> c_11(top^#(active(X))) }
Weak Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
* Path {5}: YES(O(1),O(1))
------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Weak DPs: { active^#(c()) -> c_3() }
Obligation:
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)).
Weak DPs: { active^#(c()) -> c_3() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
* Path {6}: YES(O(1),O(1))
------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Weak DPs: { proper^#(c()) -> c_8() }
Obligation:
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)).
Weak DPs: { proper^#(c()) -> c_8() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
* Path {7}: YES(O(1),O(1))
------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict Trs:
{ active(g(X)) -> mark(h(X))
, active(h(d())) -> mark(g(c()))
, active(c()) -> mark(d())
, g(ok(X)) -> ok(g(X))
, h(ok(X)) -> ok(h(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X))
, proper(c()) -> ok(c())
, proper(d()) -> ok(d()) }
Weak DPs: { proper^#(d()) -> c_9() }
Obligation:
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)).
Weak DPs: { proper^#(d()) -> c_9() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))