We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, 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^#(f(X)) -> c_1(f^#(active(X)))
, active^#(f(f(X))) -> c_2(c^#(f(g(f(X)))))
, active^#(c(X)) -> c_3(d^#(X))
, active^#(h(X)) -> c_4(c^#(d(X)))
, active^#(h(X)) -> c_5(h^#(active(X)))
, f^#(mark(X)) -> c_6(f^#(X))
, f^#(ok(X)) -> c_7(f^#(X))
, c^#(ok(X)) -> c_8(c^#(X))
, d^#(ok(X)) -> c_10(d^#(X))
, h^#(mark(X)) -> c_11(h^#(X))
, h^#(ok(X)) -> c_12(h^#(X))
, g^#(ok(X)) -> c_9(g^#(X))
, proper^#(f(X)) -> c_13(f^#(proper(X)))
, proper^#(c(X)) -> c_14(c^#(proper(X)))
, proper^#(g(X)) -> c_15(g^#(proper(X)))
, proper^#(d(X)) -> c_16(d^#(proper(X)))
, proper^#(h(X)) -> c_17(h^#(proper(X)))
, top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(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^#(f(X)) -> c_1(f^#(active(X)))
, active^#(f(f(X))) -> c_2(c^#(f(g(f(X)))))
, active^#(c(X)) -> c_3(d^#(X))
, active^#(h(X)) -> c_4(c^#(d(X)))
, active^#(h(X)) -> c_5(h^#(active(X)))
, f^#(mark(X)) -> c_6(f^#(X))
, f^#(ok(X)) -> c_7(f^#(X))
, c^#(ok(X)) -> c_8(c^#(X))
, d^#(ok(X)) -> c_10(d^#(X))
, h^#(mark(X)) -> c_11(h^#(X))
, h^#(ok(X)) -> c_12(h^#(X))
, g^#(ok(X)) -> c_9(g^#(X))
, proper^#(f(X)) -> c_13(f^#(proper(X)))
, proper^#(c(X)) -> c_14(c^#(proper(X)))
, proper^#(g(X)) -> c_15(g^#(proper(X)))
, proper^#(d(X)) -> c_16(d^#(proper(X)))
, proper^#(h(X)) -> c_17(h^#(proper(X)))
, top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X))
, 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(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict DPs:
{ active^#(f(X)) -> c_1(f^#(active(X)))
, active^#(f(f(X))) -> c_2(c^#(f(g(f(X)))))
, active^#(c(X)) -> c_3(d^#(X))
, active^#(h(X)) -> c_4(c^#(d(X)))
, active^#(h(X)) -> c_5(h^#(active(X)))
, f^#(mark(X)) -> c_6(f^#(X))
, f^#(ok(X)) -> c_7(f^#(X))
, c^#(ok(X)) -> c_8(c^#(X))
, d^#(ok(X)) -> c_10(d^#(X))
, h^#(mark(X)) -> c_11(h^#(X))
, h^#(ok(X)) -> c_12(h^#(X))
, g^#(ok(X)) -> c_9(g^#(X))
, proper^#(f(X)) -> c_13(f^#(proper(X)))
, proper^#(c(X)) -> c_14(c^#(proper(X)))
, proper^#(g(X)) -> c_15(g^#(proper(X)))
, proper^#(d(X)) -> c_16(d^#(proper(X)))
, proper^#(h(X)) -> c_17(h^#(proper(X)))
, top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Obligation:
runtime complexity
Answer:
YES(?,O(n^1))
Consider the dependency graph:
1: active^#(f(X)) -> c_1(f^#(active(X)))
-->_1 f^#(ok(X)) -> c_7(f^#(X)) :7
-->_1 f^#(mark(X)) -> c_6(f^#(X)) :6
2: active^#(f(f(X))) -> c_2(c^#(f(g(f(X)))))
-->_1 c^#(ok(X)) -> c_8(c^#(X)) :8
3: active^#(c(X)) -> c_3(d^#(X))
-->_1 d^#(ok(X)) -> c_10(d^#(X)) :9
4: active^#(h(X)) -> c_4(c^#(d(X)))
-->_1 c^#(ok(X)) -> c_8(c^#(X)) :8
5: active^#(h(X)) -> c_5(h^#(active(X)))
-->_1 h^#(ok(X)) -> c_12(h^#(X)) :11
-->_1 h^#(mark(X)) -> c_11(h^#(X)) :10
6: f^#(mark(X)) -> c_6(f^#(X))
-->_1 f^#(ok(X)) -> c_7(f^#(X)) :7
-->_1 f^#(mark(X)) -> c_6(f^#(X)) :6
7: f^#(ok(X)) -> c_7(f^#(X))
-->_1 f^#(ok(X)) -> c_7(f^#(X)) :7
-->_1 f^#(mark(X)) -> c_6(f^#(X)) :6
8: c^#(ok(X)) -> c_8(c^#(X)) -->_1 c^#(ok(X)) -> c_8(c^#(X)) :8
9: d^#(ok(X)) -> c_10(d^#(X)) -->_1 d^#(ok(X)) -> c_10(d^#(X)) :9
10: h^#(mark(X)) -> c_11(h^#(X))
-->_1 h^#(ok(X)) -> c_12(h^#(X)) :11
-->_1 h^#(mark(X)) -> c_11(h^#(X)) :10
11: h^#(ok(X)) -> c_12(h^#(X))
-->_1 h^#(ok(X)) -> c_12(h^#(X)) :11
-->_1 h^#(mark(X)) -> c_11(h^#(X)) :10
12: g^#(ok(X)) -> c_9(g^#(X)) -->_1 g^#(ok(X)) -> c_9(g^#(X)) :12
13: proper^#(f(X)) -> c_13(f^#(proper(X)))
-->_1 f^#(ok(X)) -> c_7(f^#(X)) :7
-->_1 f^#(mark(X)) -> c_6(f^#(X)) :6
14: proper^#(c(X)) -> c_14(c^#(proper(X)))
-->_1 c^#(ok(X)) -> c_8(c^#(X)) :8
15: proper^#(g(X)) -> c_15(g^#(proper(X)))
-->_1 g^#(ok(X)) -> c_9(g^#(X)) :12
16: proper^#(d(X)) -> c_16(d^#(proper(X)))
-->_1 d^#(ok(X)) -> c_10(d^#(X)) :9
17: proper^#(h(X)) -> c_17(h^#(proper(X)))
-->_1 h^#(ok(X)) -> c_12(h^#(X)) :11
-->_1 h^#(mark(X)) -> c_11(h^#(X)) :10
18: top^#(mark(X)) -> c_18(top^#(proper(X)))
-->_1 top^#(ok(X)) -> c_19(top^#(active(X))) :19
-->_1 top^#(mark(X)) -> c_18(top^#(proper(X))) :18
19: top^#(ok(X)) -> c_19(top^#(active(X)))
-->_1 top^#(ok(X)) -> c_19(top^#(active(X))) :19
-->_1 top^#(mark(X)) -> c_18(top^#(proper(X))) :18
Only the nodes {6,7,8,9,10,11,12,18,19} are reachable from nodes
{6,7,8,9,10,11,12,18,19} 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:
{ f^#(mark(X)) -> c_6(f^#(X))
, f^#(ok(X)) -> c_7(f^#(X))
, c^#(ok(X)) -> c_8(c^#(X))
, d^#(ok(X)) -> c_10(d^#(X))
, h^#(mark(X)) -> c_11(h^#(X))
, h^#(ok(X)) -> c_12(h^#(X))
, g^#(ok(X)) -> c_9(g^#(X))
, top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Obligation:
runtime complexity
Answer:
YES(?,O(n^1))
We employ 'linear path analysis' using the following approximated
dependency graph:
->{1,2} [ YES(O(1),O(n^1)) ]
->{3} [ YES(O(1),O(n^1)) ]
->{4} [ YES(O(1),O(n^1)) ]
->{5,6} [ YES(O(1),O(n^1)) ]
->{7} [ YES(O(1),O(n^1)) ]
->{8,9} [ YES(O(1),O(n^1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: f^#(mark(X)) -> c_6(f^#(X))
, 2: f^#(ok(X)) -> c_7(f^#(X))
, 3: c^#(ok(X)) -> c_8(c^#(X))
, 4: d^#(ok(X)) -> c_10(d^#(X))
, 5: h^#(mark(X)) -> c_11(h^#(X))
, 6: h^#(ok(X)) -> c_12(h^#(X))
, 7: g^#(ok(X)) -> c_9(g^#(X))
, 8: top^#(mark(X)) -> c_18(top^#(proper(X)))
, 9: top^#(ok(X)) -> c_19(top^#(active(X))) }
* Path {1,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:
{ f^#(mark(X)) -> c_6(f^#(X))
, f^#(ok(X)) -> c_7(f^#(X)) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
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:
{ f^#(mark(X)) -> c_6(f^#(X))
, f^#(ok(X)) -> c_7(f^#(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: f^#(mark(X)) -> c_6(f^#(X))
, 2: f^#(ok(X)) -> c_7(f^#(X)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_6) = {1}, Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[mark](x1) = [1] x1 + [4]
[ok](x1) = [1] x1 + [4]
[f^#](x1) = [2] x1 + [0]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[f^#(mark(X))] = [2] X + [8]
> [2] X + [0]
= [c_6(f^#(X))]
[f^#(ok(X))] = [2] X + [8]
> [2] X + [1]
= [c_7(f^#(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:
{ f^#(mark(X)) -> c_6(f^#(X))
, f^#(ok(X)) -> c_7(f^#(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.
{ f^#(mark(X)) -> c_6(f^#(X))
, f^#(ok(X)) -> c_7(f^#(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}: 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: { c^#(ok(X)) -> c_8(c^#(X)) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
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: { c^#(ok(X)) -> c_8(c^#(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: c^#(ok(X)) -> c_8(c^#(X)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_8) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[ok](x1) = [1] x1 + [2]
[c^#](x1) = [4] x1 + [0]
[c_8](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[c^#(ok(X))] = [4] X + [8]
> [4] X + [1]
= [c_8(c^#(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: { c^#(ok(X)) -> c_8(c^#(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.
{ c^#(ok(X)) -> c_8(c^#(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 {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: { d^#(ok(X)) -> c_10(d^#(X)) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
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: { d^#(ok(X)) -> c_10(d^#(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: d^#(ok(X)) -> c_10(d^#(X)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_10) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[ok](x1) = [1] x1 + [2]
[d^#](x1) = [4] x1 + [0]
[c_10](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[d^#(ok(X))] = [4] X + [8]
> [4] X + [1]
= [c_10(d^#(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: { d^#(ok(X)) -> c_10(d^#(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.
{ d^#(ok(X)) -> c_10(d^#(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 {5,6}: 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^#(mark(X)) -> c_11(h^#(X))
, h^#(ok(X)) -> c_12(h^#(X)) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
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^#(mark(X)) -> c_11(h^#(X))
, h^#(ok(X)) -> c_12(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^#(mark(X)) -> c_11(h^#(X))
, 2: h^#(ok(X)) -> c_12(h^#(X)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_11) = {1}, Uargs(c_12) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[mark](x1) = [1] x1 + [4]
[ok](x1) = [1] x1 + [4]
[h^#](x1) = [2] x1 + [0]
[c_11](x1) = [1] x1 + [0]
[c_12](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[h^#(mark(X))] = [2] X + [8]
> [2] X + [0]
= [c_11(h^#(X))]
[h^#(ok(X))] = [2] X + [8]
> [2] X + [1]
= [c_12(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^#(mark(X)) -> c_11(h^#(X))
, h^#(ok(X)) -> c_12(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^#(mark(X)) -> c_11(h^#(X))
, h^#(ok(X)) -> c_12(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 {7}: 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_9(g^#(X)) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
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_9(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_9(g^#(X)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_9) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[ok](x1) = [1] x1 + [2]
[g^#](x1) = [4] x1 + [0]
[c_9](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[g^#(ok(X))] = [4] X + [8]
> [4] X + [1]
= [c_9(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_9(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_9(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 {8,9}: 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_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
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]
[f](x1) = [1] x1 + [0]
[mark](x1) = [1] x1 + [0]
[c](x1) = [1] x1 + [0]
[g](x1) = [1] x1 + [0]
[d](x1) = [1] x1 + [0]
[h](x1) = [1] x1 + [0]
[proper](x1) = [1] x1 + [0]
[ok](x1) = [1] x1 + [0]
[top^#](x1) = [1] x1 + [0]
[c_18](x1) = [1] x1 + [0]
[c_19](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [1] X + [1]
>= [1] X + [1]
= [f(active(X))]
[active(f(f(X)))] = [1] X + [1]
> [1] X + [0]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1] X + [1]
> [1] X + [0]
= [mark(d(X))]
[active(h(X))] = [1] X + [1]
> [1] X + [0]
= [mark(c(d(X)))]
[active(h(X))] = [1] X + [1]
>= [1] X + [1]
= [h(active(X))]
[f(mark(X))] = [1] X + [0]
>= [1] X + [0]
= [mark(f(X))]
[f(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(f(X))]
[c(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(c(X))]
[g(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(g(X))]
[d(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(d(X))]
[h(mark(X))] = [1] X + [0]
>= [1] X + [0]
= [mark(h(X))]
[h(ok(X))] = [1] X + [0]
>= [1] X + [0]
= [ok(h(X))]
[proper(f(X))] = [1] X + [0]
>= [1] X + [0]
= [f(proper(X))]
[proper(c(X))] = [1] X + [0]
>= [1] X + [0]
= [c(proper(X))]
[proper(g(X))] = [1] X + [0]
>= [1] X + [0]
= [g(proper(X))]
[proper(d(X))] = [1] X + [0]
>= [1] X + [0]
= [d(proper(X))]
[proper(h(X))] = [1] X + [0]
>= [1] X + [0]
= [h(proper(X))]
[top^#(mark(X))] = [1] X + [0]
>= [1] X + [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [1] X + [0]
? [1] X + [1]
= [c_19(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_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak Trs:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X))) }
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 + [7]
[f](x1) = [1] x1 + [0]
[mark](x1) = [1] x1 + [2]
[c](x1) = [1] x1 + [0]
[g](x1) = [1] x1 + [4]
[d](x1) = [1] x1 + [2]
[h](x1) = [1] x1 + [5]
[proper](x1) = [1] x1 + [0]
[ok](x1) = [1] x1 + [1]
[top^#](x1) = [1] x1 + [4]
[c_18](x1) = [1] x1 + [0]
[c_19](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[active(f(X))] = [1] X + [7]
>= [1] X + [7]
= [f(active(X))]
[active(f(f(X)))] = [1] X + [7]
> [1] X + [6]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1] X + [7]
> [1] X + [4]
= [mark(d(X))]
[active(h(X))] = [1] X + [12]
> [1] X + [4]
= [mark(c(d(X)))]
[active(h(X))] = [1] X + [12]
>= [1] X + [12]
= [h(active(X))]
[f(mark(X))] = [1] X + [2]
>= [1] X + [2]
= [mark(f(X))]
[f(ok(X))] = [1] X + [1]
>= [1] X + [1]
= [ok(f(X))]
[c(ok(X))] = [1] X + [1]
>= [1] X + [1]
= [ok(c(X))]
[g(ok(X))] = [1] X + [5]
>= [1] X + [5]
= [ok(g(X))]
[d(ok(X))] = [1] X + [3]
>= [1] X + [3]
= [ok(d(X))]
[h(mark(X))] = [1] X + [7]
>= [1] X + [7]
= [mark(h(X))]
[h(ok(X))] = [1] X + [6]
>= [1] X + [6]
= [ok(h(X))]
[proper(f(X))] = [1] X + [0]
>= [1] X + [0]
= [f(proper(X))]
[proper(c(X))] = [1] X + [0]
>= [1] X + [0]
= [c(proper(X))]
[proper(g(X))] = [1] X + [4]
>= [1] X + [4]
= [g(proper(X))]
[proper(d(X))] = [1] X + [2]
>= [1] X + [2]
= [d(proper(X))]
[proper(h(X))] = [1] X + [5]
>= [1] X + [5]
= [h(proper(X))]
[top^#(mark(X))] = [1] X + [6]
> [1] X + [4]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [1] X + [5]
? [1] X + [12]
= [c_19(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_19(top^#(active(X))) }
Strict Trs:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs: { top^#(mark(X)) -> c_18(top^#(proper(X))) }
Weak Trs:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X))) }
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]
[f](x1) = [1] x1 + [4]
[mark](x1) = [1] x1 + [4]
[c](x1) = [1] x1 + [0]
[g](x1) = [1] x1 + [0]
[d](x1) = [1] x1 + [0]
[h](x1) = [1] x1 + [0]
[proper](x1) = [1] x1 + [4]
[ok](x1) = [1] x1 + [5]
[top^#](x1) = [1] x1 + [0]
[c_18](x1) = [1] x1 + [0]
[c_19](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [1] X + [8]
>= [1] X + [8]
= [f(active(X))]
[active(f(f(X)))] = [1] X + [12]
>= [1] X + [12]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1] X + [4]
>= [1] X + [4]
= [mark(d(X))]
[active(h(X))] = [1] X + [4]
>= [1] X + [4]
= [mark(c(d(X)))]
[active(h(X))] = [1] X + [4]
>= [1] X + [4]
= [h(active(X))]
[f(mark(X))] = [1] X + [8]
>= [1] X + [8]
= [mark(f(X))]
[f(ok(X))] = [1] X + [9]
>= [1] X + [9]
= [ok(f(X))]
[c(ok(X))] = [1] X + [5]
>= [1] X + [5]
= [ok(c(X))]
[g(ok(X))] = [1] X + [5]
>= [1] X + [5]
= [ok(g(X))]
[d(ok(X))] = [1] X + [5]
>= [1] X + [5]
= [ok(d(X))]
[h(mark(X))] = [1] X + [4]
>= [1] X + [4]
= [mark(h(X))]
[h(ok(X))] = [1] X + [5]
>= [1] X + [5]
= [ok(h(X))]
[proper(f(X))] = [1] X + [8]
>= [1] X + [8]
= [f(proper(X))]
[proper(c(X))] = [1] X + [4]
>= [1] X + [4]
= [c(proper(X))]
[proper(g(X))] = [1] X + [4]
>= [1] X + [4]
= [g(proper(X))]
[proper(d(X))] = [1] X + [4]
>= [1] X + [4]
= [d(proper(X))]
[proper(h(X))] = [1] X + [4]
>= [1] X + [4]
= [h(proper(X))]
[top^#(mark(X))] = [1] X + [4]
>= [1] X + [4]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [1] X + [5]
> [1] X + [4]
= [c_19(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:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(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.
Trs:
{ f(ok(X)) -> ok(f(X))
, 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).
[active](x1) = [1] x1 + [0]
[f](x1) = [3] x1 + [2]
[mark](x1) = [1] x1 + [0]
[c](x1) = [1] x1 + [0]
[g](x1) = [1] x1 + [0]
[d](x1) = [1] x1 + [0]
[h](x1) = [2] x1 + [2]
[proper](x1) = [1] x1 + [0]
[ok](x1) = [1] x1 + [4]
[top^#](x1) = [3] x1 + [2]
[c_18](x1) = [1] x1 + [0]
[c_19](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [3] X + [2]
>= [3] X + [2]
= [f(active(X))]
[active(f(f(X)))] = [9] X + [8]
>= [9] X + [8]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1] X + [0]
>= [1] X + [0]
= [mark(d(X))]
[active(h(X))] = [2] X + [2]
> [1] X + [0]
= [mark(c(d(X)))]
[active(h(X))] = [2] X + [2]
>= [2] X + [2]
= [h(active(X))]
[f(mark(X))] = [3] X + [2]
>= [3] X + [2]
= [mark(f(X))]
[f(ok(X))] = [3] X + [14]
> [3] X + [6]
= [ok(f(X))]
[c(ok(X))] = [1] X + [4]
>= [1] X + [4]
= [ok(c(X))]
[g(ok(X))] = [1] X + [4]
>= [1] X + [4]
= [ok(g(X))]
[d(ok(X))] = [1] X + [4]
>= [1] X + [4]
= [ok(d(X))]
[h(mark(X))] = [2] X + [2]
>= [2] X + [2]
= [mark(h(X))]
[h(ok(X))] = [2] X + [10]
> [2] X + [6]
= [ok(h(X))]
[proper(f(X))] = [3] X + [2]
>= [3] X + [2]
= [f(proper(X))]
[proper(c(X))] = [1] X + [0]
>= [1] X + [0]
= [c(proper(X))]
[proper(g(X))] = [1] X + [0]
>= [1] X + [0]
= [g(proper(X))]
[proper(d(X))] = [1] X + [0]
>= [1] X + [0]
= [d(proper(X))]
[proper(h(X))] = [2] X + [2]
>= [2] X + [2]
= [h(proper(X))]
[top^#(mark(X))] = [3] X + [2]
>= [3] X + [2]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [3] X + [14]
> [3] X + [2]
= [c_19(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:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, f(ok(X)) -> ok(f(X))
, h(ok(X)) -> ok(h(X)) }
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:
{ active(f(X)) -> f(active(X))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(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) = [2 0] x1 + [0]
[0 0] [0]
[f](x1) = [2 0] x1 + [2]
[0 2] [0]
[mark](x1) = [1 0] x1 + [1]
[0 0] [0]
[c](x1) = [1 0] x1 + [2]
[0 4] [0]
[g](x1) = [1 0] x1 + [1]
[0 4] [0]
[d](x1) = [1 0] x1 + [0]
[0 1] [0]
[h](x1) = [1 0] x1 + [2]
[0 3] [0]
[proper](x1) = [1 0] x1 + [0]
[0 0] [0]
[ok](x1) = [1 0] x1 + [2]
[1 0] [2]
[top^#](x1) = [1 3] x1 + [7]
[0 0] [1]
[c_18](x1) = [1 1] x1 + [0]
[0 0] [0]
[c_19](x1) = [2 1] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [4 0] X + [4]
[0 0] [0]
> [4 0] X + [2]
[0 0] [0]
= [f(active(X))]
[active(f(f(X)))] = [8 0] X + [12]
[0 0] [0]
> [4 0] X + [11]
[0 0] [0]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [2 0] X + [4]
[0 0] [0]
> [1 0] X + [1]
[0 0] [0]
= [mark(d(X))]
[active(h(X))] = [2 0] X + [4]
[0 0] [0]
> [1 0] X + [3]
[0 0] [0]
= [mark(c(d(X)))]
[active(h(X))] = [2 0] X + [4]
[0 0] [0]
> [2 0] X + [2]
[0 0] [0]
= [h(active(X))]
[f(mark(X))] = [2 0] X + [4]
[0 0] [0]
> [2 0] X + [3]
[0 0] [0]
= [mark(f(X))]
[f(ok(X))] = [2 0] X + [6]
[2 0] [4]
> [2 0] X + [4]
[2 0] [4]
= [ok(f(X))]
[c(ok(X))] = [1 0] X + [4]
[4 0] [8]
>= [1 0] X + [4]
[1 0] [4]
= [ok(c(X))]
[g(ok(X))] = [1 0] X + [3]
[4 0] [8]
>= [1 0] X + [3]
[1 0] [3]
= [ok(g(X))]
[d(ok(X))] = [1 0] X + [2]
[1 0] [2]
>= [1 0] X + [2]
[1 0] [2]
= [ok(d(X))]
[h(mark(X))] = [1 0] X + [3]
[0 0] [0]
>= [1 0] X + [3]
[0 0] [0]
= [mark(h(X))]
[h(ok(X))] = [1 0] X + [4]
[3 0] [6]
>= [1 0] X + [4]
[1 0] [4]
= [ok(h(X))]
[proper(f(X))] = [2 0] X + [2]
[0 0] [0]
>= [2 0] X + [2]
[0 0] [0]
= [f(proper(X))]
[proper(c(X))] = [1 0] X + [2]
[0 0] [0]
>= [1 0] X + [2]
[0 0] [0]
= [c(proper(X))]
[proper(g(X))] = [1 0] X + [1]
[0 0] [0]
>= [1 0] X + [1]
[0 0] [0]
= [g(proper(X))]
[proper(d(X))] = [1 0] X + [0]
[0 0] [0]
>= [1 0] X + [0]
[0 0] [0]
= [d(proper(X))]
[proper(h(X))] = [1 0] X + [2]
[0 0] [0]
>= [1 0] X + [2]
[0 0] [0]
= [h(proper(X))]
[top^#(mark(X))] = [1 0] X + [8]
[0 0] [1]
>= [1 0] X + [8]
[0 0] [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [4 0] X + [15]
[0 0] [1]
>= [4 0] X + [15]
[0 0] [0]
= [c_19(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:
{ c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, h(ok(X)) -> ok(h(X)) }
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: { c(ok(X)) -> ok(c(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) = [2 0] x1 + [0]
[0 0] [0]
[f](x1) = [2 0] x1 + [0]
[0 3] [0]
[mark](x1) = [1 0] x1 + [0]
[0 0] [0]
[c](x1) = [2 0] x1 + [0]
[0 4] [0]
[g](x1) = [1 0] x1 + [0]
[0 2] [0]
[d](x1) = [1 0] x1 + [0]
[0 4] [0]
[h](x1) = [1 0] x1 + [0]
[0 1] [0]
[proper](x1) = [1 0] x1 + [0]
[0 0] [0]
[ok](x1) = [1 0] x1 + [2]
[1 0] [0]
[top^#](x1) = [7 7] x1 + [0]
[0 0] [4]
[c_18](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_19](x1) = [1 0] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [4 0] X + [0]
[0 0] [0]
>= [4 0] X + [0]
[0 0] [0]
= [f(active(X))]
[active(f(f(X)))] = [8 0] X + [0]
[0 0] [0]
>= [8 0] X + [0]
[0 0] [0]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [4 0] X + [0]
[0 0] [0]
>= [1 0] X + [0]
[0 0] [0]
= [mark(d(X))]
[active(h(X))] = [2 0] X + [0]
[0 0] [0]
>= [2 0] X + [0]
[0 0] [0]
= [mark(c(d(X)))]
[active(h(X))] = [2 0] X + [0]
[0 0] [0]
>= [2 0] X + [0]
[0 0] [0]
= [h(active(X))]
[f(mark(X))] = [2 0] X + [0]
[0 0] [0]
>= [2 0] X + [0]
[0 0] [0]
= [mark(f(X))]
[f(ok(X))] = [2 0] X + [4]
[3 0] [0]
> [2 0] X + [2]
[2 0] [0]
= [ok(f(X))]
[c(ok(X))] = [2 0] X + [4]
[4 0] [0]
> [2 0] X + [2]
[2 0] [0]
= [ok(c(X))]
[g(ok(X))] = [1 0] X + [2]
[2 0] [0]
>= [1 0] X + [2]
[1 0] [0]
= [ok(g(X))]
[d(ok(X))] = [1 0] X + [2]
[4 0] [0]
>= [1 0] X + [2]
[1 0] [0]
= [ok(d(X))]
[h(mark(X))] = [1 0] X + [0]
[0 0] [0]
>= [1 0] X + [0]
[0 0] [0]
= [mark(h(X))]
[h(ok(X))] = [1 0] X + [2]
[1 0] [0]
>= [1 0] X + [2]
[1 0] [0]
= [ok(h(X))]
[proper(f(X))] = [2 0] X + [0]
[0 0] [0]
>= [2 0] X + [0]
[0 0] [0]
= [f(proper(X))]
[proper(c(X))] = [2 0] X + [0]
[0 0] [0]
>= [2 0] X + [0]
[0 0] [0]
= [c(proper(X))]
[proper(g(X))] = [1 0] X + [0]
[0 0] [0]
>= [1 0] X + [0]
[0 0] [0]
= [g(proper(X))]
[proper(d(X))] = [1 0] X + [0]
[0 0] [0]
>= [1 0] X + [0]
[0 0] [0]
= [d(proper(X))]
[proper(h(X))] = [1 0] X + [0]
[0 0] [0]
>= [1 0] X + [0]
[0 0] [0]
= [h(proper(X))]
[top^#(mark(X))] = [7 0] X + [0]
[0 0] [4]
>= [7 0] X + [0]
[0 0] [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [14 0] X + [14]
[ 0 0] [4]
> [14 0] X + [0]
[ 0 0] [0]
= [c_19(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))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, h(ok(X)) -> ok(h(X)) }
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(mark(X)) -> mark(h(X))
, proper(f(X)) -> f(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 2] x1 + [0]
[0 1] [0]
[f](x1) = [2 0] x1 + [1]
[0 2] [1]
[mark](x1) = [1 1] x1 + [1]
[0 0] [0]
[c](x1) = [1 0] x1 + [2]
[0 1] [0]
[g](x1) = [1 0] x1 + [0]
[0 1] [0]
[d](x1) = [1 0] x1 + [0]
[0 1] [0]
[h](x1) = [2 0] x1 + [5]
[0 2] [0]
[proper](x1) = [1 1] x1 + [0]
[0 1] [0]
[ok](x1) = [1 4] x1 + [4]
[0 0] [1]
[top^#](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_18](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_19](x1) = [1 2] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [2 4] X + [3]
[0 2] [1]
> [2 4] X + [1]
[0 2] [1]
= [f(active(X))]
[active(f(f(X)))] = [4 8] X + [9]
[0 4] [3]
>= [4 4] X + [9]
[0 0] [0]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1 2] X + [2]
[0 1] [0]
> [1 1] X + [1]
[0 0] [0]
= [mark(d(X))]
[active(h(X))] = [2 4] X + [5]
[0 2] [0]
> [1 1] X + [3]
[0 0] [0]
= [mark(c(d(X)))]
[active(h(X))] = [2 4] X + [5]
[0 2] [0]
>= [2 4] X + [5]
[0 2] [0]
= [h(active(X))]
[f(mark(X))] = [2 2] X + [3]
[0 0] [1]
>= [2 2] X + [3]
[0 0] [0]
= [mark(f(X))]
[f(ok(X))] = [2 8] X + [9]
[0 0] [3]
>= [2 8] X + [9]
[0 0] [1]
= [ok(f(X))]
[c(ok(X))] = [1 4] X + [6]
[0 0] [1]
>= [1 4] X + [6]
[0 0] [1]
= [ok(c(X))]
[g(ok(X))] = [1 4] X + [4]
[0 0] [1]
>= [1 4] X + [4]
[0 0] [1]
= [ok(g(X))]
[d(ok(X))] = [1 4] X + [4]
[0 0] [1]
>= [1 4] X + [4]
[0 0] [1]
= [ok(d(X))]
[h(mark(X))] = [2 2] X + [7]
[0 0] [0]
> [2 2] X + [6]
[0 0] [0]
= [mark(h(X))]
[h(ok(X))] = [2 8] X + [13]
[0 0] [2]
> [2 8] X + [9]
[0 0] [1]
= [ok(h(X))]
[proper(f(X))] = [2 2] X + [2]
[0 2] [1]
> [2 2] X + [1]
[0 2] [1]
= [f(proper(X))]
[proper(c(X))] = [1 1] X + [2]
[0 1] [0]
>= [1 1] X + [2]
[0 1] [0]
= [c(proper(X))]
[proper(g(X))] = [1 1] X + [0]
[0 1] [0]
>= [1 1] X + [0]
[0 1] [0]
= [g(proper(X))]
[proper(d(X))] = [1 1] X + [0]
[0 1] [0]
>= [1 1] X + [0]
[0 1] [0]
= [d(proper(X))]
[proper(h(X))] = [2 2] X + [5]
[0 2] [0]
>= [2 2] X + [5]
[0 2] [0]
= [h(proper(X))]
[top^#(mark(X))] = [1 1] X + [1]
[0 0] [0]
> [1 1] X + [0]
[0 0] [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [1 4] X + [4]
[0 0] [1]
> [1 4] X + [0]
[0 0] [0]
= [c_19(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))
, d(ok(X)) -> ok(d(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X)) }
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 + [0]
[0 1] [0]
[f](x1) = [2 3] x1 + [2]
[3 2] [3]
[mark](x1) = [1 0] x1 + [0]
[0 1] [1]
[c](x1) = [1 0] x1 + [1]
[0 0] [1]
[g](x1) = [2 0] x1 + [1]
[0 0] [0]
[d](x1) = [1 0] x1 + [1]
[0 0] [0]
[h](x1) = [2 0] x1 + [4]
[0 2] [3]
[proper](x1) = [1 0] x1 + [0]
[0 1] [0]
[ok](x1) = [1 0] x1 + [3]
[0 1] [0]
[top^#](x1) = [2 0] x1 + [0]
[1 0] [0]
[c_18](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_19](x1) = [1 0] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [2 3] X + [2]
[3 2] [3]
>= [2 3] X + [2]
[3 2] [3]
= [f(active(X))]
[active(f(f(X)))] = [13 12] X + [15]
[12 13] [15]
> [8 12] X + [13]
[0 0] [2]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1 0] X + [1]
[0 0] [1]
>= [1 0] X + [1]
[0 0] [1]
= [mark(d(X))]
[active(h(X))] = [2 0] X + [4]
[0 2] [3]
> [1 0] X + [2]
[0 0] [2]
= [mark(c(d(X)))]
[active(h(X))] = [2 0] X + [4]
[0 2] [3]
>= [2 0] X + [4]
[0 2] [3]
= [h(active(X))]
[f(mark(X))] = [2 3] X + [5]
[3 2] [5]
> [2 3] X + [2]
[3 2] [4]
= [mark(f(X))]
[f(ok(X))] = [2 3] X + [8]
[3 2] [12]
> [2 3] X + [5]
[3 2] [3]
= [ok(f(X))]
[c(ok(X))] = [1 0] X + [4]
[0 0] [1]
>= [1 0] X + [4]
[0 0] [1]
= [ok(c(X))]
[g(ok(X))] = [2 0] X + [7]
[0 0] [0]
> [2 0] X + [4]
[0 0] [0]
= [ok(g(X))]
[d(ok(X))] = [1 0] X + [4]
[0 0] [0]
>= [1 0] X + [4]
[0 0] [0]
= [ok(d(X))]
[h(mark(X))] = [2 0] X + [4]
[0 2] [5]
>= [2 0] X + [4]
[0 2] [4]
= [mark(h(X))]
[h(ok(X))] = [2 0] X + [10]
[0 2] [3]
> [2 0] X + [7]
[0 2] [3]
= [ok(h(X))]
[proper(f(X))] = [2 3] X + [2]
[3 2] [3]
>= [2 3] X + [2]
[3 2] [3]
= [f(proper(X))]
[proper(c(X))] = [1 0] X + [1]
[0 0] [1]
>= [1 0] X + [1]
[0 0] [1]
= [c(proper(X))]
[proper(g(X))] = [2 0] X + [1]
[0 0] [0]
>= [2 0] X + [1]
[0 0] [0]
= [g(proper(X))]
[proper(d(X))] = [1 0] X + [1]
[0 0] [0]
>= [1 0] X + [1]
[0 0] [0]
= [d(proper(X))]
[proper(h(X))] = [2 0] X + [4]
[0 2] [3]
>= [2 0] X + [4]
[0 2] [3]
= [h(proper(X))]
[top^#(mark(X))] = [2 0] X + [0]
[1 0] [0]
>= [2 0] X + [0]
[0 0] [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [2 0] X + [6]
[1 0] [3]
> [2 0] X + [0]
[0 0] [0]
= [c_19(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:
{ d(ok(X)) -> ok(d(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X)) }
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: { d(ok(X)) -> ok(d(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) = [2 0] x1 + [2]
[0 0] [0]
[f](x1) = [1 0] x1 + [3]
[0 3] [0]
[mark](x1) = [1 0] x1 + [1]
[0 0] [0]
[c](x1) = [1 0] x1 + [0]
[0 1] [0]
[g](x1) = [2 0] x1 + [4]
[0 3] [0]
[d](x1) = [2 0] x1 + [0]
[0 4] [0]
[h](x1) = [2 0] x1 + [2]
[0 5] [0]
[proper](x1) = [1 0] x1 + [0]
[0 0] [0]
[ok](x1) = [1 0] x1 + [2]
[1 0] [2]
[top^#](x1) = [2 4] x1 + [3]
[0 0] [1]
[c_18](x1) = [1 1] x1 + [0]
[0 0] [0]
[c_19](x1) = [1 3] x1 + [4]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [2 0] X + [8]
[0 0] [0]
> [2 0] X + [5]
[0 0] [0]
= [f(active(X))]
[active(f(f(X)))] = [2 0] X + [14]
[0 0] [0]
>= [2 0] X + [14]
[0 0] [0]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [2 0] X + [2]
[0 0] [0]
> [2 0] X + [1]
[0 0] [0]
= [mark(d(X))]
[active(h(X))] = [4 0] X + [6]
[0 0] [0]
> [2 0] X + [1]
[0 0] [0]
= [mark(c(d(X)))]
[active(h(X))] = [4 0] X + [6]
[0 0] [0]
>= [4 0] X + [6]
[0 0] [0]
= [h(active(X))]
[f(mark(X))] = [1 0] X + [4]
[0 0] [0]
>= [1 0] X + [4]
[0 0] [0]
= [mark(f(X))]
[f(ok(X))] = [1 0] X + [5]
[3 0] [6]
>= [1 0] X + [5]
[1 0] [5]
= [ok(f(X))]
[c(ok(X))] = [1 0] X + [2]
[1 0] [2]
>= [1 0] X + [2]
[1 0] [2]
= [ok(c(X))]
[g(ok(X))] = [2 0] X + [8]
[3 0] [6]
> [2 0] X + [6]
[2 0] [6]
= [ok(g(X))]
[d(ok(X))] = [2 0] X + [4]
[4 0] [8]
> [2 0] X + [2]
[2 0] [2]
= [ok(d(X))]
[h(mark(X))] = [2 0] X + [4]
[0 0] [0]
> [2 0] X + [3]
[0 0] [0]
= [mark(h(X))]
[h(ok(X))] = [2 0] X + [6]
[5 0] [10]
> [2 0] X + [4]
[2 0] [4]
= [ok(h(X))]
[proper(f(X))] = [1 0] X + [3]
[0 0] [0]
>= [1 0] X + [3]
[0 0] [0]
= [f(proper(X))]
[proper(c(X))] = [1 0] X + [0]
[0 0] [0]
>= [1 0] X + [0]
[0 0] [0]
= [c(proper(X))]
[proper(g(X))] = [2 0] X + [4]
[0 0] [0]
>= [2 0] X + [4]
[0 0] [0]
= [g(proper(X))]
[proper(d(X))] = [2 0] X + [0]
[0 0] [0]
>= [2 0] X + [0]
[0 0] [0]
= [d(proper(X))]
[proper(h(X))] = [2 0] X + [2]
[0 0] [0]
>= [2 0] X + [2]
[0 0] [0]
= [h(proper(X))]
[top^#(mark(X))] = [2 0] X + [5]
[0 0] [1]
> [2 0] X + [4]
[0 0] [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [6 0] X + [15]
[0 0] [1]
> [4 0] X + [14]
[0 0] [0]
= [c_19(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:
{ proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X)) }
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 + [0]
[1 0] [1]
[f](x1) = [3 0] x1 + [2]
[0 3] [0]
[mark](x1) = [1 0] x1 + [0]
[1 0] [1]
[c](x1) = [1 0] x1 + [0]
[0 1] [0]
[g](x1) = [1 0] x1 + [0]
[0 1] [0]
[d](x1) = [1 0] x1 + [0]
[0 1] [0]
[h](x1) = [5 0] x1 + [4]
[0 5] [0]
[proper](x1) = [3 0] x1 + [0]
[0 0] [0]
[ok](x1) = [1 0] x1 + [2]
[1 0] [2]
[top^#](x1) = [1 3] x1 + [7]
[1 0] [2]
[c_18](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_19](x1) = [1 0] x1 + [4]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [3 0] X + [2]
[3 0] [3]
>= [3 0] X + [2]
[3 0] [3]
= [f(active(X))]
[active(f(f(X)))] = [9 0] X + [8]
[9 0] [9]
>= [9 0] X + [8]
[9 0] [9]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1 0] X + [0]
[1 0] [1]
>= [1 0] X + [0]
[1 0] [1]
= [mark(d(X))]
[active(h(X))] = [5 0] X + [4]
[5 0] [5]
> [1 0] X + [0]
[1 0] [1]
= [mark(c(d(X)))]
[active(h(X))] = [5 0] X + [4]
[5 0] [5]
>= [5 0] X + [4]
[5 0] [5]
= [h(active(X))]
[f(mark(X))] = [3 0] X + [2]
[3 0] [3]
>= [3 0] X + [2]
[3 0] [3]
= [mark(f(X))]
[f(ok(X))] = [3 0] X + [8]
[3 0] [6]
> [3 0] X + [4]
[3 0] [4]
= [ok(f(X))]
[c(ok(X))] = [1 0] X + [2]
[1 0] [2]
>= [1 0] X + [2]
[1 0] [2]
= [ok(c(X))]
[g(ok(X))] = [1 0] X + [2]
[1 0] [2]
>= [1 0] X + [2]
[1 0] [2]
= [ok(g(X))]
[d(ok(X))] = [1 0] X + [2]
[1 0] [2]
>= [1 0] X + [2]
[1 0] [2]
= [ok(d(X))]
[h(mark(X))] = [5 0] X + [4]
[5 0] [5]
>= [5 0] X + [4]
[5 0] [5]
= [mark(h(X))]
[h(ok(X))] = [5 0] X + [14]
[5 0] [10]
> [5 0] X + [6]
[5 0] [6]
= [ok(h(X))]
[proper(f(X))] = [9 0] X + [6]
[0 0] [0]
> [9 0] X + [2]
[0 0] [0]
= [f(proper(X))]
[proper(c(X))] = [3 0] X + [0]
[0 0] [0]
>= [3 0] X + [0]
[0 0] [0]
= [c(proper(X))]
[proper(g(X))] = [3 0] X + [0]
[0 0] [0]
>= [3 0] X + [0]
[0 0] [0]
= [g(proper(X))]
[proper(d(X))] = [3 0] X + [0]
[0 0] [0]
>= [3 0] X + [0]
[0 0] [0]
= [d(proper(X))]
[proper(h(X))] = [15 0] X + [12]
[ 0 0] [0]
> [15 0] X + [4]
[ 0 0] [0]
= [h(proper(X))]
[top^#(mark(X))] = [4 0] X + [10]
[1 0] [2]
> [3 0] X + [7]
[0 0] [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [4 0] X + [15]
[1 0] [4]
> [4 0] X + [14]
[0 0] [0]
= [c_19(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:
{ proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(h(X)) -> h(proper(X)) }
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 0] x1 + [1]
[1 0] [2]
[f](x1) = [1 0] x1 + [0]
[0 1] [0]
[mark](x1) = [1 0] x1 + [0]
[1 0] [0]
[c](x1) = [1 0] x1 + [0]
[0 1] [0]
[g](x1) = [1 0] x1 + [1]
[0 3] [0]
[d](x1) = [1 0] x1 + [0]
[0 1] [0]
[h](x1) = [1 0] x1 + [0]
[0 1] [0]
[proper](x1) = [4 0] x1 + [0]
[0 0] [0]
[ok](x1) = [1 0] x1 + [4]
[1 0] [1]
[top^#](x1) = [2 6] x1 + [0]
[0 0] [0]
[c_18](x1) = [1 1] x1 + [0]
[0 0] [0]
[c_19](x1) = [1 1] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [1 0] X + [1]
[1 0] [2]
>= [1 0] X + [1]
[1 0] [2]
= [f(active(X))]
[active(f(f(X)))] = [1 0] X + [1]
[1 0] [2]
>= [1 0] X + [1]
[1 0] [1]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1 0] X + [1]
[1 0] [2]
> [1 0] X + [0]
[1 0] [0]
= [mark(d(X))]
[active(h(X))] = [1 0] X + [1]
[1 0] [2]
> [1 0] X + [0]
[1 0] [0]
= [mark(c(d(X)))]
[active(h(X))] = [1 0] X + [1]
[1 0] [2]
>= [1 0] X + [1]
[1 0] [2]
= [h(active(X))]
[f(mark(X))] = [1 0] X + [0]
[1 0] [0]
>= [1 0] X + [0]
[1 0] [0]
= [mark(f(X))]
[f(ok(X))] = [1 0] X + [4]
[1 0] [1]
>= [1 0] X + [4]
[1 0] [1]
= [ok(f(X))]
[c(ok(X))] = [1 0] X + [4]
[1 0] [1]
>= [1 0] X + [4]
[1 0] [1]
= [ok(c(X))]
[g(ok(X))] = [1 0] X + [5]
[3 0] [3]
>= [1 0] X + [5]
[1 0] [2]
= [ok(g(X))]
[d(ok(X))] = [1 0] X + [4]
[1 0] [1]
>= [1 0] X + [4]
[1 0] [1]
= [ok(d(X))]
[h(mark(X))] = [1 0] X + [0]
[1 0] [0]
>= [1 0] X + [0]
[1 0] [0]
= [mark(h(X))]
[h(ok(X))] = [1 0] X + [4]
[1 0] [1]
>= [1 0] X + [4]
[1 0] [1]
= [ok(h(X))]
[proper(f(X))] = [4 0] X + [0]
[0 0] [0]
>= [4 0] X + [0]
[0 0] [0]
= [f(proper(X))]
[proper(c(X))] = [4 0] X + [0]
[0 0] [0]
>= [4 0] X + [0]
[0 0] [0]
= [c(proper(X))]
[proper(g(X))] = [4 0] X + [4]
[0 0] [0]
> [4 0] X + [1]
[0 0] [0]
= [g(proper(X))]
[proper(d(X))] = [4 0] X + [0]
[0 0] [0]
>= [4 0] X + [0]
[0 0] [0]
= [d(proper(X))]
[proper(h(X))] = [4 0] X + [0]
[0 0] [0]
>= [4 0] X + [0]
[0 0] [0]
= [h(proper(X))]
[top^#(mark(X))] = [8 0] X + [0]
[0 0] [0]
>= [8 0] X + [0]
[0 0] [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [8 0] X + [14]
[0 0] [0]
>= [8 0] X + [14]
[0 0] [0]
= [c_19(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:
{ proper(c(X)) -> c(proper(X))
, proper(d(X)) -> d(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(h(X)) -> h(proper(X)) }
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(d(X)) -> d(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 + [1]
[1 0] [2]
[f](x1) = [1 0] x1 + [0]
[0 1] [0]
[mark](x1) = [1 0] x1 + [0]
[1 0] [1]
[c](x1) = [1 0] x1 + [0]
[0 1] [0]
[g](x1) = [1 0] x1 + [0]
[0 1] [0]
[d](x1) = [1 0] x1 + [1]
[0 2] [0]
[h](x1) = [1 0] x1 + [0]
[0 1] [0]
[proper](x1) = [4 0] x1 + [0]
[0 0] [0]
[ok](x1) = [1 0] x1 + [3]
[1 0] [3]
[top^#](x1) = [1 4] x1 + [0]
[0 0] [2]
[c_18](x1) = [1 1] x1 + [2]
[0 0] [0]
[c_19](x1) = [1 1] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [1 0] X + [1]
[1 0] [2]
>= [1 0] X + [1]
[1 0] [2]
= [f(active(X))]
[active(f(f(X)))] = [1 0] X + [1]
[1 0] [2]
> [1 0] X + [0]
[1 0] [1]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1 0] X + [1]
[1 0] [2]
>= [1 0] X + [1]
[1 0] [2]
= [mark(d(X))]
[active(h(X))] = [1 0] X + [1]
[1 0] [2]
>= [1 0] X + [1]
[1 0] [2]
= [mark(c(d(X)))]
[active(h(X))] = [1 0] X + [1]
[1 0] [2]
>= [1 0] X + [1]
[1 0] [2]
= [h(active(X))]
[f(mark(X))] = [1 0] X + [0]
[1 0] [1]
>= [1 0] X + [0]
[1 0] [1]
= [mark(f(X))]
[f(ok(X))] = [1 0] X + [3]
[1 0] [3]
>= [1 0] X + [3]
[1 0] [3]
= [ok(f(X))]
[c(ok(X))] = [1 0] X + [3]
[1 0] [3]
>= [1 0] X + [3]
[1 0] [3]
= [ok(c(X))]
[g(ok(X))] = [1 0] X + [3]
[1 0] [3]
>= [1 0] X + [3]
[1 0] [3]
= [ok(g(X))]
[d(ok(X))] = [1 0] X + [4]
[2 0] [6]
>= [1 0] X + [4]
[1 0] [4]
= [ok(d(X))]
[h(mark(X))] = [1 0] X + [0]
[1 0] [1]
>= [1 0] X + [0]
[1 0] [1]
= [mark(h(X))]
[h(ok(X))] = [1 0] X + [3]
[1 0] [3]
>= [1 0] X + [3]
[1 0] [3]
= [ok(h(X))]
[proper(f(X))] = [4 0] X + [0]
[0 0] [0]
>= [4 0] X + [0]
[0 0] [0]
= [f(proper(X))]
[proper(c(X))] = [4 0] X + [0]
[0 0] [0]
>= [4 0] X + [0]
[0 0] [0]
= [c(proper(X))]
[proper(g(X))] = [4 0] X + [0]
[0 0] [0]
>= [4 0] X + [0]
[0 0] [0]
= [g(proper(X))]
[proper(d(X))] = [4 0] X + [4]
[0 0] [0]
> [4 0] X + [1]
[0 0] [0]
= [d(proper(X))]
[proper(h(X))] = [4 0] X + [0]
[0 0] [0]
>= [4 0] X + [0]
[0 0] [0]
= [h(proper(X))]
[top^#(mark(X))] = [5 0] X + [4]
[0 0] [2]
>= [4 0] X + [4]
[0 0] [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [5 0] X + [15]
[0 0] [2]
> [5 0] X + [11]
[0 0] [0]
= [c_19(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: { proper(c(X)) -> c(proper(X)) }
Weak DPs:
{ top^#(mark(X)) -> c_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
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(c(X)) -> c(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 + [3]
[1 0] [2]
[f](x1) = [1 0] x1 + [0]
[0 1] [0]
[mark](x1) = [1 0] x1 + [1]
[1 0] [0]
[c](x1) = [1 0] x1 + [2]
[0 4] [0]
[g](x1) = [1 0] x1 + [0]
[0 1] [0]
[d](x1) = [1 0] x1 + [0]
[0 1] [0]
[h](x1) = [1 0] x1 + [0]
[0 1] [0]
[proper](x1) = [3 0] x1 + [1]
[0 0] [0]
[ok](x1) = [1 0] x1 + [3]
[1 0] [2]
[top^#](x1) = [1 6] x1 + [0]
[1 3] [4]
[c_18](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_19](x1) = [1 0] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[active(f(X))] = [1 0] X + [3]
[1 0] [2]
>= [1 0] X + [3]
[1 0] [2]
= [f(active(X))]
[active(f(f(X)))] = [1 0] X + [3]
[1 0] [2]
>= [1 0] X + [3]
[1 0] [2]
= [mark(c(f(g(f(X)))))]
[active(c(X))] = [1 0] X + [5]
[1 0] [4]
> [1 0] X + [1]
[1 0] [0]
= [mark(d(X))]
[active(h(X))] = [1 0] X + [3]
[1 0] [2]
>= [1 0] X + [3]
[1 0] [2]
= [mark(c(d(X)))]
[active(h(X))] = [1 0] X + [3]
[1 0] [2]
>= [1 0] X + [3]
[1 0] [2]
= [h(active(X))]
[f(mark(X))] = [1 0] X + [1]
[1 0] [0]
>= [1 0] X + [1]
[1 0] [0]
= [mark(f(X))]
[f(ok(X))] = [1 0] X + [3]
[1 0] [2]
>= [1 0] X + [3]
[1 0] [2]
= [ok(f(X))]
[c(ok(X))] = [1 0] X + [5]
[4 0] [8]
>= [1 0] X + [5]
[1 0] [4]
= [ok(c(X))]
[g(ok(X))] = [1 0] X + [3]
[1 0] [2]
>= [1 0] X + [3]
[1 0] [2]
= [ok(g(X))]
[d(ok(X))] = [1 0] X + [3]
[1 0] [2]
>= [1 0] X + [3]
[1 0] [2]
= [ok(d(X))]
[h(mark(X))] = [1 0] X + [1]
[1 0] [0]
>= [1 0] X + [1]
[1 0] [0]
= [mark(h(X))]
[h(ok(X))] = [1 0] X + [3]
[1 0] [2]
>= [1 0] X + [3]
[1 0] [2]
= [ok(h(X))]
[proper(f(X))] = [3 0] X + [1]
[0 0] [0]
>= [3 0] X + [1]
[0 0] [0]
= [f(proper(X))]
[proper(c(X))] = [3 0] X + [7]
[0 0] [0]
> [3 0] X + [3]
[0 0] [0]
= [c(proper(X))]
[proper(g(X))] = [3 0] X + [1]
[0 0] [0]
>= [3 0] X + [1]
[0 0] [0]
= [g(proper(X))]
[proper(d(X))] = [3 0] X + [1]
[0 0] [0]
>= [3 0] X + [1]
[0 0] [0]
= [d(proper(X))]
[proper(h(X))] = [3 0] X + [1]
[0 0] [0]
>= [3 0] X + [1]
[0 0] [0]
= [h(proper(X))]
[top^#(mark(X))] = [7 0] X + [1]
[4 0] [5]
>= [3 0] X + [1]
[0 0] [0]
= [c_18(top^#(proper(X)))]
[top^#(ok(X))] = [7 0] X + [15]
[4 0] [13]
>= [7 0] X + [15]
[0 0] [0]
= [c_19(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_18(top^#(proper(X)))
, top^#(ok(X)) -> c_19(top^#(active(X))) }
Weak Trs:
{ active(f(X)) -> f(active(X))
, active(f(f(X))) -> mark(c(f(g(f(X)))))
, active(c(X)) -> mark(d(X))
, active(h(X)) -> mark(c(d(X)))
, active(h(X)) -> h(active(X))
, f(mark(X)) -> mark(f(X))
, f(ok(X)) -> ok(f(X))
, c(ok(X)) -> ok(c(X))
, g(ok(X)) -> ok(g(X))
, d(ok(X)) -> ok(d(X))
, h(mark(X)) -> mark(h(X))
, h(ok(X)) -> ok(h(X))
, proper(f(X)) -> f(proper(X))
, proper(c(X)) -> c(proper(X))
, proper(g(X)) -> g(proper(X))
, proper(d(X)) -> d(proper(X))
, proper(h(X)) -> h(proper(X)) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))