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