WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(add(z0,z1),z2) -> c8(APP(z1,z2)) APP(nil(),z0) -> c7() HIGH(z0,add(z1,z2)) -> c14(IF_HIGH(le(z1,z0),z0,add(z1,z2)),LE(z1,z0)) HIGH(z0,nil()) -> c13() IF_HIGH(false(),z0,add(z1,z2)) -> c16(HIGH(z0,z2)) IF_HIGH(true(),z0,add(z1,z2)) -> c15(HIGH(z0,z2)) IF_LOW(false(),z0,add(z1,z2)) -> c12(LOW(z0,z2)) IF_LOW(true(),z0,add(z1,z2)) -> c11(LOW(z0,z2)) LE(0(),z0) -> c4() LE(s(z0),0()) -> c5() LE(s(z0),s(z1)) -> c6(LE(z0,z1)) LOW(z0,add(z1,z2)) -> c10(IF_LOW(le(z1,z0),z0,add(z1,z2)),LE(z1,z0)) LOW(z0,nil()) -> c9() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUICKSORT(add(z0,z1)) -> c18(APP(quicksort(low(z0,z1)),add(z0,quicksort(high(z0,z1)))) ,QUICKSORT(low(z0,z1)) ,LOW(z0,z1)) QUICKSORT(add(z0,z1)) -> c19(APP(quicksort(low(z0,z1)),add(z0,quicksort(high(z0,z1)))) ,QUICKSORT(high(z0,z1)) ,HIGH(z0,z1)) QUICKSORT(nil()) -> c17() QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 high(z0,add(z1,z2)) -> if_high(le(z1,z0),z0,add(z1,z2)) high(z0,nil()) -> nil() if_high(false(),z0,add(z1,z2)) -> add(z1,high(z0,z2)) if_high(true(),z0,add(z1,z2)) -> high(z0,z2) if_low(false(),z0,add(z1,z2)) -> low(z0,z2) if_low(true(),z0,add(z1,z2)) -> add(z1,low(z0,z2)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) low(z0,add(z1,z2)) -> if_low(le(z1,z0),z0,add(z1,z2)) low(z0,nil()) -> nil() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quicksort(add(z0,z1)) -> app(quicksort(low(z0,z1)),add(z0,quicksort(high(z0,z1)))) quicksort(nil()) -> nil() quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) - Signature: {APP/2,HIGH/2,IF_HIGH/3,IF_LOW/3,LE/2,LOW/2,MINUS/2,QUICKSORT/1,QUOT/2,app/2,high/2,if_high/3,if_low/3,le/2 ,low/2,minus/2,quicksort/1,quot/2} / {0/0,add/2,c/0,c1/1,c10/2,c11/1,c12/1,c13/0,c14/2,c15/1,c16/1,c17/0 ,c18/3,c19/3,c2/0,c3/2,c4/0,c5/0,c6/1,c7/0,c8/1,c9/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,HIGH,IF_HIGH,IF_LOW,LE,LOW,MINUS,QUICKSORT,QUOT,app ,high,if_high,if_low,le,low,minus,quicksort,quot} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c16 ,c17,c18,c19,c2,c3,c4,c5,c6,c7,c8,c9,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(add(z0,z1),z2) -> c8(APP(z1,z2)) APP(nil(),z0) -> c7() HIGH(z0,add(z1,z2)) -> c14(IF_HIGH(le(z1,z0),z0,add(z1,z2)),LE(z1,z0)) HIGH(z0,nil()) -> c13() IF_HIGH(false(),z0,add(z1,z2)) -> c16(HIGH(z0,z2)) IF_HIGH(true(),z0,add(z1,z2)) -> c15(HIGH(z0,z2)) IF_LOW(false(),z0,add(z1,z2)) -> c12(LOW(z0,z2)) IF_LOW(true(),z0,add(z1,z2)) -> c11(LOW(z0,z2)) LE(0(),z0) -> c4() LE(s(z0),0()) -> c5() LE(s(z0),s(z1)) -> c6(LE(z0,z1)) LOW(z0,add(z1,z2)) -> c10(IF_LOW(le(z1,z0),z0,add(z1,z2)),LE(z1,z0)) LOW(z0,nil()) -> c9() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUICKSORT(add(z0,z1)) -> c18(APP(quicksort(low(z0,z1)),add(z0,quicksort(high(z0,z1)))) ,QUICKSORT(low(z0,z1)) ,LOW(z0,z1)) QUICKSORT(add(z0,z1)) -> c19(APP(quicksort(low(z0,z1)),add(z0,quicksort(high(z0,z1)))) ,QUICKSORT(high(z0,z1)) ,HIGH(z0,z1)) QUICKSORT(nil()) -> c17() QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 high(z0,add(z1,z2)) -> if_high(le(z1,z0),z0,add(z1,z2)) high(z0,nil()) -> nil() if_high(false(),z0,add(z1,z2)) -> add(z1,high(z0,z2)) if_high(true(),z0,add(z1,z2)) -> high(z0,z2) if_low(false(),z0,add(z1,z2)) -> low(z0,z2) if_low(true(),z0,add(z1,z2)) -> add(z1,low(z0,z2)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) low(z0,add(z1,z2)) -> if_low(le(z1,z0),z0,add(z1,z2)) low(z0,nil()) -> nil() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quicksort(add(z0,z1)) -> app(quicksort(low(z0,z1)),add(z0,quicksort(high(z0,z1)))) quicksort(nil()) -> nil() quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) - Signature: {APP/2,HIGH/2,IF_HIGH/3,IF_LOW/3,LE/2,LOW/2,MINUS/2,QUICKSORT/1,QUOT/2,app/2,high/2,if_high/3,if_low/3,le/2 ,low/2,minus/2,quicksort/1,quot/2} / {0/0,add/2,c/0,c1/1,c10/2,c11/1,c12/1,c13/0,c14/2,c15/1,c16/1,c17/0 ,c18/3,c19/3,c2/0,c3/2,c4/0,c5/0,c6/1,c7/0,c8/1,c9/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,HIGH,IF_HIGH,IF_LOW,LE,LOW,MINUS,QUICKSORT,QUOT,app ,high,if_high,if_low,le,low,minus,quicksort,quot} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c16 ,c17,c18,c19,c2,c3,c4,c5,c6,c7,c8,c9,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(add(z0,z1),z2) -> c8(APP(z1,z2)) APP(nil(),z0) -> c7() HIGH(z0,add(z1,z2)) -> c14(IF_HIGH(le(z1,z0),z0,add(z1,z2)),LE(z1,z0)) HIGH(z0,nil()) -> c13() IF_HIGH(false(),z0,add(z1,z2)) -> c16(HIGH(z0,z2)) IF_HIGH(true(),z0,add(z1,z2)) -> c15(HIGH(z0,z2)) IF_LOW(false(),z0,add(z1,z2)) -> c12(LOW(z0,z2)) IF_LOW(true(),z0,add(z1,z2)) -> c11(LOW(z0,z2)) LE(0(),z0) -> c4() LE(s(z0),0()) -> c5() LE(s(z0),s(z1)) -> c6(LE(z0,z1)) LOW(z0,add(z1,z2)) -> c10(IF_LOW(le(z1,z0),z0,add(z1,z2)),LE(z1,z0)) LOW(z0,nil()) -> c9() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUICKSORT(add(z0,z1)) -> c18(APP(quicksort(low(z0,z1)),add(z0,quicksort(high(z0,z1)))) ,QUICKSORT(low(z0,z1)) ,LOW(z0,z1)) QUICKSORT(add(z0,z1)) -> c19(APP(quicksort(low(z0,z1)),add(z0,quicksort(high(z0,z1)))) ,QUICKSORT(high(z0,z1)) ,HIGH(z0,z1)) QUICKSORT(nil()) -> c17() QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 high(z0,add(z1,z2)) -> if_high(le(z1,z0),z0,add(z1,z2)) high(z0,nil()) -> nil() if_high(false(),z0,add(z1,z2)) -> add(z1,high(z0,z2)) if_high(true(),z0,add(z1,z2)) -> high(z0,z2) if_low(false(),z0,add(z1,z2)) -> low(z0,z2) if_low(true(),z0,add(z1,z2)) -> add(z1,low(z0,z2)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) low(z0,add(z1,z2)) -> if_low(le(z1,z0),z0,add(z1,z2)) low(z0,nil()) -> nil() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quicksort(add(z0,z1)) -> app(quicksort(low(z0,z1)),add(z0,quicksort(high(z0,z1)))) quicksort(nil()) -> nil() quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) - Signature: {APP/2,HIGH/2,IF_HIGH/3,IF_LOW/3,LE/2,LOW/2,MINUS/2,QUICKSORT/1,QUOT/2,app/2,high/2,if_high/3,if_low/3,le/2 ,low/2,minus/2,quicksort/1,quot/2} / {0/0,add/2,c/0,c1/1,c10/2,c11/1,c12/1,c13/0,c14/2,c15/1,c16/1,c17/0 ,c18/3,c19/3,c2/0,c3/2,c4/0,c5/0,c6/1,c7/0,c8/1,c9/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,HIGH,IF_HIGH,IF_LOW,LE,LOW,MINUS,QUICKSORT,QUOT,app ,high,if_high,if_low,le,low,minus,quicksort,quot} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c16 ,c17,c18,c19,c2,c3,c4,c5,c6,c7,c8,c9,false,nil,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: APP(y,z){y -> add(x,y)} = APP(add(x,y),z) ->^+ c8(APP(y,z)) = C[APP(y,z) = APP(y,z){}] WORST_CASE(Omega(n^1),?)