WORST_CASE(?,O(1)) * Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: filter(cons(X),0(),M) -> cons(0()) filter(cons(X),s(N),M) -> cons(X) nats(N) -> cons(N) sieve(cons(0())) -> cons(0()) sieve(cons(s(N))) -> cons(s(N)) zprimes() -> sieve(nats(s(s(0())))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0} / {0/0,cons/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {filter,nats,sieve,zprimes} and constructors {0,cons,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: filter(cons(X),0(),M) -> cons(0()) filter(cons(X),s(N),M) -> cons(X) nats(N) -> cons(N) sieve(cons(0())) -> cons(0()) sieve(cons(s(N))) -> cons(s(N)) zprimes() -> sieve(nats(s(s(0())))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0} / {0/0,cons/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {filter,nats,sieve,zprimes} and constructors {0,cons,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs filter#(cons(X),0(),M) -> c_1() filter#(cons(X),s(N),M) -> c_2() nats#(N) -> c_3() sieve#(cons(0())) -> c_4() sieve#(cons(s(N))) -> c_5() zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: filter#(cons(X),0(),M) -> c_1() filter#(cons(X),s(N),M) -> c_2() nats#(N) -> c_3() sieve#(cons(0())) -> c_4() sieve#(cons(s(N))) -> c_5() zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X),0(),M) -> cons(0()) filter(cons(X),s(N),M) -> cons(X) nats(N) -> cons(N) sieve(cons(0())) -> cons(0()) sieve(cons(s(N))) -> cons(s(N)) zprimes() -> sieve(nats(s(s(0())))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/1,s/1,c_1/0,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,5} by application of Pre({1,2,3,4,5}) = {6}. Here rules are labelled as follows: 1: filter#(cons(X),0(),M) -> c_1() 2: filter#(cons(X),s(N),M) -> c_2() 3: nats#(N) -> c_3() 4: sieve#(cons(0())) -> c_4() 5: sieve#(cons(s(N))) -> c_5() 6: zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) * Step 4: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak DPs: filter#(cons(X),0(),M) -> c_1() filter#(cons(X),s(N),M) -> c_2() nats#(N) -> c_3() sieve#(cons(0())) -> c_4() sieve#(cons(s(N))) -> c_5() - Weak TRS: filter(cons(X),0(),M) -> cons(0()) filter(cons(X),s(N),M) -> cons(X) nats(N) -> cons(N) sieve(cons(0())) -> cons(0()) sieve(cons(s(N))) -> cons(s(N)) zprimes() -> sieve(nats(s(s(0())))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/1,s/1,c_1/0,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {}. Here rules are labelled as follows: 1: zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) 2: filter#(cons(X),0(),M) -> c_1() 3: filter#(cons(X),s(N),M) -> c_2() 4: nats#(N) -> c_3() 5: sieve#(cons(0())) -> c_4() 6: sieve#(cons(s(N))) -> c_5() * Step 5: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: filter#(cons(X),0(),M) -> c_1() filter#(cons(X),s(N),M) -> c_2() nats#(N) -> c_3() sieve#(cons(0())) -> c_4() sieve#(cons(s(N))) -> c_5() zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X),0(),M) -> cons(0()) filter(cons(X),s(N),M) -> cons(X) nats(N) -> cons(N) sieve(cons(0())) -> cons(0()) sieve(cons(s(N))) -> cons(s(N)) zprimes() -> sieve(nats(s(s(0())))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/1,s/1,c_1/0,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:filter#(cons(X),0(),M) -> c_1() 2:W:filter#(cons(X),s(N),M) -> c_2() 3:W:nats#(N) -> c_3() 4:W:sieve#(cons(0())) -> c_4() 5:W:sieve#(cons(s(N))) -> c_5() 6:W:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) -->_1 sieve#(cons(s(N))) -> c_5():5 -->_1 sieve#(cons(0())) -> c_4():4 -->_2 nats#(N) -> c_3():3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) 5: sieve#(cons(s(N))) -> c_5() 4: sieve#(cons(0())) -> c_4() 3: nats#(N) -> c_3() 2: filter#(cons(X),s(N),M) -> c_2() 1: filter#(cons(X),0(),M) -> c_1() * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: filter(cons(X),0(),M) -> cons(0()) filter(cons(X),s(N),M) -> cons(X) nats(N) -> cons(N) sieve(cons(0())) -> cons(0()) sieve(cons(s(N))) -> cons(s(N)) zprimes() -> sieve(nats(s(s(0())))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/1,s/1,c_1/0,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))