* 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: UsableRules 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: UsableRules + Details: We replace rewrite rules by usable rules: nats(N) -> cons(N) 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())))) * Step 4: Trivial 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: nats(N) -> cons(N) - 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: Trivial + Details: Consider the dependency graph 1:S:filter#(cons(X),0(),M) -> c_1() 2:S:filter#(cons(X),s(N),M) -> c_2() 3:S:nats#(N) -> c_3() 4:S:sieve#(cons(0())) -> c_4() 5:S:sieve#(cons(s(N))) -> c_5() 6:S: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 dependency graph contains no loops, we remove all dependency pairs. * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: nats(N) -> cons(N) - 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))