* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
main(0()) -> 0()
main(S(x1)) -> sum#1(map#2(Cons(S(x1),unfoldr#2(S(x1)))))
map#2(Cons(x2,x5)) -> Cons(mult#2(x2,x2),map#2(x5))
map#2(Nil()) -> Nil()
mult#2(0(),x2) -> 0()
mult#2(S(x4),x2) -> plus#2(x2,mult#2(x4,x2))
plus#2(0(),x8) -> x8
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
sum#1(Cons(x2,x1)) -> plus#2(x2,sum#1(x1))
sum#1(Nil()) -> 0()
unfoldr#2(0()) -> Nil()
unfoldr#2(S(x2)) -> Cons(x2,unfoldr#2(x2))
- Signature:
{main/1,map#2/1,mult#2/2,plus#2/2,sum#1/1,unfoldr#2/1} / {0/0,Cons/2,Nil/0,S/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {main,map#2,mult#2,plus#2,sum#1
,unfoldr#2} and constructors {0,Cons,Nil,S}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
main(0()) -> 0()
main(S(x1)) -> sum#1(map#2(Cons(S(x1),unfoldr#2(S(x1)))))
map#2(Cons(x2,x5)) -> Cons(mult#2(x2,x2),map#2(x5))
map#2(Nil()) -> Nil()
mult#2(0(),x2) -> 0()
mult#2(S(x4),x2) -> plus#2(x2,mult#2(x4,x2))
plus#2(0(),x8) -> x8
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
sum#1(Cons(x2,x1)) -> plus#2(x2,sum#1(x1))
sum#1(Nil()) -> 0()
unfoldr#2(0()) -> Nil()
unfoldr#2(S(x2)) -> Cons(x2,unfoldr#2(x2))
- Signature:
{main/1,map#2/1,mult#2/2,plus#2/2,sum#1/1,unfoldr#2/1} / {0/0,Cons/2,Nil/0,S/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {main,map#2,mult#2,plus#2,sum#1
,unfoldr#2} and constructors {0,Cons,Nil,S}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
map#2(y){y -> Cons(x,y)} =
map#2(Cons(x,y)) ->^+ Cons(mult#2(x,x),map#2(y))
= C[map#2(y) = map#2(y){}]
WORST_CASE(Omega(n^1),?)