* 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),?)