WORST_CASE(Omega(n^1),?) * Step 1: Sum WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ack(0(),x) -> s(x) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) d(x) -> if(le(x,nr()),x) if(false(),x) -> nil() if(true(),x) -> cons(x,d(s(x))) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) nr() -> ack(s(s(s(s(s(s(0())))))),0()) numbers() -> d(0()) - Signature: {ack/2,d/1,if/2,le/2,nr/0,numbers/0} / {0/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ack,d,if,le,nr,numbers} and constructors {0,cons,false ,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ack(0(),x) -> s(x) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) d(x) -> if(le(x,nr()),x) if(false(),x) -> nil() if(true(),x) -> cons(x,d(s(x))) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) nr() -> ack(s(s(s(s(s(s(0())))))),0()) numbers() -> d(0()) - Signature: {ack/2,d/1,if/2,le/2,nr/0,numbers/0} / {0/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ack,d,if,le,nr,numbers} and constructors {0,cons,false ,nil,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: ack(s(x),y){y -> s(y)} = ack(s(x),s(y)) ->^+ ack(x,ack(s(x),y)) = C[ack(s(x),y) = ack(s(x),y){}] WORST_CASE(Omega(n^1),?)