We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z))
, rev(nil()) -> nil()
, rev(unit(x)) -> unit(x)
, rev(++(x, y)) -> ++(rev(y), rev(x))
, rev(rev(x)) -> x }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following dependency tuples:
Strict DPs:
{ flatten^#(flatten(x)) -> c_1(flatten^#(x))
, flatten^#(nil()) -> c_2()
, flatten^#(unit(x)) -> c_3(flatten^#(x))
, flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, ++^#(x, nil()) -> c_6()
, ++^#(nil(), y) -> c_7()
, ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
, rev^#(nil()) -> c_9()
, rev^#(unit(x)) -> c_10()
, rev^#(++(x, y)) -> c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x))
, rev^#(rev(x)) -> c_12() }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ flatten^#(flatten(x)) -> c_1(flatten^#(x))
, flatten^#(nil()) -> c_2()
, flatten^#(unit(x)) -> c_3(flatten^#(x))
, flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, ++^#(x, nil()) -> c_6()
, ++^#(nil(), y) -> c_7()
, ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
, rev^#(nil()) -> c_9()
, rev^#(unit(x)) -> c_10()
, rev^#(++(x, y)) -> c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x))
, rev^#(rev(x)) -> c_12() }
Weak Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z))
, rev(nil()) -> nil()
, rev(unit(x)) -> unit(x)
, rev(++(x, y)) -> ++(rev(y), rev(x))
, rev(rev(x)) -> x }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Consider the dependency graph:
1: flatten^#(flatten(x)) -> c_1(flatten^#(x))
2: flatten^#(nil()) -> c_2()
3: flatten^#(unit(x)) -> c_3(flatten^#(x))
-->_1 flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5
-->_1 flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4
-->_1 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
-->_1 flatten^#(nil()) -> c_2() :2
-->_1 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
4: flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
-->_1 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8
-->_3 flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5
-->_1 ++^#(nil(), y) -> c_7() :7
-->_1 ++^#(x, nil()) -> c_6() :6
-->_3 flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4
-->_3 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
-->_2 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
-->_3 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
-->_2 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
5: flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
-->_1 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8
-->_1 ++^#(nil(), y) -> c_7() :7
-->_1 ++^#(x, nil()) -> c_6() :6
-->_3 flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5
-->_2 flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5
-->_3 flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4
-->_2 flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4
-->_3 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
-->_2 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
-->_2 flatten^#(nil()) -> c_2() :2
-->_3 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
-->_2 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
6: ++^#(x, nil()) -> c_6()
7: ++^#(nil(), y) -> c_7()
8: ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
-->_2 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8
-->_2 ++^#(x, nil()) -> c_6() :6
-->_1 ++^#(x, nil()) -> c_6() :6
9: rev^#(nil()) -> c_9()
10: rev^#(unit(x)) -> c_10()
11: rev^#(++(x, y)) ->
c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x))
-->_3 rev^#(rev(x)) -> c_12() :12
-->_2 rev^#(rev(x)) -> c_12() :12
-->_2 rev^#(++(x, y)) ->
c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x)) :11
-->_3 rev^#(unit(x)) -> c_10() :10
-->_2 rev^#(unit(x)) -> c_10() :10
-->_1 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8
-->_1 ++^#(nil(), y) -> c_7() :7
-->_1 ++^#(x, nil()) -> c_6() :6
12: rev^#(rev(x)) -> c_12()
Only the nodes {2,3,5,8,6,7,4,1,9,10} are reachable from nodes
{2,3,6,7,9,10} 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(1),O(n^1)).
Strict DPs:
{ flatten^#(flatten(x)) -> c_1(flatten^#(x))
, flatten^#(nil()) -> c_2()
, flatten^#(unit(x)) -> c_3(flatten^#(x))
, flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, ++^#(x, nil()) -> c_6()
, ++^#(nil(), y) -> c_7()
, ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
, rev^#(nil()) -> c_9()
, rev^#(unit(x)) -> c_10() }
Weak Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z))
, rev(nil()) -> nil()
, rev(unit(x)) -> unit(x)
, rev(++(x, y)) -> ++(rev(y), rev(x))
, rev(rev(x)) -> x }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {1,2,6,7,9,10} by
applications of Pre({1,2,6,7,9,10}) = {3,4,5,8}. Here rules are
labeled as follows:
DPs:
{ 1: flatten^#(flatten(x)) -> c_1(flatten^#(x))
, 2: flatten^#(nil()) -> c_2()
, 3: flatten^#(unit(x)) -> c_3(flatten^#(x))
, 4: flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, 5: flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, 6: ++^#(x, nil()) -> c_6()
, 7: ++^#(nil(), y) -> c_7()
, 8: ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
, 9: rev^#(nil()) -> c_9()
, 10: rev^#(unit(x)) -> c_10() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ flatten^#(unit(x)) -> c_3(flatten^#(x))
, flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) }
Weak DPs:
{ flatten^#(flatten(x)) -> c_1(flatten^#(x))
, flatten^#(nil()) -> c_2()
, ++^#(x, nil()) -> c_6()
, ++^#(nil(), y) -> c_7()
, rev^#(nil()) -> c_9()
, rev^#(unit(x)) -> c_10() }
Weak Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z))
, rev(nil()) -> nil()
, rev(unit(x)) -> unit(x)
, rev(++(x, y)) -> ++(rev(y), rev(x))
, rev(rev(x)) -> 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.
{ flatten^#(flatten(x)) -> c_1(flatten^#(x))
, flatten^#(nil()) -> c_2()
, ++^#(x, nil()) -> c_6()
, ++^#(nil(), y) -> c_7()
, rev^#(nil()) -> c_9()
, rev^#(unit(x)) -> c_10() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ flatten^#(unit(x)) -> c_3(flatten^#(x))
, flatten^#(++(x, y)) ->
c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) }
Weak Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z))
, rev(nil()) -> nil()
, rev(unit(x)) -> unit(x)
, rev(++(x, y)) -> ++(rev(y), rev(x))
, rev(rev(x)) -> 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:
{ ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ flatten^#(unit(x)) -> c_1(flatten^#(x))
, flatten^#(++(x, y)) ->
c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, ++^#(++(x, y), z) -> c_4(++^#(y, z)) }
Weak Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z))
, rev(nil()) -> nil()
, rev(unit(x)) -> unit(x)
, rev(++(x, y)) -> ++(rev(y), rev(x))
, rev(rev(x)) -> x }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ flatten^#(unit(x)) -> c_1(flatten^#(x))
, flatten^#(++(x, y)) ->
c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, ++^#(++(x, y), z) -> c_4(++^#(y, z)) }
Weak Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z)) }
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:
{ 4: ++^#(++(x, y), z) -> c_4(++^#(y, z)) }
Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2, 3}, Uargs(c_3) = {1, 2, 3},
Uargs(c_4) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[flatten](x1) = [3] x1 + [2]
[nil] = [0]
[unit](x1) = [1] x1 + [0]
[++](x1, x2) = [3] x1 + [1] x2 + [3]
[flatten^#](x1) = [4] x1 + [2]
[++^#](x1, x2) = [2] x1 + [6]
[c_1](x1) = [1] x1 + [0]
[c_2](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
[c_3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
[c_4](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[flatten(flatten(x))] = [9] x + [8]
> [3] x + [2]
= [flatten(x)]
[flatten(nil())] = [2]
> [0]
= [nil()]
[flatten(unit(x))] = [3] x + [2]
>= [3] x + [2]
= [flatten(x)]
[flatten(++(x, y))] = [9] x + [3] y + [11]
>= [9] x + [3] y + [11]
= [++(flatten(x), flatten(y))]
[flatten(++(unit(x), y))] = [9] x + [3] y + [11]
>= [9] x + [3] y + [11]
= [++(flatten(x), flatten(y))]
[++(x, nil())] = [3] x + [3]
> [1] x + [0]
= [x]
[++(nil(), y)] = [1] y + [3]
> [1] y + [0]
= [y]
[++(++(x, y), z)] = [9] x + [3] y + [1] z + [12]
> [3] x + [3] y + [1] z + [6]
= [++(x, ++(y, z))]
[flatten^#(unit(x))] = [4] x + [2]
>= [4] x + [2]
= [c_1(flatten^#(x))]
[flatten^#(++(x, y))] = [12] x + [4] y + [14]
>= [10] x + [4] y + [14]
= [c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))]
[flatten^#(++(unit(x), y))] = [12] x + [4] y + [14]
>= [10] x + [4] y + [14]
= [c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))]
[++^#(++(x, y), z)] = [6] x + [2] y + [12]
> [2] y + [7]
= [c_4(++^#(y, z))]
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:
{ flatten^#(unit(x)) -> c_1(flatten^#(x))
, flatten^#(++(x, y)) ->
c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) }
Weak DPs: { ++^#(++(x, y), z) -> c_4(++^#(y, z)) }
Weak Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z)) }
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.
{ ++^#(++(x, y), z) -> c_4(++^#(y, z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ flatten^#(unit(x)) -> c_1(flatten^#(x))
, flatten^#(++(x, y)) ->
c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) }
Weak Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z)) }
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:
{ flatten^#(++(x, y)) ->
c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ flatten^#(unit(x)) -> c_1(flatten^#(x))
, flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) }
Weak Trs:
{ flatten(flatten(x)) -> flatten(x)
, flatten(nil()) -> nil()
, flatten(unit(x)) -> flatten(x)
, flatten(++(x, y)) -> ++(flatten(x), flatten(y))
, flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
, ++(x, nil()) -> x
, ++(nil(), y) -> y
, ++(++(x, y), z) -> ++(x, ++(y, z)) }
Obligation:
innermost 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:
{ flatten^#(unit(x)) -> c_1(flatten^#(x))
, flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) }
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:
{ 2: flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y))
, 3: flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[flatten](x1) = [0]
[nil] = [0]
[unit](x1) = [1] x1 + [0]
[++](x1, x2) = [4] x1 + [4] x2 + [4]
[flatten^#](x1) = [2] x1 + [0]
[++^#](x1, x2) = [0]
[c_1](x1) = [0]
[c_2](x1, x2, x3) = [0]
[c_3](x1, x2, x3) = [0]
[c_4](x1) = [0]
[c] = [0]
[c_1](x1) = [1] x1 + [0]
[c_2](x1, x2) = [4] x1 + [4] x2 + [0]
[c_3](x1, x2) = [1] x1 + [1] x2 + [1]
The order satisfies the following ordering constraints:
[flatten^#(unit(x))] = [2] x + [0]
>= [2] x + [0]
= [c_1(flatten^#(x))]
[flatten^#(++(x, y))] = [8] x + [8] y + [8]
> [8] x + [8] y + [0]
= [c_2(flatten^#(x), flatten^#(y))]
[flatten^#(++(unit(x), y))] = [8] x + [8] y + [8]
> [2] x + [2] y + [1]
= [c_3(flatten^#(x), flatten^#(y))]
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: { flatten^#(unit(x)) -> c_1(flatten^#(x)) }
Weak DPs:
{ flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) }
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: flatten^#(unit(x)) -> c_1(flatten^#(x))
, 3: flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[flatten](x1) = [0]
[nil] = [0]
[unit](x1) = [1] x1 + [2]
[++](x1, x2) = [1] x1 + [2] x2 + [2]
[flatten^#](x1) = [3] x1 + [3]
[++^#](x1, x2) = [0]
[c_1](x1) = [0]
[c_2](x1, x2, x3) = [0]
[c_3](x1, x2, x3) = [0]
[c_4](x1) = [0]
[c] = [0]
[c_1](x1) = [1] x1 + [4]
[c_2](x1, x2) = [1] x1 + [2] x2 + [0]
[c_3](x1, x2) = [1] x1 + [1] x2 + [4]
The order satisfies the following ordering constraints:
[flatten^#(unit(x))] = [3] x + [9]
> [3] x + [7]
= [c_1(flatten^#(x))]
[flatten^#(++(x, y))] = [3] x + [6] y + [9]
>= [3] x + [6] y + [9]
= [c_2(flatten^#(x), flatten^#(y))]
[flatten^#(++(unit(x), y))] = [3] x + [6] y + [15]
> [3] x + [3] y + [10]
= [c_3(flatten^#(x), flatten^#(y))]
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:
{ flatten^#(unit(x)) -> c_1(flatten^#(x))
, flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) }
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.
{ flatten^#(unit(x)) -> c_1(flatten^#(x))
, flatten^#(++(x, y)) -> c_2(flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) -> c_3(flatten^#(x), flatten^#(y)) }
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^1))