WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(cons(z0,z1),z2) -> c4(APP(z1,z2)) APP(nil(),z0) -> c3() HIGH(z0,cons(z1,z2)) -> c10(IFHIGH(le(z1,z0),z0,cons(z1,z2)),LE(z1,z0)) HIGH(z0,nil()) -> c9() IFHIGH(false(),z0,cons(z1,z2)) -> c12(HIGH(z0,z2)) IFHIGH(true(),z0,cons(z1,z2)) -> c11(HIGH(z0,z2)) IFLOW(false(),z0,cons(z1,z2)) -> c8(LOW(z0,z2)) IFLOW(true(),z0,cons(z1,z2)) -> c7(LOW(z0,z2)) LE(0(),z0) -> c() LE(s(z0),0()) -> c1() LE(s(z0),s(z1)) -> c2(LE(z0,z1)) LOW(z0,cons(z1,z2)) -> c6(IFLOW(le(z1,z0),z0,cons(z1,z2)),LE(z1,z0)) LOW(z0,nil()) -> c5() QUICKSORT(cons(z0,z1)) -> c14(APP(quicksort(low(z0,z1)),cons(z0,quicksort(high(z0,z1)))) ,QUICKSORT(low(z0,z1)) ,LOW(z0,z1)) QUICKSORT(cons(z0,z1)) -> c15(APP(quicksort(low(z0,z1)),cons(z0,quicksort(high(z0,z1)))) ,QUICKSORT(high(z0,z1)) ,HIGH(z0,z1)) QUICKSORT(nil()) -> c13() - Weak TRS: app(cons(z0,z1),z2) -> cons(z0,app(z1,z2)) app(nil(),z0) -> z0 high(z0,cons(z1,z2)) -> ifhigh(le(z1,z0),z0,cons(z1,z2)) high(z0,nil()) -> nil() ifhigh(false(),z0,cons(z1,z2)) -> cons(z1,high(z0,z2)) ifhigh(true(),z0,cons(z1,z2)) -> high(z0,z2) iflow(false(),z0,cons(z1,z2)) -> low(z0,z2) iflow(true(),z0,cons(z1,z2)) -> cons(z1,low(z0,z2)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) low(z0,cons(z1,z2)) -> iflow(le(z1,z0),z0,cons(z1,z2)) low(z0,nil()) -> nil() quicksort(cons(z0,z1)) -> app(quicksort(low(z0,z1)),cons(z0,quicksort(high(z0,z1)))) quicksort(nil()) -> nil() - Signature: {APP/2,HIGH/2,IFHIGH/3,IFLOW/3,LE/2,LOW/2,QUICKSORT/1,app/2,high/2,ifhigh/3,iflow/3,le/2,low/2 ,quicksort/1} / {0/0,c/0,c1/0,c10/2,c11/1,c12/1,c13/0,c14/3,c15/3,c2/1,c3/0,c4/1,c5/0,c6/2,c7/1,c8/1,c9/0 ,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,HIGH,IFHIGH,IFLOW,LE,LOW,QUICKSORT,app,high,ifhigh ,iflow,le,low,quicksort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false ,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(cons(z0,z1),z2) -> c4(APP(z1,z2)) APP(nil(),z0) -> c3() HIGH(z0,cons(z1,z2)) -> c10(IFHIGH(le(z1,z0),z0,cons(z1,z2)),LE(z1,z0)) HIGH(z0,nil()) -> c9() IFHIGH(false(),z0,cons(z1,z2)) -> c12(HIGH(z0,z2)) IFHIGH(true(),z0,cons(z1,z2)) -> c11(HIGH(z0,z2)) IFLOW(false(),z0,cons(z1,z2)) -> c8(LOW(z0,z2)) IFLOW(true(),z0,cons(z1,z2)) -> c7(LOW(z0,z2)) LE(0(),z0) -> c() LE(s(z0),0()) -> c1() LE(s(z0),s(z1)) -> c2(LE(z0,z1)) LOW(z0,cons(z1,z2)) -> c6(IFLOW(le(z1,z0),z0,cons(z1,z2)),LE(z1,z0)) LOW(z0,nil()) -> c5() QUICKSORT(cons(z0,z1)) -> c14(APP(quicksort(low(z0,z1)),cons(z0,quicksort(high(z0,z1)))) ,QUICKSORT(low(z0,z1)) ,LOW(z0,z1)) QUICKSORT(cons(z0,z1)) -> c15(APP(quicksort(low(z0,z1)),cons(z0,quicksort(high(z0,z1)))) ,QUICKSORT(high(z0,z1)) ,HIGH(z0,z1)) QUICKSORT(nil()) -> c13() - Weak TRS: app(cons(z0,z1),z2) -> cons(z0,app(z1,z2)) app(nil(),z0) -> z0 high(z0,cons(z1,z2)) -> ifhigh(le(z1,z0),z0,cons(z1,z2)) high(z0,nil()) -> nil() ifhigh(false(),z0,cons(z1,z2)) -> cons(z1,high(z0,z2)) ifhigh(true(),z0,cons(z1,z2)) -> high(z0,z2) iflow(false(),z0,cons(z1,z2)) -> low(z0,z2) iflow(true(),z0,cons(z1,z2)) -> cons(z1,low(z0,z2)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) low(z0,cons(z1,z2)) -> iflow(le(z1,z0),z0,cons(z1,z2)) low(z0,nil()) -> nil() quicksort(cons(z0,z1)) -> app(quicksort(low(z0,z1)),cons(z0,quicksort(high(z0,z1)))) quicksort(nil()) -> nil() - Signature: {APP/2,HIGH/2,IFHIGH/3,IFLOW/3,LE/2,LOW/2,QUICKSORT/1,app/2,high/2,ifhigh/3,iflow/3,le/2,low/2 ,quicksort/1} / {0/0,c/0,c1/0,c10/2,c11/1,c12/1,c13/0,c14/3,c15/3,c2/1,c3/0,c4/1,c5/0,c6/2,c7/1,c8/1,c9/0 ,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,HIGH,IFHIGH,IFLOW,LE,LOW,QUICKSORT,app,high,ifhigh ,iflow,le,low,quicksort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false ,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(cons(z0,z1),z2) -> c4(APP(z1,z2)) APP(nil(),z0) -> c3() HIGH(z0,cons(z1,z2)) -> c10(IFHIGH(le(z1,z0),z0,cons(z1,z2)),LE(z1,z0)) HIGH(z0,nil()) -> c9() IFHIGH(false(),z0,cons(z1,z2)) -> c12(HIGH(z0,z2)) IFHIGH(true(),z0,cons(z1,z2)) -> c11(HIGH(z0,z2)) IFLOW(false(),z0,cons(z1,z2)) -> c8(LOW(z0,z2)) IFLOW(true(),z0,cons(z1,z2)) -> c7(LOW(z0,z2)) LE(0(),z0) -> c() LE(s(z0),0()) -> c1() LE(s(z0),s(z1)) -> c2(LE(z0,z1)) LOW(z0,cons(z1,z2)) -> c6(IFLOW(le(z1,z0),z0,cons(z1,z2)),LE(z1,z0)) LOW(z0,nil()) -> c5() QUICKSORT(cons(z0,z1)) -> c14(APP(quicksort(low(z0,z1)),cons(z0,quicksort(high(z0,z1)))) ,QUICKSORT(low(z0,z1)) ,LOW(z0,z1)) QUICKSORT(cons(z0,z1)) -> c15(APP(quicksort(low(z0,z1)),cons(z0,quicksort(high(z0,z1)))) ,QUICKSORT(high(z0,z1)) ,HIGH(z0,z1)) QUICKSORT(nil()) -> c13() - Weak TRS: app(cons(z0,z1),z2) -> cons(z0,app(z1,z2)) app(nil(),z0) -> z0 high(z0,cons(z1,z2)) -> ifhigh(le(z1,z0),z0,cons(z1,z2)) high(z0,nil()) -> nil() ifhigh(false(),z0,cons(z1,z2)) -> cons(z1,high(z0,z2)) ifhigh(true(),z0,cons(z1,z2)) -> high(z0,z2) iflow(false(),z0,cons(z1,z2)) -> low(z0,z2) iflow(true(),z0,cons(z1,z2)) -> cons(z1,low(z0,z2)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) low(z0,cons(z1,z2)) -> iflow(le(z1,z0),z0,cons(z1,z2)) low(z0,nil()) -> nil() quicksort(cons(z0,z1)) -> app(quicksort(low(z0,z1)),cons(z0,quicksort(high(z0,z1)))) quicksort(nil()) -> nil() - Signature: {APP/2,HIGH/2,IFHIGH/3,IFLOW/3,LE/2,LOW/2,QUICKSORT/1,app/2,high/2,ifhigh/3,iflow/3,le/2,low/2 ,quicksort/1} / {0/0,c/0,c1/0,c10/2,c11/1,c12/1,c13/0,c14/3,c15/3,c2/1,c3/0,c4/1,c5/0,c6/2,c7/1,c8/1,c9/0 ,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,HIGH,IFHIGH,IFLOW,LE,LOW,QUICKSORT,app,high,ifhigh ,iflow,le,low,quicksort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false ,nil,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: APP(y,z){y -> cons(x,y)} = APP(cons(x,y),z) ->^+ c4(APP(y,z)) = C[APP(y,z) = APP(y,z){}] WORST_CASE(Omega(n^1),?)