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