WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APPEND(cons(z0,z1),ys()) -> c16(APPEND(z1,ys())) APPEND(nil(),ys()) -> c15() FILTERHIGH(z0,cons(z1,z2)) -> c9(IF2(ge(z1,z0),z0,z1,z2),GE(z1,z0)) FILTERHIGH(z0,nil()) -> c8() FILTERLOW(z0,cons(z1,z2)) -> c5(IF1(ge(z0,z1),z0,z1,z2),GE(z0,z1)) FILTERLOW(z0,nil()) -> c4() GE(z0,0()) -> c12() GE(0(),s(z0)) -> c13() GE(s(z0),s(z1)) -> c14(GE(z0,z1)) IF1(false(),z0,z1,z2) -> c7(FILTERLOW(z0,z2)) IF1(true(),z0,z1,z2) -> c6(FILTERLOW(z0,z2)) IF2(false(),z0,z1,z2) -> c11(FILTERHIGH(z0,z2)) IF2(true(),z0,z1,z2) -> c10(FILTERHIGH(z0,z2)) LAST(cons(z0,cons(z1,z2))) -> c19(LAST(cons(z1,z2))) LAST(cons(z0,nil())) -> c18() LAST(nil()) -> c17() QSORT(cons(z0,z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) ,QSORT(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,FILTERLOW(last(cons(z0,z1)),cons(z0,z1)) ,LAST(cons(z0,z1))) QSORT(cons(z0,z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) ,LAST(cons(z0,z1))) QSORT(cons(z0,z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) ,QSORT(filterhigh(last(cons(z0,z1)),cons(z0,z1))) ,FILTERHIGH(last(cons(z0,z1)),cons(z0,z1)) ,LAST(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) last(cons(z0,cons(z1,z2))) -> last(cons(z1,z2)) last(cons(z0,nil())) -> z0 last(nil()) -> 0() qsort(cons(z0,z1)) -> append(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) qsort(nil()) -> nil() - Signature: {APPEND/2,FILTERHIGH/2,FILTERLOW/2,GE/2,IF1/4,IF2/4,LAST/1,QSORT/1,append/2,filterhigh/2,filterlow/2,ge/2 ,if1/4,if2/4,last/1,qsort/1} / {0/0,c/0,c1/4,c10/1,c11/1,c12/0,c13/0,c14/1,c15/0,c16/1,c17/0,c18/0,c19/1 ,c2/2,c3/4,c4/0,c5/2,c6/1,c7/1,c8/0,c9/2,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,LAST,QSORT,append ,filterhigh,filterlow,ge,if1,if2,last,qsort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18 ,c19,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()) -> c16(APPEND(z1,ys())) APPEND(nil(),ys()) -> c15() FILTERHIGH(z0,cons(z1,z2)) -> c9(IF2(ge(z1,z0),z0,z1,z2),GE(z1,z0)) FILTERHIGH(z0,nil()) -> c8() FILTERLOW(z0,cons(z1,z2)) -> c5(IF1(ge(z0,z1),z0,z1,z2),GE(z0,z1)) FILTERLOW(z0,nil()) -> c4() GE(z0,0()) -> c12() GE(0(),s(z0)) -> c13() GE(s(z0),s(z1)) -> c14(GE(z0,z1)) IF1(false(),z0,z1,z2) -> c7(FILTERLOW(z0,z2)) IF1(true(),z0,z1,z2) -> c6(FILTERLOW(z0,z2)) IF2(false(),z0,z1,z2) -> c11(FILTERHIGH(z0,z2)) IF2(true(),z0,z1,z2) -> c10(FILTERHIGH(z0,z2)) LAST(cons(z0,cons(z1,z2))) -> c19(LAST(cons(z1,z2))) LAST(cons(z0,nil())) -> c18() LAST(nil()) -> c17() QSORT(cons(z0,z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) ,QSORT(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,FILTERLOW(last(cons(z0,z1)),cons(z0,z1)) ,LAST(cons(z0,z1))) QSORT(cons(z0,z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) ,LAST(cons(z0,z1))) QSORT(cons(z0,z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) ,QSORT(filterhigh(last(cons(z0,z1)),cons(z0,z1))) ,FILTERHIGH(last(cons(z0,z1)),cons(z0,z1)) ,LAST(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) last(cons(z0,cons(z1,z2))) -> last(cons(z1,z2)) last(cons(z0,nil())) -> z0 last(nil()) -> 0() qsort(cons(z0,z1)) -> append(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) qsort(nil()) -> nil() - Signature: {APPEND/2,FILTERHIGH/2,FILTERLOW/2,GE/2,IF1/4,IF2/4,LAST/1,QSORT/1,append/2,filterhigh/2,filterlow/2,ge/2 ,if1/4,if2/4,last/1,qsort/1} / {0/0,c/0,c1/4,c10/1,c11/1,c12/0,c13/0,c14/1,c15/0,c16/1,c17/0,c18/0,c19/1 ,c2/2,c3/4,c4/0,c5/2,c6/1,c7/1,c8/0,c9/2,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,LAST,QSORT,append ,filterhigh,filterlow,ge,if1,if2,last,qsort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18 ,c19,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()) -> c16(APPEND(z1,ys())) APPEND(nil(),ys()) -> c15() FILTERHIGH(z0,cons(z1,z2)) -> c9(IF2(ge(z1,z0),z0,z1,z2),GE(z1,z0)) FILTERHIGH(z0,nil()) -> c8() FILTERLOW(z0,cons(z1,z2)) -> c5(IF1(ge(z0,z1),z0,z1,z2),GE(z0,z1)) FILTERLOW(z0,nil()) -> c4() GE(z0,0()) -> c12() GE(0(),s(z0)) -> c13() GE(s(z0),s(z1)) -> c14(GE(z0,z1)) IF1(false(),z0,z1,z2) -> c7(FILTERLOW(z0,z2)) IF1(true(),z0,z1,z2) -> c6(FILTERLOW(z0,z2)) IF2(false(),z0,z1,z2) -> c11(FILTERHIGH(z0,z2)) IF2(true(),z0,z1,z2) -> c10(FILTERHIGH(z0,z2)) LAST(cons(z0,cons(z1,z2))) -> c19(LAST(cons(z1,z2))) LAST(cons(z0,nil())) -> c18() LAST(nil()) -> c17() QSORT(cons(z0,z1)) -> c1(APPEND(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) ,QSORT(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,FILTERLOW(last(cons(z0,z1)),cons(z0,z1)) ,LAST(cons(z0,z1))) QSORT(cons(z0,z1)) -> c2(APPEND(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) ,LAST(cons(z0,z1))) QSORT(cons(z0,z1)) -> c3(APPEND(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) ,QSORT(filterhigh(last(cons(z0,z1)),cons(z0,z1))) ,FILTERHIGH(last(cons(z0,z1)),cons(z0,z1)) ,LAST(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) last(cons(z0,cons(z1,z2))) -> last(cons(z1,z2)) last(cons(z0,nil())) -> z0 last(nil()) -> 0() qsort(cons(z0,z1)) -> append(qsort(filterlow(last(cons(z0,z1)),cons(z0,z1))) ,cons(last(cons(z0,z1)),qsort(filterhigh(last(cons(z0,z1)),cons(z0,z1))))) qsort(nil()) -> nil() - Signature: {APPEND/2,FILTERHIGH/2,FILTERLOW/2,GE/2,IF1/4,IF2/4,LAST/1,QSORT/1,append/2,filterhigh/2,filterlow/2,ge/2 ,if1/4,if2/4,last/1,qsort/1} / {0/0,c/0,c1/4,c10/1,c11/1,c12/0,c13/0,c14/1,c15/0,c16/1,c17/0,c18/0,c19/1 ,c2/2,c3/4,c4/0,c5/2,c6/1,c7/1,c8/0,c9/2,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,LAST,QSORT,append ,filterhigh,filterlow,ge,if1,if2,last,qsort} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18 ,c19,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()) ->^+ c16(APPEND(y,ys())) = C[APPEND(y,ys()) = APPEND(y,ys()){}] WORST_CASE(Omega(n^1),?)