* Step 1: Sum WORST_CASE(Omega(n^1),O(n^2))
+ Considered Problem:
- Strict TRS:
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()
selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs)))
,selects(x,Cons(x',revprefix),xs))
- Signature:
{revapp/2,select/1,selects/3} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
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()
selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs)))
,selects(x,Cons(x',revprefix),xs))
- Signature:
{revapp/2,select/1,selects/3} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
revapp(y,z){y -> Cons(x,y)} =
revapp(Cons(x,y),z) ->^+ revapp(y,Cons(x,z))
= C[revapp(y,Cons(x,z)) = revapp(y,z){z -> Cons(x,z)}]
** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
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()
selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs)))
,selects(x,Cons(x',revprefix),xs))
- Signature:
{revapp/2,select/1,selects/3} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(Cons) = {1,2}
Following symbols are considered usable:
{revapp,select,selects}
TcT has computed the following interpretation:
p(Cons) = 1 + x1 + x2
p(Nil) = 0
p(revapp) = x1 + x2
p(select) = 3 + 4*x1^2
p(selects) = 7 + 2*x1 + x1*x3 + 3*x1^2 + 2*x2 + x2*x3 + 3*x3 + 3*x3^2
Following rules are strictly oriented:
select(Nil()) = 3
> 0
= Nil()
selects(x,revprefix,Nil()) = 7 + 2*revprefix + 2*x + 3*x^2
> 2 + revprefix + x
= Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) = 13 + 3*revprefix + revprefix*x + revprefix*xs + 9*x + x*x' + 6*x*xs + 3*x^2 + 3*x' + x'*xs + 3*x'^2 + 9*xs + 3*xs^2
> 12 + 3*revprefix + revprefix*xs + 3*x + x*xs + 3*x^2 + 3*x' + x'*xs + 5*xs + 3*xs^2
= Cons(Cons(x',revapp(revprefix,Cons(x,xs))),selects(x,Cons(x',revprefix),xs))
Following rules are (at-least) weakly oriented:
revapp(Cons(x,xs),rest) = 1 + rest + x + xs
>= 1 + rest + x + xs
= revapp(xs,Cons(x,rest))
revapp(Nil(),rest) = rest
>= rest
= rest
select(Cons(x,xs)) = 7 + 8*x + 8*x*xs + 4*x^2 + 8*xs + 4*xs^2
>= 7 + 2*x + x*xs + 3*x^2 + 3*xs + 3*xs^2
= selects(x,Nil(),xs)
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
revapp(Nil(),rest) -> rest
select(Cons(x,xs)) -> selects(x,Nil(),xs)
- Weak TRS:
select(Nil()) -> Nil()
selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs)))
,selects(x,Cons(x',revprefix),xs))
- Signature:
{revapp/2,select/1,selects/3} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(Cons) = {1,2}
Following symbols are considered usable:
{revapp,select,selects}
TcT has computed the following interpretation:
p(Cons) = 1 + x1 + x2
p(Nil) = 0
p(revapp) = x1 + x2
p(select) = 2 + 5*x1 + x1^2
p(selects) = 2 + 3*x1 + x1*x2 + 2*x1*x3 + 3*x2 + x2*x3 + 6*x3 + x3^2
Following rules are strictly oriented:
select(Cons(x,xs)) = 8 + 7*x + 2*x*xs + x^2 + 7*xs + xs^2
> 2 + 3*x + 2*x*xs + 6*xs + xs^2
= selects(x,Nil(),xs)
Following rules are (at-least) weakly oriented:
revapp(Cons(x,xs),rest) = 1 + rest + x + xs
>= 1 + rest + x + xs
= revapp(xs,Cons(x,rest))
revapp(Nil(),rest) = rest
>= rest
= rest
select(Nil()) = 2
>= 0
= Nil()
selects(x,revprefix,Nil()) = 2 + 3*revprefix + revprefix*x + 3*x
>= 2 + revprefix + x
= Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) = 9 + 4*revprefix + revprefix*x + revprefix*x' + revprefix*xs + 8*x + 2*x*x' + 2*x*xs + x^2 + 5*x' + 2*x'*xs + 8*xs + xs^2
>= 8 + 4*revprefix + revprefix*x + revprefix*xs + 5*x + x*x' + 2*x*xs + 4*x' + x'*xs + 8*xs + xs^2
= Cons(Cons(x',revapp(revprefix,Cons(x,xs))),selects(x,Cons(x',revprefix),xs))
** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
revapp(Nil(),rest) -> rest
- Weak TRS:
select(Cons(x,xs)) -> selects(x,Nil(),xs)
select(Nil()) -> Nil()
selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs)))
,selects(x,Cons(x',revprefix),xs))
- Signature:
{revapp/2,select/1,selects/3} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(Cons) = {1,2}
Following symbols are considered usable:
{revapp,select,selects}
TcT has computed the following interpretation:
p(Cons) = 1 + x1 + x2
p(Nil) = 1
p(revapp) = x1 + x2
p(select) = 4*x1 + 5*x1^2
p(selects) = 2 + 7*x1 + 5*x1*x2 + 6*x1*x3 + 5*x1^2 + 5*x2*x3 + 2*x2^2 + 3*x3 + 5*x3^2
Following rules are strictly oriented:
revapp(Nil(),rest) = 1 + rest
> rest
= rest
Following rules are (at-least) weakly oriented:
revapp(Cons(x,xs),rest) = 1 + rest + x + xs
>= 1 + rest + x + xs
= revapp(xs,Cons(x,rest))
select(Cons(x,xs)) = 9 + 14*x + 10*x*xs + 5*x^2 + 14*xs + 5*xs^2
>= 4 + 12*x + 6*x*xs + 5*x^2 + 8*xs + 5*xs^2
= selects(x,Nil(),xs)
select(Nil()) = 9
>= 1
= Nil()
selects(x,revprefix,Nil()) = 10 + 5*revprefix + 5*revprefix*x + 2*revprefix^2 + 13*x + 5*x^2
>= 4 + revprefix + x
= Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) = 10 + 5*revprefix + 5*revprefix*x + 5*revprefix*x' + 5*revprefix*xs + 2*revprefix^2 + 13*x + 6*x*x' + 10*x*xs + 5*x^2 + 13*x' + 6*x'*xs + 5*x'^2 + 13*xs + 5*xs^2
>= 7 + 5*revprefix + 5*revprefix*x + 4*revprefix*x' + 5*revprefix*xs + 2*revprefix^2 + 13*x + 5*x*x' + 6*x*xs + 5*x^2 + 5*x' + 5*x'*xs + 2*x'^2 + 9*xs + 5*xs^2
= Cons(Cons(x',revapp(revprefix,Cons(x,xs))),selects(x,Cons(x',revprefix),xs))
** Step 1.b:4: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
- Weak TRS:
revapp(Nil(),rest) -> rest
select(Cons(x,xs)) -> selects(x,Nil(),xs)
select(Nil()) -> Nil()
selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs)))
,selects(x,Cons(x',revprefix),xs))
- Signature:
{revapp/2,select/1,selects/3} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(Cons) = {1,2}
Following symbols are considered usable:
{revapp,select,selects}
TcT has computed the following interpretation:
p(Cons) = 1 + x1 + x2
p(Nil) = 1
p(revapp) = 3*x1 + 2*x2
p(select) = 7*x1 + 4*x1^2
p(selects) = 7 + 7*x1*x3 + x1^2 + 4*x2*x3 + x3 + 4*x3^2
Following rules are strictly oriented:
revapp(Cons(x,xs),rest) = 3 + 2*rest + 3*x + 3*xs
> 2 + 2*rest + 2*x + 3*xs
= revapp(xs,Cons(x,rest))
Following rules are (at-least) weakly oriented:
revapp(Nil(),rest) = 3 + 2*rest
>= rest
= rest
select(Cons(x,xs)) = 11 + 15*x + 8*x*xs + 4*x^2 + 15*xs + 4*xs^2
>= 7 + 7*x*xs + x^2 + 5*xs + 4*xs^2
= selects(x,Nil(),xs)
select(Nil()) = 11
>= 1
= Nil()
selects(x,revprefix,Nil()) = 12 + 4*revprefix + 7*x + x^2
>= 5 + 3*revprefix + x
= Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) = 12 + 4*revprefix + 4*revprefix*x + 4*revprefix*xs + 9*x + 7*x*x' + 8*x*xs + 4*x^2 + 7*x' + 7*x'*xs + x'^2 + 9*xs + 4*xs^2
>= 11 + 3*revprefix + 4*revprefix*xs + 2*x + 7*x*xs + x^2 + x' + 4*x'*xs + 7*xs + 4*xs^2
= Cons(Cons(x',revapp(revprefix,Cons(x,xs))),selects(x,Cons(x',revprefix),xs))
** Step 1.b:5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
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()
selects(x,revprefix,Nil()) -> Cons(Cons(x,revapp(revprefix,Nil())),Nil())
selects(x',revprefix,Cons(x,xs)) -> Cons(Cons(x',revapp(revprefix,Cons(x,xs)))
,selects(x,Cons(x',revprefix),xs))
- Signature:
{revapp/2,select/1,selects/3} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {revapp,select,selects} and constructors {Cons,Nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^2))