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