*** 1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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))
Weak DP Rules:
Weak TRS Rules:
Signature:
{revapp/2,select/1,selects/3} / {Cons/2,Nil/0}
Obligation:
Innermost
basic terms: {revapp,select,selects}/{Cons,Nil}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
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) = 1 + 6*x1 + 3*x1^2
p(selects) = 2*x1 + 2*x1*x3 + x1^2 + x2*x3 + 4*x3 + x3^2
Following rules are strictly oriented:
revapp(Nil(),rest) = 1 + rest
> rest
= rest
select(Cons(x,xs)) = 10 + 12*x + 6*x*xs + 3*x^2 + 12*xs + 3*xs^2
> 2*x + 2*x*xs + x^2 + 5*xs + xs^2
= selects(x,Nil(),xs)
select(Nil()) = 10
> 1
= Nil()
selects(x,revprefix,Nil()) = 5 + revprefix + 4*x + x^2
> 4 + revprefix + x
= Cons(Cons(x
,revapp(revprefix,Nil()))
,Nil())
selects(x',revprefix,Cons(x,xs)) = 5 + revprefix + revprefix*x + revprefix*xs + 6*x + 2*x*x' + 2*x*xs + x^2 + 4*x' + 2*x'*xs + x'^2 + 6*xs + xs^2
> 3 + revprefix + revprefix*xs + 3*x + 2*x*xs + x^2 + x' + x'*xs + 6*xs + 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))
*** 1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
Weak DP Rules:
Weak TRS Rules:
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
basic terms: {revapp,select,selects}/{Cons,Nil}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
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) = 4 + 2*x1 + x2
p(select) = 3*x1 + 6*x1^2
p(selects) = 3 + 7*x1 + x1*x2 + 6*x1*x3 + 2*x2*x3 + 2*x3 + 5*x3^2
Following rules are strictly oriented:
revapp(Cons(x,xs),rest) = 6 + rest + 2*x + 2*xs
> 5 + rest + x + 2*xs
= revapp(xs,Cons(x,rest))
Following rules are (at-least) weakly oriented:
revapp(Nil(),rest) = 6 + rest
>= rest
= rest
select(Cons(x,xs)) = 9 + 15*x + 12*x*xs + 6*x^2 + 15*xs + 6*xs^2
>= 3 + 8*x + 6*x*xs + 4*xs + 5*xs^2
= selects(x,Nil(),xs)
select(Nil()) = 9
>= 1
= Nil()
selects(x,revprefix,Nil()) = 10 + 2*revprefix + revprefix*x + 13*x
>= 8 + 2*revprefix + x
= Cons(Cons(x
,revapp(revprefix,Nil()))
,Nil())
selects(x',revprefix,Cons(x,xs)) = 10 + 2*revprefix + 2*revprefix*x + revprefix*x' + 2*revprefix*xs + 12*x + 6*x*x' + 10*x*xs + 5*x^2 + 13*x' + 6*x'*xs + 12*xs + 5*xs^2
>= 10 + 2*revprefix + revprefix*x + 2*revprefix*xs + 9*x + x*x' + 6*x*xs + x' + 2*x'*xs + 5*xs + 5*xs^2
= Cons(Cons(x'
,revapp(revprefix,Cons(x,xs)))
,selects(x
,Cons(x',revprefix)
,xs))
*** 1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
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
basic terms: {revapp,select,selects}/{Cons,Nil}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).