* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
goal(xs) -> permute(xs)
mapconsapp(x,Nil(),rest) -> rest
mapconsapp(x',Cons(x,xs),rest) -> Cons(Cons(x',x),mapconsapp(x',xs,rest))
permute(Cons(x,xs)) -> select(x,Nil(),xs)
permute(Nil()) -> Cons(Nil(),Nil())
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
revapp(Nil(),rest) -> rest
select(x,revprefix,Nil()) -> mapconsapp(x,permute(revapp(revprefix,Nil())),Nil())
select(x',revprefix,Cons(x,xs)) -> mapconsapp(x'
,permute(revapp(revprefix,Cons(x,xs)))
,select(x,Cons(x',revprefix),xs))
- Signature:
{goal/1,mapconsapp/3,permute/1,revapp/2,select/3} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {goal,mapconsapp,permute,revapp
,select} and constructors {Cons,Nil}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
goal(xs) -> permute(xs)
mapconsapp(x,Nil(),rest) -> rest
mapconsapp(x',Cons(x,xs),rest) -> Cons(Cons(x',x),mapconsapp(x',xs,rest))
permute(Cons(x,xs)) -> select(x,Nil(),xs)
permute(Nil()) -> Cons(Nil(),Nil())
revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
revapp(Nil(),rest) -> rest
select(x,revprefix,Nil()) -> mapconsapp(x,permute(revapp(revprefix,Nil())),Nil())
select(x',revprefix,Cons(x,xs)) -> mapconsapp(x'
,permute(revapp(revprefix,Cons(x,xs)))
,select(x,Cons(x',revprefix),xs))
- Signature:
{goal/1,mapconsapp/3,permute/1,revapp/2,select/3} / {Cons/2,Nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {goal,mapconsapp,permute,revapp
,select} and constructors {Cons,Nil}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
mapconsapp(x,z,u){z -> Cons(y,z)} =
mapconsapp(x,Cons(y,z),u) ->^+ Cons(Cons(x,y),mapconsapp(x,z,u))
= C[mapconsapp(x,z,u) = mapconsapp(x,z,u){}]
WORST_CASE(Omega(n^1),?)