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