MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) sieve(cons(0(),Y)) -> cons(0(),sieve(Y)) sieve(cons(s(N),Y)) -> cons(s(N),sieve(filter(Y,N,N))) zprimes() -> sieve(nats(s(s(0())))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0} / {0/0,cons/2,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,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) sieve(cons(0(),Y)) -> cons(0(),sieve(Y)) sieve(cons(s(N),Y)) -> cons(s(N),sieve(filter(Y,N,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/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/2,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: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) * Step 3: Decompose MAYBE + Considered Problem: - Strict DPs: filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/2,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) - Weak DPs: nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/2,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} Problem (S) - Strict DPs: nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak DPs: filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/2,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} ** Step 3.a:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) - Weak DPs: nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/2,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:S:filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) -->_1 filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)):2 -->_1 filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)):1 2:S:filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) -->_1 filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)):1 -->_1 filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)):2 3:W:nats#(N) -> c_3(nats#(s(N))) -->_1 nats#(N) -> c_3(nats#(s(N))):3 4:W:sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):5 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):4 5:W:sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) -->_2 filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)):1 -->_2 filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):4 -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):5 6:W:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) -->_2 nats#(N) -> c_3(nats#(s(N))):3 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):4 -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: nats#(N) -> c_3(nats#(s(N))) ** Step 3.a:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) - Weak DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/2,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) -->_1 filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)):2 -->_1 filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)):1 2:S:filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) -->_1 filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)):1 -->_1 filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)):2 4:W:sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):5 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):4 5:W:sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) -->_2 filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)):1 -->_2 filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):4 -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):5 6:W:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):4 -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: zprimes#() -> c_6(sieve#(nats(s(s(0()))))) ** Step 3.a:3: Failure MAYBE + Considered Problem: - Strict DPs: filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) - Weak DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0()))))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/2,c_6/1} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 3.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak DPs: filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/2,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:S:nats#(N) -> c_3(nats#(s(N))) -->_1 nats#(N) -> c_3(nats#(s(N))):1 2:S:sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):3 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):2 3:S:sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) -->_2 filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)):6 -->_2 filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)):5 -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):3 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):2 4:S:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):3 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):2 -->_2 nats#(N) -> c_3(nats#(s(N))):1 5:W:filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) -->_1 filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)):6 -->_1 filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)):5 6:W:filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) -->_1 filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)):6 -->_1 filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: filter#(cons(X,Y),s(N),M) -> c_2(filter#(Y,N,M)) 5: filter#(cons(X,Y),0(),M) -> c_1(filter#(Y,M,M)) ** Step 3.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/2,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:nats#(N) -> c_3(nats#(s(N))) -->_1 nats#(N) -> c_3(nats#(s(N))):1 2:S:sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):3 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):2 3:S:sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):3 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):2 4:S:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N)),filter#(Y,N,N)):3 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):2 -->_2 nats#(N) -> c_3(nats#(s(N))):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) ** Step 3.b:3: Decompose MAYBE + Considered Problem: - Strict DPs: nats#(N) -> c_3(nats#(s(N))) sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: nats#(N) -> c_3(nats#(s(N))) - Weak DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} Problem (S) - Strict DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak DPs: nats#(N) -> c_3(nats#(s(N))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} *** Step 3.b:3.a:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: nats#(N) -> c_3(nats#(s(N))) - Weak DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,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:S:nats#(N) -> c_3(nats#(s(N))) -->_1 nats#(N) -> c_3(nats#(s(N))):1 2:W:sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):3 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):2 3:W:sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):2 -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):3 4:W:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) -->_2 nats#(N) -> c_3(nats#(s(N))):1 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):2 -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) 3: sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) *** Step 3.b:3.a:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: nats#(N) -> c_3(nats#(s(N))) - Weak DPs: zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:nats#(N) -> c_3(nats#(s(N))) -->_1 nats#(N) -> c_3(nats#(s(N))):1 4:W:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) -->_2 nats#(N) -> c_3(nats#(s(N))):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: zprimes#() -> c_6(nats#(s(s(0())))) *** Step 3.b:3.a:3: UsableRules MAYBE + Considered Problem: - Strict DPs: nats#(N) -> c_3(nats#(s(N))) - Weak DPs: zprimes#() -> c_6(nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/1} - 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) -> c_3(nats#(s(N))) zprimes#() -> c_6(nats#(s(s(0())))) *** Step 3.b:3.a:4: Failure MAYBE + Considered Problem: - Strict DPs: nats#(N) -> c_3(nats#(s(N))) - Weak DPs: zprimes#() -> c_6(nats#(s(s(0())))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/1} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. *** Step 3.b:3.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak DPs: nats#(N) -> c_3(nats#(s(N))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,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:S:sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):1 2:S:sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):1 3:S:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) -->_2 nats#(N) -> c_3(nats#(s(N))):4 -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):1 4:W:nats#(N) -> c_3(nats#(s(N))) -->_1 nats#(N) -> c_3(nats#(s(N))):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: nats#(N) -> c_3(nats#(s(N))) *** Step 3.b:3.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/2} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):1 2:S:sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):1 3:S:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0())))) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: zprimes#() -> c_6(sieve#(nats(s(s(0()))))) *** Step 3.b:3.b:3: Decompose MAYBE + Considered Problem: - Strict DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) zprimes#() -> c_6(sieve#(nats(s(s(0()))))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/1} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) - Weak DPs: zprimes#() -> c_6(sieve#(nats(s(s(0()))))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/1} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} Problem (S) - Strict DPs: zprimes#() -> c_6(sieve#(nats(s(s(0()))))) - Weak DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/1} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} **** Step 3.b:3.b:3.a:1: Failure MAYBE + Considered Problem: - Strict DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) - Weak DPs: zprimes#() -> c_6(sieve#(nats(s(s(0()))))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/1} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons ,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. **** Step 3.b:3.b:3.b:1: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: zprimes#() -> c_6(sieve#(nats(s(s(0()))))) - Weak DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/1} - 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()))))) 2: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) 3: sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) **** Step 3.b:3.b:3.b:2: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) zprimes#() -> c_6(sieve#(nats(s(s(0()))))) - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/1} - 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:sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):1 2:W:sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):1 3:W:zprimes#() -> c_6(sieve#(nats(s(s(0()))))) -->_1 sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))):2 -->_1 sieve#(cons(0(),Y)) -> c_4(sieve#(Y)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: zprimes#() -> c_6(sieve#(nats(s(s(0()))))) 1: sieve#(cons(0(),Y)) -> c_4(sieve#(Y)) 2: sieve#(cons(s(N),Y)) -> c_5(sieve#(filter(Y,N,N))) **** Step 3.b:3.b:3.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: filter(cons(X,Y),0(),M) -> cons(0(),filter(Y,M,M)) filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M)) nats(N) -> cons(N,nats(s(N))) - Signature: {filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/2,s/1,c_1/1,c_2/1 ,c_3/1,c_4/1,c_5/1,c_6/1} - 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). MAYBE