WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FILTER(z0,z1) -> c13() A__FILTER(s(s(z0)),cons(z1,z2)) -> c11(A__IF(divides(s(s(mark(z0))),mark(z1)) ,filter(s(s(z0)),z2) ,cons(z1,filter(z0,sieve(z1)))) ,MARK(z0)) A__FILTER(s(s(z0)),cons(z1,z2)) -> c12(A__IF(divides(s(s(mark(z0))),mark(z1)) ,filter(s(s(z0)),z2) ,cons(z1,filter(z0,sieve(z1)))) ,MARK(z1)) A__FROM(z0) -> c2(MARK(z0)) A__FROM(z0) -> c3() A__HEAD(z0) -> c5() A__HEAD(cons(z0,z1)) -> c4(MARK(z0)) A__IF(z0,z1,z2) -> c10() A__IF(false(),z0,z1) -> c9(MARK(z1)) A__IF(true(),z0,z1) -> c8(MARK(z0)) A__PRIMES() -> c(A__SIEVE(a__from(s(s(0())))),A__FROM(s(s(0())))) A__PRIMES() -> c1() A__SIEVE(z0) -> c15() A__SIEVE(cons(z0,z1)) -> c14(MARK(z0)) A__TAIL(z0) -> c7() A__TAIL(cons(z0,z1)) -> c6(MARK(z1)) MARK(0()) -> c25() MARK(cons(z0,z1)) -> c26(MARK(z0)) MARK(divides(z0,z1)) -> c29(MARK(z0)) MARK(divides(z0,z1)) -> c30(MARK(z1)) MARK(false()) -> c28() MARK(filter(z0,z1)) -> c22(A__FILTER(mark(z0),mark(z1)),MARK(z0)) MARK(filter(z0,z1)) -> c23(A__FILTER(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c18(A__FROM(mark(z0)),MARK(z0)) MARK(head(z0)) -> c19(A__HEAD(mark(z0)),MARK(z0)) MARK(if(z0,z1,z2)) -> c21(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(primes()) -> c16(A__PRIMES()) MARK(s(z0)) -> c24(MARK(z0)) MARK(sieve(z0)) -> c17(A__SIEVE(mark(z0)),MARK(z0)) MARK(tail(z0)) -> c20(A__TAIL(mark(z0)),MARK(z0)) MARK(true()) -> c27() - Weak TRS: a__filter(z0,z1) -> filter(z0,z1) a__filter(s(s(z0)),cons(z1,z2)) -> a__if(divides(s(s(mark(z0))),mark(z1)) ,filter(s(s(z0)),z2) ,cons(z1,filter(z0,sieve(z1)))) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> mark(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) a__primes() -> a__sieve(a__from(s(s(0())))) a__primes() -> primes() a__sieve(z0) -> sieve(z0) a__sieve(cons(z0,z1)) -> cons(mark(z0),filter(z0,sieve(z1))) a__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> mark(z1) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(divides(z0,z1)) -> divides(mark(z0),mark(z1)) mark(false()) -> false() mark(filter(z0,z1)) -> a__filter(mark(z0),mark(z1)) mark(from(z0)) -> a__from(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(primes()) -> a__primes() mark(s(z0)) -> s(mark(z0)) mark(sieve(z0)) -> a__sieve(mark(z0)) mark(tail(z0)) -> a__tail(mark(z0)) mark(true()) -> true() - Signature: {A__FILTER/2,A__FROM/1,A__HEAD/1,A__IF/3,A__PRIMES/0,A__SIEVE/1,A__TAIL/1,MARK/1,a__filter/2,a__from/1 ,a__head/1,a__if/3,a__primes/0,a__sieve/1,a__tail/1,mark/1} / {0/0,c/2,c1/0,c10/0,c11/2,c12/2,c13/0,c14/1 ,c15/0,c16/1,c17/2,c18/2,c19/2,c2/1,c20/2,c21/2,c22/2,c23/2,c24/1,c25/0,c26/1,c27/0,c28/0,c29/1,c3/0,c30/1 ,c4/1,c5/0,c6/1,c7/0,c8/1,c9/1,cons/2,divides/2,false/0,filter/2,from/1,head/1,if/3,primes/0,s/1,sieve/1 ,tail/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__FILTER,A__FROM,A__HEAD,A__IF,A__PRIMES,A__SIEVE ,A__TAIL,MARK,a__filter,a__from,a__head,a__if,a__primes,a__sieve,a__tail,mark} and constructors {0,c,c1,c10 ,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c4,c5,c6,c7,c8,c9 ,cons,divides,false,filter,from,head,if,primes,s,sieve,tail,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FILTER(z0,z1) -> c13() A__FILTER(s(s(z0)),cons(z1,z2)) -> c11(A__IF(divides(s(s(mark(z0))),mark(z1)) ,filter(s(s(z0)),z2) ,cons(z1,filter(z0,sieve(z1)))) ,MARK(z0)) A__FILTER(s(s(z0)),cons(z1,z2)) -> c12(A__IF(divides(s(s(mark(z0))),mark(z1)) ,filter(s(s(z0)),z2) ,cons(z1,filter(z0,sieve(z1)))) ,MARK(z1)) A__FROM(z0) -> c2(MARK(z0)) A__FROM(z0) -> c3() A__HEAD(z0) -> c5() A__HEAD(cons(z0,z1)) -> c4(MARK(z0)) A__IF(z0,z1,z2) -> c10() A__IF(false(),z0,z1) -> c9(MARK(z1)) A__IF(true(),z0,z1) -> c8(MARK(z0)) A__PRIMES() -> c(A__SIEVE(a__from(s(s(0())))),A__FROM(s(s(0())))) A__PRIMES() -> c1() A__SIEVE(z0) -> c15() A__SIEVE(cons(z0,z1)) -> c14(MARK(z0)) A__TAIL(z0) -> c7() A__TAIL(cons(z0,z1)) -> c6(MARK(z1)) MARK(0()) -> c25() MARK(cons(z0,z1)) -> c26(MARK(z0)) MARK(divides(z0,z1)) -> c29(MARK(z0)) MARK(divides(z0,z1)) -> c30(MARK(z1)) MARK(false()) -> c28() MARK(filter(z0,z1)) -> c22(A__FILTER(mark(z0),mark(z1)),MARK(z0)) MARK(filter(z0,z1)) -> c23(A__FILTER(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c18(A__FROM(mark(z0)),MARK(z0)) MARK(head(z0)) -> c19(A__HEAD(mark(z0)),MARK(z0)) MARK(if(z0,z1,z2)) -> c21(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(primes()) -> c16(A__PRIMES()) MARK(s(z0)) -> c24(MARK(z0)) MARK(sieve(z0)) -> c17(A__SIEVE(mark(z0)),MARK(z0)) MARK(tail(z0)) -> c20(A__TAIL(mark(z0)),MARK(z0)) MARK(true()) -> c27() - Weak TRS: a__filter(z0,z1) -> filter(z0,z1) a__filter(s(s(z0)),cons(z1,z2)) -> a__if(divides(s(s(mark(z0))),mark(z1)) ,filter(s(s(z0)),z2) ,cons(z1,filter(z0,sieve(z1)))) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> mark(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) a__primes() -> a__sieve(a__from(s(s(0())))) a__primes() -> primes() a__sieve(z0) -> sieve(z0) a__sieve(cons(z0,z1)) -> cons(mark(z0),filter(z0,sieve(z1))) a__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> mark(z1) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(divides(z0,z1)) -> divides(mark(z0),mark(z1)) mark(false()) -> false() mark(filter(z0,z1)) -> a__filter(mark(z0),mark(z1)) mark(from(z0)) -> a__from(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(primes()) -> a__primes() mark(s(z0)) -> s(mark(z0)) mark(sieve(z0)) -> a__sieve(mark(z0)) mark(tail(z0)) -> a__tail(mark(z0)) mark(true()) -> true() - Signature: {A__FILTER/2,A__FROM/1,A__HEAD/1,A__IF/3,A__PRIMES/0,A__SIEVE/1,A__TAIL/1,MARK/1,a__filter/2,a__from/1 ,a__head/1,a__if/3,a__primes/0,a__sieve/1,a__tail/1,mark/1} / {0/0,c/2,c1/0,c10/0,c11/2,c12/2,c13/0,c14/1 ,c15/0,c16/1,c17/2,c18/2,c19/2,c2/1,c20/2,c21/2,c22/2,c23/2,c24/1,c25/0,c26/1,c27/0,c28/0,c29/1,c3/0,c30/1 ,c4/1,c5/0,c6/1,c7/0,c8/1,c9/1,cons/2,divides/2,false/0,filter/2,from/1,head/1,if/3,primes/0,s/1,sieve/1 ,tail/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__FILTER,A__FROM,A__HEAD,A__IF,A__PRIMES,A__SIEVE ,A__TAIL,MARK,a__filter,a__from,a__head,a__if,a__primes,a__sieve,a__tail,mark} and constructors {0,c,c1,c10 ,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c4,c5,c6,c7,c8,c9 ,cons,divides,false,filter,from,head,if,primes,s,sieve,tail,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FILTER(z0,z1) -> c13() A__FILTER(s(s(z0)),cons(z1,z2)) -> c11(A__IF(divides(s(s(mark(z0))),mark(z1)) ,filter(s(s(z0)),z2) ,cons(z1,filter(z0,sieve(z1)))) ,MARK(z0)) A__FILTER(s(s(z0)),cons(z1,z2)) -> c12(A__IF(divides(s(s(mark(z0))),mark(z1)) ,filter(s(s(z0)),z2) ,cons(z1,filter(z0,sieve(z1)))) ,MARK(z1)) A__FROM(z0) -> c2(MARK(z0)) A__FROM(z0) -> c3() A__HEAD(z0) -> c5() A__HEAD(cons(z0,z1)) -> c4(MARK(z0)) A__IF(z0,z1,z2) -> c10() A__IF(false(),z0,z1) -> c9(MARK(z1)) A__IF(true(),z0,z1) -> c8(MARK(z0)) A__PRIMES() -> c(A__SIEVE(a__from(s(s(0())))),A__FROM(s(s(0())))) A__PRIMES() -> c1() A__SIEVE(z0) -> c15() A__SIEVE(cons(z0,z1)) -> c14(MARK(z0)) A__TAIL(z0) -> c7() A__TAIL(cons(z0,z1)) -> c6(MARK(z1)) MARK(0()) -> c25() MARK(cons(z0,z1)) -> c26(MARK(z0)) MARK(divides(z0,z1)) -> c29(MARK(z0)) MARK(divides(z0,z1)) -> c30(MARK(z1)) MARK(false()) -> c28() MARK(filter(z0,z1)) -> c22(A__FILTER(mark(z0),mark(z1)),MARK(z0)) MARK(filter(z0,z1)) -> c23(A__FILTER(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c18(A__FROM(mark(z0)),MARK(z0)) MARK(head(z0)) -> c19(A__HEAD(mark(z0)),MARK(z0)) MARK(if(z0,z1,z2)) -> c21(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(primes()) -> c16(A__PRIMES()) MARK(s(z0)) -> c24(MARK(z0)) MARK(sieve(z0)) -> c17(A__SIEVE(mark(z0)),MARK(z0)) MARK(tail(z0)) -> c20(A__TAIL(mark(z0)),MARK(z0)) MARK(true()) -> c27() - Weak TRS: a__filter(z0,z1) -> filter(z0,z1) a__filter(s(s(z0)),cons(z1,z2)) -> a__if(divides(s(s(mark(z0))),mark(z1)) ,filter(s(s(z0)),z2) ,cons(z1,filter(z0,sieve(z1)))) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> mark(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) a__primes() -> a__sieve(a__from(s(s(0())))) a__primes() -> primes() a__sieve(z0) -> sieve(z0) a__sieve(cons(z0,z1)) -> cons(mark(z0),filter(z0,sieve(z1))) a__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> mark(z1) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(divides(z0,z1)) -> divides(mark(z0),mark(z1)) mark(false()) -> false() mark(filter(z0,z1)) -> a__filter(mark(z0),mark(z1)) mark(from(z0)) -> a__from(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(primes()) -> a__primes() mark(s(z0)) -> s(mark(z0)) mark(sieve(z0)) -> a__sieve(mark(z0)) mark(tail(z0)) -> a__tail(mark(z0)) mark(true()) -> true() - Signature: {A__FILTER/2,A__FROM/1,A__HEAD/1,A__IF/3,A__PRIMES/0,A__SIEVE/1,A__TAIL/1,MARK/1,a__filter/2,a__from/1 ,a__head/1,a__if/3,a__primes/0,a__sieve/1,a__tail/1,mark/1} / {0/0,c/2,c1/0,c10/0,c11/2,c12/2,c13/0,c14/1 ,c15/0,c16/1,c17/2,c18/2,c19/2,c2/1,c20/2,c21/2,c22/2,c23/2,c24/1,c25/0,c26/1,c27/0,c28/0,c29/1,c3/0,c30/1 ,c4/1,c5/0,c6/1,c7/0,c8/1,c9/1,cons/2,divides/2,false/0,filter/2,from/1,head/1,if/3,primes/0,s/1,sieve/1 ,tail/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__FILTER,A__FROM,A__HEAD,A__IF,A__PRIMES,A__SIEVE ,A__TAIL,MARK,a__filter,a__from,a__head,a__if,a__primes,a__sieve,a__tail,mark} and constructors {0,c,c1,c10 ,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c4,c5,c6,c7,c8,c9 ,cons,divides,false,filter,from,head,if,primes,s,sieve,tail,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> cons(x,y)} = MARK(cons(x,y)) ->^+ c26(MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)