We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ selects(x', revprefix, Cons(x, xs)) ->
Cons(Cons(x', revapp(revprefix, Cons(x, xs))),
selects(x, Cons(x', revprefix), xs))
, selects(x, revprefix, Nil()) ->
Cons(Cons(x, revapp(revprefix, Nil())), Nil())
, revapp(Cons(x, xs), rest) -> revapp(xs, Cons(x, rest))
, revapp(Nil(), rest) -> rest
, select(Cons(x, xs)) -> selects(x, Nil(), xs)
, select(Nil()) -> Nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add the following weak dependency pairs:
Strict DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))
, selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil()))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest)))
, revapp^#(Nil(), rest) -> c_4()
, select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs))
, select^#(Nil()) -> c_6() }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))
, selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil()))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest)))
, revapp^#(Nil(), rest) -> c_4()
, select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs))
, select^#(Nil()) -> c_6() }
Strict Trs:
{ selects(x', revprefix, Cons(x, xs)) ->
Cons(Cons(x', revapp(revprefix, Cons(x, xs))),
selects(x, Cons(x', revprefix), xs))
, selects(x, revprefix, Nil()) ->
Cons(Cons(x, revapp(revprefix, Nil())), Nil())
, revapp(Cons(x, xs), rest) -> revapp(xs, Cons(x, rest))
, revapp(Nil(), rest) -> rest
, select(Cons(x, xs)) -> selects(x, Nil(), xs)
, select(Nil()) -> Nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
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^2)).
Strict DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))
, selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil()))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest)))
, revapp^#(Nil(), rest) -> c_4()
, select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs))
, select^#(Nil()) -> c_6() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
Uargs(c_5) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[Cons](x1, x2) = [0]
[0]
[Nil] = [0]
[0]
[selects^#](x1, x2, x3) = [0]
[0]
[c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
[revapp^#](x1, x2) = [0]
[0]
[c_2](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_3](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_4] = [0]
[0]
[select^#](x1) = [1]
[0]
[c_5](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_6] = [0]
[0]
The order satisfies the following ordering constraints:
[selects^#(x', revprefix, Cons(x, xs))] = [0]
[0]
>= [0]
[0]
= [c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))]
[selects^#(x, revprefix, Nil())] = [0]
[0]
>= [0]
[0]
= [c_2(revapp^#(revprefix, Nil()))]
[revapp^#(Cons(x, xs), rest)] = [0]
[0]
>= [0]
[0]
= [c_3(revapp^#(xs, Cons(x, rest)))]
[revapp^#(Nil(), rest)] = [0]
[0]
>= [0]
[0]
= [c_4()]
[select^#(Cons(x, xs))] = [1]
[0]
> [0]
[0]
= [c_5(selects^#(x, Nil(), xs))]
[select^#(Nil())] = [1]
[0]
> [0]
[0]
= [c_6()]
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^2)).
Strict DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))
, selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil()))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest)))
, revapp^#(Nil(), rest) -> c_4() }
Weak DPs:
{ select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs))
, select^#(Nil()) -> c_6() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We estimate the number of application of {4} by applications of
Pre({4}) = {1,2,3}. Here rules are labeled as follows:
DPs:
{ 1: selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))
, 2: selects^#(x, revprefix, Nil()) ->
c_2(revapp^#(revprefix, Nil()))
, 3: revapp^#(Cons(x, xs), rest) ->
c_3(revapp^#(xs, Cons(x, rest)))
, 4: revapp^#(Nil(), rest) -> c_4()
, 5: select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs))
, 6: select^#(Nil()) -> c_6() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))
, selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil()))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) }
Weak DPs:
{ revapp^#(Nil(), rest) -> c_4()
, select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs))
, select^#(Nil()) -> c_6() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ revapp^#(Nil(), rest) -> c_4()
, select^#(Nil()) -> c_6() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))
, selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil()))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) }
Weak DPs: { select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
Consider the dependency graph
1: selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))
-->_1 revapp^#(Cons(x, xs), rest) ->
c_3(revapp^#(xs, Cons(x, rest))) :3
-->_2 selects^#(x, revprefix, Nil()) ->
c_2(revapp^#(revprefix, Nil())) :2
-->_2 selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs)) :1
2: selects^#(x, revprefix, Nil()) ->
c_2(revapp^#(revprefix, Nil()))
-->_1 revapp^#(Cons(x, xs), rest) ->
c_3(revapp^#(xs, Cons(x, rest))) :3
3: revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest)))
-->_1 revapp^#(Cons(x, xs), rest) ->
c_3(revapp^#(xs, Cons(x, rest))) :3
4: select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs))
-->_1 selects^#(x, revprefix, Nil()) ->
c_2(revapp^#(revprefix, Nil())) :2
-->_1 selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs)) :1
Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).
{ select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs))
, selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil()))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We decompose the input problem according to the dependency graph
into the upper component
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs)) }
and lower component
{ selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil()))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) }
Further, following extension rules are added to the lower
component.
{ selects^#(x', revprefix, Cons(x, xs)) ->
selects^#(x, Cons(x', revprefix), xs)
, selects^#(x', revprefix, Cons(x, xs)) ->
revapp^#(revprefix, Cons(x, xs)) }
TcT solves the upper component with certificate YES(O(1),O(n^1)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.
DPs:
{ 1: selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs)) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(Cons) = {1, 2}, safe(selects^#) = {1, 2}, safe(c_1) = {},
safe(revapp^#) = {}
and precedence
empty .
Following symbols are considered recursive:
{selects^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(Cons) = [2], pi(selects^#) = [2, 3], pi(c_1) = [1, 2],
pi(revapp^#) = []
Usable defined function symbols are a subset of:
{selects^#, revapp^#}
For your convenience, here are the satisfied ordering constraints:
pi(selects^#(x', revprefix, Cons(x, xs))) = selects^#(Cons(; xs); revprefix)
> c_1(revapp^#(), selects^#(xs; Cons(; revprefix));)
= pi(c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs)))
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:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs)) }
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.
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_1(revapp^#(revprefix, Cons(x, xs)),
selects^#(x, Cons(x', revprefix), xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil()))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) }
Weak DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
selects^#(x, Cons(x', revprefix), xs)
, selects^#(x', revprefix, Cons(x, xs)) ->
revapp^#(revprefix, Cons(x, xs)) }
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: revapp^#(Cons(x, xs), rest) ->
c_3(revapp^#(xs, Cons(x, rest)))
, 4: selects^#(x', revprefix, Cons(x, xs)) ->
revapp^#(revprefix, Cons(x, xs)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_2) = {1}, Uargs(c_3) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[Cons](x1, x2) = [1] x2 + [2]
[Nil] = [0]
[selects^#](x1, x2, x3) = [4] x2 + [4] x3 + [0]
[revapp^#](x1, x2) = [4] x1 + [0]
[c_2](x1) = [1] x1 + [0]
[c_3](x1) = [1] x1 + [7]
The order satisfies the following ordering constraints:
[selects^#(x', revprefix, Cons(x, xs))] = [4] revprefix + [4] xs + [8]
>= [4] revprefix + [4] xs + [8]
= [selects^#(x, Cons(x', revprefix), xs)]
[selects^#(x', revprefix, Cons(x, xs))] = [4] revprefix + [4] xs + [8]
> [4] revprefix + [0]
= [revapp^#(revprefix, Cons(x, xs))]
[selects^#(x, revprefix, Nil())] = [4] revprefix + [0]
>= [4] revprefix + [0]
= [c_2(revapp^#(revprefix, Nil()))]
[revapp^#(Cons(x, xs), rest)] = [4] xs + [8]
> [4] xs + [7]
= [c_3(revapp^#(xs, Cons(x, rest)))]
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)).
Strict DPs:
{ selects^#(x, revprefix, Nil()) ->
c_2(revapp^#(revprefix, Nil())) }
Weak DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
selects^#(x, Cons(x', revprefix), xs)
, selects^#(x', revprefix, Cons(x, xs)) ->
revapp^#(revprefix, Cons(x, xs))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) }
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.
{ selects^#(x', revprefix, Cons(x, xs)) ->
revapp^#(revprefix, Cons(x, xs))
, revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ selects^#(x, revprefix, Nil()) ->
c_2(revapp^#(revprefix, Nil())) }
Weak DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
selects^#(x, Cons(x', revprefix), xs) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ selects^#(x, revprefix, Nil()) ->
c_2(revapp^#(revprefix, Nil())) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { selects^#(x, revprefix, Nil()) -> c_1() }
Weak DPs:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_2(selects^#(x, Cons(x', revprefix), xs)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: selects^#(x, revprefix, Nil()) -> c_1() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_2) = {1}
TcT has computed the following constructor-restricted matrix
interpretation. Note that the diagonal of the component-wise maxima
of interpretation-entries (of constructors) contains no more than 0
non-zero entries.
[Cons](x1, x2) = [0]
[Nil] = [0]
[selects^#](x1, x2, x3) = [1] x2 + [1]
[revapp^#](x1, x2) = [0]
[c_2](x1) = [0]
[c_3](x1) = [0]
[c] = [0]
[c_1] = [0]
[c_2](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[selects^#(x', revprefix, Cons(x, xs))] = [1] revprefix + [1]
>= [1]
= [c_2(selects^#(x, Cons(x', revprefix), xs))]
[selects^#(x, revprefix, Nil())] = [1] revprefix + [1]
> [0]
= [c_1()]
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:
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_2(selects^#(x, Cons(x', revprefix), xs))
, selects^#(x, revprefix, Nil()) -> c_1() }
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.
{ selects^#(x', revprefix, Cons(x, xs)) ->
c_2(selects^#(x, Cons(x', revprefix), xs))
, selects^#(x, revprefix, Nil()) -> c_1() }
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^2))