WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FILTER(z0,z1,z2) -> c2() A__FILTER(cons(z0,z1),0(),z2) -> c() A__FILTER(cons(z0,z1),s(z2),z3) -> c1(MARK(z0)) A__NATS(z0) -> c6(MARK(z0)) A__NATS(z0) -> c7() A__SIEVE(z0) -> c5() A__SIEVE(cons(0(),z0)) -> c3() A__SIEVE(cons(s(z0),z1)) -> c4(MARK(z0)) A__ZPRIMES() -> c8(A__SIEVE(a__nats(s(s(0())))),A__NATS(s(s(0())))) A__ZPRIMES() -> c9() MARK(0()) -> c17() MARK(cons(z0,z1)) -> c16(MARK(z0)) MARK(filter(z0,z1,z2)) -> c10(A__FILTER(mark(z0),mark(z1),mark(z2)),MARK(z0)) MARK(filter(z0,z1,z2)) -> c11(A__FILTER(mark(z0),mark(z1),mark(z2)),MARK(z1)) MARK(filter(z0,z1,z2)) -> c12(A__FILTER(mark(z0),mark(z1),mark(z2)),MARK(z2)) MARK(nats(z0)) -> c14(A__NATS(mark(z0)),MARK(z0)) MARK(s(z0)) -> c18(MARK(z0)) MARK(sieve(z0)) -> c13(A__SIEVE(mark(z0)),MARK(z0)) MARK(zprimes()) -> c15(A__ZPRIMES()) - Weak TRS: a__filter(z0,z1,z2) -> filter(z0,z1,z2) a__filter(cons(z0,z1),0(),z2) -> cons(0(),filter(z1,z2,z2)) a__filter(cons(z0,z1),s(z2),z3) -> cons(mark(z0),filter(z1,z2,z3)) a__nats(z0) -> cons(mark(z0),nats(s(z0))) a__nats(z0) -> nats(z0) a__sieve(z0) -> sieve(z0) a__sieve(cons(0(),z0)) -> cons(0(),sieve(z0)) a__sieve(cons(s(z0),z1)) -> cons(s(mark(z0)),sieve(filter(z1,z0,z0))) a__zprimes() -> a__sieve(a__nats(s(s(0())))) a__zprimes() -> zprimes() mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(filter(z0,z1,z2)) -> a__filter(mark(z0),mark(z1),mark(z2)) mark(nats(z0)) -> a__nats(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(sieve(z0)) -> a__sieve(mark(z0)) mark(zprimes()) -> a__zprimes() - Signature: {A__FILTER/3,A__NATS/1,A__SIEVE/1,A__ZPRIMES/0,MARK/1,a__filter/3,a__nats/1,a__sieve/1,a__zprimes/0 ,mark/1} / {0/0,c/0,c1/1,c10/2,c11/2,c12/2,c13/2,c14/2,c15/1,c16/1,c17/0,c18/1,c2/0,c3/0,c4/1,c5/0,c6/1,c7/0 ,c8/2,c9/0,cons/2,filter/3,nats/1,s/1,sieve/1,zprimes/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__FILTER,A__NATS,A__SIEVE,A__ZPRIMES,MARK,a__filter ,a__nats,a__sieve,a__zprimes,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3,c4,c5 ,c6,c7,c8,c9,cons,filter,nats,s,sieve,zprimes} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FILTER(z0,z1,z2) -> c2() A__FILTER(cons(z0,z1),0(),z2) -> c() A__FILTER(cons(z0,z1),s(z2),z3) -> c1(MARK(z0)) A__NATS(z0) -> c6(MARK(z0)) A__NATS(z0) -> c7() A__SIEVE(z0) -> c5() A__SIEVE(cons(0(),z0)) -> c3() A__SIEVE(cons(s(z0),z1)) -> c4(MARK(z0)) A__ZPRIMES() -> c8(A__SIEVE(a__nats(s(s(0())))),A__NATS(s(s(0())))) A__ZPRIMES() -> c9() MARK(0()) -> c17() MARK(cons(z0,z1)) -> c16(MARK(z0)) MARK(filter(z0,z1,z2)) -> c10(A__FILTER(mark(z0),mark(z1),mark(z2)),MARK(z0)) MARK(filter(z0,z1,z2)) -> c11(A__FILTER(mark(z0),mark(z1),mark(z2)),MARK(z1)) MARK(filter(z0,z1,z2)) -> c12(A__FILTER(mark(z0),mark(z1),mark(z2)),MARK(z2)) MARK(nats(z0)) -> c14(A__NATS(mark(z0)),MARK(z0)) MARK(s(z0)) -> c18(MARK(z0)) MARK(sieve(z0)) -> c13(A__SIEVE(mark(z0)),MARK(z0)) MARK(zprimes()) -> c15(A__ZPRIMES()) - Weak TRS: a__filter(z0,z1,z2) -> filter(z0,z1,z2) a__filter(cons(z0,z1),0(),z2) -> cons(0(),filter(z1,z2,z2)) a__filter(cons(z0,z1),s(z2),z3) -> cons(mark(z0),filter(z1,z2,z3)) a__nats(z0) -> cons(mark(z0),nats(s(z0))) a__nats(z0) -> nats(z0) a__sieve(z0) -> sieve(z0) a__sieve(cons(0(),z0)) -> cons(0(),sieve(z0)) a__sieve(cons(s(z0),z1)) -> cons(s(mark(z0)),sieve(filter(z1,z0,z0))) a__zprimes() -> a__sieve(a__nats(s(s(0())))) a__zprimes() -> zprimes() mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(filter(z0,z1,z2)) -> a__filter(mark(z0),mark(z1),mark(z2)) mark(nats(z0)) -> a__nats(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(sieve(z0)) -> a__sieve(mark(z0)) mark(zprimes()) -> a__zprimes() - Signature: {A__FILTER/3,A__NATS/1,A__SIEVE/1,A__ZPRIMES/0,MARK/1,a__filter/3,a__nats/1,a__sieve/1,a__zprimes/0 ,mark/1} / {0/0,c/0,c1/1,c10/2,c11/2,c12/2,c13/2,c14/2,c15/1,c16/1,c17/0,c18/1,c2/0,c3/0,c4/1,c5/0,c6/1,c7/0 ,c8/2,c9/0,cons/2,filter/3,nats/1,s/1,sieve/1,zprimes/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__FILTER,A__NATS,A__SIEVE,A__ZPRIMES,MARK,a__filter ,a__nats,a__sieve,a__zprimes,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3,c4,c5 ,c6,c7,c8,c9,cons,filter,nats,s,sieve,zprimes} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FILTER(z0,z1,z2) -> c2() A__FILTER(cons(z0,z1),0(),z2) -> c() A__FILTER(cons(z0,z1),s(z2),z3) -> c1(MARK(z0)) A__NATS(z0) -> c6(MARK(z0)) A__NATS(z0) -> c7() A__SIEVE(z0) -> c5() A__SIEVE(cons(0(),z0)) -> c3() A__SIEVE(cons(s(z0),z1)) -> c4(MARK(z0)) A__ZPRIMES() -> c8(A__SIEVE(a__nats(s(s(0())))),A__NATS(s(s(0())))) A__ZPRIMES() -> c9() MARK(0()) -> c17() MARK(cons(z0,z1)) -> c16(MARK(z0)) MARK(filter(z0,z1,z2)) -> c10(A__FILTER(mark(z0),mark(z1),mark(z2)),MARK(z0)) MARK(filter(z0,z1,z2)) -> c11(A__FILTER(mark(z0),mark(z1),mark(z2)),MARK(z1)) MARK(filter(z0,z1,z2)) -> c12(A__FILTER(mark(z0),mark(z1),mark(z2)),MARK(z2)) MARK(nats(z0)) -> c14(A__NATS(mark(z0)),MARK(z0)) MARK(s(z0)) -> c18(MARK(z0)) MARK(sieve(z0)) -> c13(A__SIEVE(mark(z0)),MARK(z0)) MARK(zprimes()) -> c15(A__ZPRIMES()) - Weak TRS: a__filter(z0,z1,z2) -> filter(z0,z1,z2) a__filter(cons(z0,z1),0(),z2) -> cons(0(),filter(z1,z2,z2)) a__filter(cons(z0,z1),s(z2),z3) -> cons(mark(z0),filter(z1,z2,z3)) a__nats(z0) -> cons(mark(z0),nats(s(z0))) a__nats(z0) -> nats(z0) a__sieve(z0) -> sieve(z0) a__sieve(cons(0(),z0)) -> cons(0(),sieve(z0)) a__sieve(cons(s(z0),z1)) -> cons(s(mark(z0)),sieve(filter(z1,z0,z0))) a__zprimes() -> a__sieve(a__nats(s(s(0())))) a__zprimes() -> zprimes() mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(filter(z0,z1,z2)) -> a__filter(mark(z0),mark(z1),mark(z2)) mark(nats(z0)) -> a__nats(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(sieve(z0)) -> a__sieve(mark(z0)) mark(zprimes()) -> a__zprimes() - Signature: {A__FILTER/3,A__NATS/1,A__SIEVE/1,A__ZPRIMES/0,MARK/1,a__filter/3,a__nats/1,a__sieve/1,a__zprimes/0 ,mark/1} / {0/0,c/0,c1/1,c10/2,c11/2,c12/2,c13/2,c14/2,c15/1,c16/1,c17/0,c18/1,c2/0,c3/0,c4/1,c5/0,c6/1,c7/0 ,c8/2,c9/0,cons/2,filter/3,nats/1,s/1,sieve/1,zprimes/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__FILTER,A__NATS,A__SIEVE,A__ZPRIMES,MARK,a__filter ,a__nats,a__sieve,a__zprimes,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c2,c3,c4,c5 ,c6,c7,c8,c9,cons,filter,nats,s,sieve,zprimes} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> cons(x,y)} = MARK(cons(x,y)) ->^+ c16(MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)