WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPEND(cons(z0,z1),ys()) -> c15(APPEND(z1,ys())) APPEND(nil(),ys()) -> c14() FILTERHIGH(z0,cons(z1,z2)) -> c8(IF2(ge(z1,z0),z0,z1,z2),GE(z1,z0)) FILTERHIGH(z0,nil()) -> c7() FILTERLOW(z0,cons(z1,z2)) -> c4(IF1(ge(z0,z1),z0,z1,z2),GE(z0,z1)) FILTERLOW(z0,nil()) -> c3() GE(z0,0()) -> c11() GE(0(),s(z0)) -> c12() GE(s(z0),s(z1)) -> c13(GE(z0,z1)) IF1(false(),z0,z1,z2) -> c6(FILTERLOW(z0,z2)) IF1(true(),z0,z1,z2) -> c5(FILTERLOW(z0,z2)) IF2(false(),z0,z1,z2) -> c10(FILTERHIGH(z0,z2)) IF2(true(),z0,z1,z2) -> c9(FILTERHIGH(z0,z2)) QSORT(cons(z0,z1)) -> c1(APPEND(qsort(filterlow(z0,cons(z0,z1))),cons(z0,qsort(filterhigh(z0,cons(z0,z1))))) ,QSORT(filterlow(z0,cons(z0,z1))) ,FILTERLOW(z0,cons(z0,z1))) QSORT(cons(z0,z1)) -> c2(APPEND(qsort(filterlow(z0,cons(z0,z1))),cons(z0,qsort(filterhigh(z0,cons(z0,z1))))) ,QSORT(filterhigh(z0,cons(z0,z1))) ,FILTERHIGH(z0,cons(z0,z1))) QSORT(nil()) -> c() - Weak TRS: append(cons(z0,z1),ys()) -> cons(z0,append(z1,ys())) append(nil(),ys()) -> ys() filterhigh(z0,cons(z1,z2)) -> if2(ge(z1,z0),z0,z1,z2) filterhigh(z0,nil()) -> nil() filterlow(z0,cons(z1,z2)) -> if1(ge(z0,z1),z0,z1,z2) filterlow(z0,nil()) -> nil() ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) if1(false(),z0,z1,z2) -> cons(z1,filterlow(z0,z2)) if1(true(),z0,z1,z2) -> filterlow(z0,z2) if2(false(),z0,z1,z2) -> cons(z1,filterhigh(z0,z2)) if2(true(),z0,z1,z2) -> filterhigh(z0,z2) qsort(cons(z0,z1)) -> append(qsort(filterlow(z0,cons(z0,z1))),cons(z0,qsort(filterhigh(z0,cons(z0,z1))))) qsort(nil()) -> nil() - Signature: {APPEND/2,FILTERHIGH/2,FILTERLOW/2,GE/2,IF1/4,IF2/4,QSORT/1,append/2,filterhigh/2,filterlow/2,ge/2,if1/4 ,if2/4,qsort/1} / {0/0,c/0,c1/3,c10/1,c11/0,c12/0,c13/1,c14/0,c15/1,c2/3,c3/0,c4/2,c5/1,c6/1,c7/0,c8/2,c9/1 ,cons/2,false/0,nil/0,s/1,true/0,ys/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND,FILTERHIGH,FILTERLOW,GE,IF1,IF2,QSORT,append ,filterhigh,filterlow,ge,if1,if2,qsort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c2,c3,c4,c5,c6,c7 ,c8,c9,cons,false,nil,s,true,ys} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPEND(cons(z0,z1),ys()) -> c15(APPEND(z1,ys())) APPEND(nil(),ys()) -> c14() FILTERHIGH(z0,cons(z1,z2)) -> c8(IF2(ge(z1,z0),z0,z1,z2),GE(z1,z0)) FILTERHIGH(z0,nil()) -> c7() FILTERLOW(z0,cons(z1,z2)) -> c4(IF1(ge(z0,z1),z0,z1,z2),GE(z0,z1)) FILTERLOW(z0,nil()) -> c3() GE(z0,0()) -> c11() GE(0(),s(z0)) -> c12() GE(s(z0),s(z1)) -> c13(GE(z0,z1)) IF1(false(),z0,z1,z2) -> c6(FILTERLOW(z0,z2)) IF1(true(),z0,z1,z2) -> c5(FILTERLOW(z0,z2)) IF2(false(),z0,z1,z2) -> c10(FILTERHIGH(z0,z2)) IF2(true(),z0,z1,z2) -> c9(FILTERHIGH(z0,z2)) QSORT(cons(z0,z1)) -> c1(APPEND(qsort(filterlow(z0,cons(z0,z1))),cons(z0,qsort(filterhigh(z0,cons(z0,z1))))) ,QSORT(filterlow(z0,cons(z0,z1))) ,FILTERLOW(z0,cons(z0,z1))) QSORT(cons(z0,z1)) -> c2(APPEND(qsort(filterlow(z0,cons(z0,z1))),cons(z0,qsort(filterhigh(z0,cons(z0,z1))))) ,QSORT(filterhigh(z0,cons(z0,z1))) ,FILTERHIGH(z0,cons(z0,z1))) QSORT(nil()) -> c() - Weak TRS: append(cons(z0,z1),ys()) -> cons(z0,append(z1,ys())) append(nil(),ys()) -> ys() filterhigh(z0,cons(z1,z2)) -> if2(ge(z1,z0),z0,z1,z2) filterhigh(z0,nil()) -> nil() filterlow(z0,cons(z1,z2)) -> if1(ge(z0,z1),z0,z1,z2) filterlow(z0,nil()) -> nil() ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) if1(false(),z0,z1,z2) -> cons(z1,filterlow(z0,z2)) if1(true(),z0,z1,z2) -> filterlow(z0,z2) if2(false(),z0,z1,z2) -> cons(z1,filterhigh(z0,z2)) if2(true(),z0,z1,z2) -> filterhigh(z0,z2) qsort(cons(z0,z1)) -> append(qsort(filterlow(z0,cons(z0,z1))),cons(z0,qsort(filterhigh(z0,cons(z0,z1))))) qsort(nil()) -> nil() - Signature: {APPEND/2,FILTERHIGH/2,FILTERLOW/2,GE/2,IF1/4,IF2/4,QSORT/1,append/2,filterhigh/2,filterlow/2,ge/2,if1/4 ,if2/4,qsort/1} / {0/0,c/0,c1/3,c10/1,c11/0,c12/0,c13/1,c14/0,c15/1,c2/3,c3/0,c4/2,c5/1,c6/1,c7/0,c8/2,c9/1 ,cons/2,false/0,nil/0,s/1,true/0,ys/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND,FILTERHIGH,FILTERLOW,GE,IF1,IF2,QSORT,append ,filterhigh,filterlow,ge,if1,if2,qsort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c2,c3,c4,c5,c6,c7 ,c8,c9,cons,false,nil,s,true,ys} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPEND(cons(z0,z1),ys()) -> c15(APPEND(z1,ys())) APPEND(nil(),ys()) -> c14() FILTERHIGH(z0,cons(z1,z2)) -> c8(IF2(ge(z1,z0),z0,z1,z2),GE(z1,z0)) FILTERHIGH(z0,nil()) -> c7() FILTERLOW(z0,cons(z1,z2)) -> c4(IF1(ge(z0,z1),z0,z1,z2),GE(z0,z1)) FILTERLOW(z0,nil()) -> c3() GE(z0,0()) -> c11() GE(0(),s(z0)) -> c12() GE(s(z0),s(z1)) -> c13(GE(z0,z1)) IF1(false(),z0,z1,z2) -> c6(FILTERLOW(z0,z2)) IF1(true(),z0,z1,z2) -> c5(FILTERLOW(z0,z2)) IF2(false(),z0,z1,z2) -> c10(FILTERHIGH(z0,z2)) IF2(true(),z0,z1,z2) -> c9(FILTERHIGH(z0,z2)) QSORT(cons(z0,z1)) -> c1(APPEND(qsort(filterlow(z0,cons(z0,z1))),cons(z0,qsort(filterhigh(z0,cons(z0,z1))))) ,QSORT(filterlow(z0,cons(z0,z1))) ,FILTERLOW(z0,cons(z0,z1))) QSORT(cons(z0,z1)) -> c2(APPEND(qsort(filterlow(z0,cons(z0,z1))),cons(z0,qsort(filterhigh(z0,cons(z0,z1))))) ,QSORT(filterhigh(z0,cons(z0,z1))) ,FILTERHIGH(z0,cons(z0,z1))) QSORT(nil()) -> c() - Weak TRS: append(cons(z0,z1),ys()) -> cons(z0,append(z1,ys())) append(nil(),ys()) -> ys() filterhigh(z0,cons(z1,z2)) -> if2(ge(z1,z0),z0,z1,z2) filterhigh(z0,nil()) -> nil() filterlow(z0,cons(z1,z2)) -> if1(ge(z0,z1),z0,z1,z2) filterlow(z0,nil()) -> nil() ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) if1(false(),z0,z1,z2) -> cons(z1,filterlow(z0,z2)) if1(true(),z0,z1,z2) -> filterlow(z0,z2) if2(false(),z0,z1,z2) -> cons(z1,filterhigh(z0,z2)) if2(true(),z0,z1,z2) -> filterhigh(z0,z2) qsort(cons(z0,z1)) -> append(qsort(filterlow(z0,cons(z0,z1))),cons(z0,qsort(filterhigh(z0,cons(z0,z1))))) qsort(nil()) -> nil() - Signature: {APPEND/2,FILTERHIGH/2,FILTERLOW/2,GE/2,IF1/4,IF2/4,QSORT/1,append/2,filterhigh/2,filterlow/2,ge/2,if1/4 ,if2/4,qsort/1} / {0/0,c/0,c1/3,c10/1,c11/0,c12/0,c13/1,c14/0,c15/1,c2/3,c3/0,c4/2,c5/1,c6/1,c7/0,c8/2,c9/1 ,cons/2,false/0,nil/0,s/1,true/0,ys/0} - Obligation: innermost runtime complexity wrt. defined symbols {APPEND,FILTERHIGH,FILTERLOW,GE,IF1,IF2,QSORT,append ,filterhigh,filterlow,ge,if1,if2,qsort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c2,c3,c4,c5,c6,c7 ,c8,c9,cons,false,nil,s,true,ys} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: APPEND(y,ys()){y -> cons(x,y)} = APPEND(cons(x,y),ys()) ->^+ c15(APPEND(y,ys())) = C[APPEND(y,ys()) = APPEND(y,ys()){}] WORST_CASE(Omega(n^1),?)