MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) from(X) -> cons(X,from(s(X))) head(cons(X,Y)) -> X if(false(),X,Y) -> Y if(true(),X,Y) -> X primes() -> sieve(from(s(s(0())))) sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y))) tail(cons(X,Y)) -> Y - Signature: {filter/2,from/1,head/1,if/3,primes/0,sieve/1,tail/1} / {0/0,cons/2,divides/2,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {filter,from,head,if,primes,sieve ,tail} and constructors {0,cons,divides,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)) from#(X) -> c_2(from#(s(X))) head#(cons(X,Y)) -> c_3() if#(false(),X,Y) -> c_4() if#(true(),X,Y) -> c_5() primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) tail#(cons(X,Y)) -> c_8() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)) from#(X) -> c_2(from#(s(X))) head#(cons(X,Y)) -> c_3() if#(false(),X,Y) -> c_4() if#(true(),X,Y) -> c_5() primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) tail#(cons(X,Y)) -> c_8() - Weak TRS: filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) from(X) -> cons(X,from(s(X))) head(cons(X,Y)) -> X if(false(),X,Y) -> Y if(true(),X,Y) -> X primes() -> sieve(from(s(s(0())))) sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y))) tail(cons(X,Y)) -> Y - Signature: {filter/2,from/1,head/1,if/3,primes/0,sieve/1,tail/1,filter#/2,from#/1,head#/1,if#/3,primes#/0,sieve#/1 ,tail#/1} / {0/0,cons/2,divides/2,false/0,s/1,true/0,c_1/4,c_2/1,c_3/0,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,from#,head#,if#,primes#,sieve# ,tail#} and constructors {0,cons,divides,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) from(X) -> cons(X,from(s(X))) sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y))) filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)) from#(X) -> c_2(from#(s(X))) head#(cons(X,Y)) -> c_3() if#(false(),X,Y) -> c_4() if#(true(),X,Y) -> c_5() primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) tail#(cons(X,Y)) -> c_8() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)) from#(X) -> c_2(from#(s(X))) head#(cons(X,Y)) -> c_3() if#(false(),X,Y) -> c_4() if#(true(),X,Y) -> c_5() primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) tail#(cons(X,Y)) -> c_8() - Weak TRS: filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) from(X) -> cons(X,from(s(X))) sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y))) - Signature: {filter/2,from/1,head/1,if/3,primes/0,sieve/1,tail/1,filter#/2,from#/1,head#/1,if#/3,primes#/0,sieve#/1 ,tail#/1} / {0/0,cons/2,divides/2,false/0,s/1,true/0,c_1/4,c_2/1,c_3/0,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,from#,head#,if#,primes#,sieve# ,tail#} and constructors {0,cons,divides,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,4,5,8} by application of Pre({3,4,5,8}) = {}. Here rules are labelled as follows: 1: filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)) 2: from#(X) -> c_2(from#(s(X))) 3: head#(cons(X,Y)) -> c_3() 4: if#(false(),X,Y) -> c_4() 5: if#(true(),X,Y) -> c_5() 6: primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) 7: sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) 8: tail#(cons(X,Y)) -> c_8() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)) from#(X) -> c_2(from#(s(X))) primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) - Weak DPs: head#(cons(X,Y)) -> c_3() if#(false(),X,Y) -> c_4() if#(true(),X,Y) -> c_5() tail#(cons(X,Y)) -> c_8() - Weak TRS: filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) from(X) -> cons(X,from(s(X))) sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y))) - Signature: {filter/2,from/1,head/1,if/3,primes/0,sieve/1,tail/1,filter#/2,from#/1,head#/1,if#/3,primes#/0,sieve#/1 ,tail#/1} / {0/0,cons/2,divides/2,false/0,s/1,true/0,c_1/4,c_2/1,c_3/0,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,from#,head#,if#,primes#,sieve# ,tail#} and constructors {0,cons,divides,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)) -->_4 sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)):4 -->_3 filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y) ,filter(s(s(X)),Z) ,cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)):1 -->_2 filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y) ,filter(s(s(X)),Z) ,cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)):1 2:S:from#(X) -> c_2(from#(s(X))) -->_1 from#(X) -> c_2(from#(s(X))):2 3:S:primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) -->_1 sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)):4 -->_2 from#(X) -> c_2(from#(s(X))):2 4:S:sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) -->_2 sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)):4 -->_1 filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y) ,filter(s(s(X)),Z) ,cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)):1 5:W:head#(cons(X,Y)) -> c_3() 6:W:if#(false(),X,Y) -> c_4() 7:W:if#(true(),X,Y) -> c_5() 8:W:tail#(cons(X,Y)) -> c_8() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: tail#(cons(X,Y)) -> c_8() 7: if#(true(),X,Y) -> c_5() 6: if#(false(),X,Y) -> c_4() 5: head#(cons(X,Y)) -> c_3() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)) from#(X) -> c_2(from#(s(X))) primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) - Weak TRS: filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) from(X) -> cons(X,from(s(X))) sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y))) - Signature: {filter/2,from/1,head/1,if/3,primes/0,sieve/1,tail/1,filter#/2,from#/1,head#/1,if#/3,primes#/0,sieve#/1 ,tail#/1} / {0/0,cons/2,divides/2,false/0,s/1,true/0,c_1/4,c_2/1,c_3/0,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,from#,head#,if#,primes#,sieve# ,tail#} and constructors {0,cons,divides,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)) -->_4 sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)):4 -->_3 filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y) ,filter(s(s(X)),Z) ,cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)):1 -->_2 filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y) ,filter(s(s(X)),Z) ,cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)):1 2:S:from#(X) -> c_2(from#(s(X))) -->_1 from#(X) -> c_2(from#(s(X))):2 3:S:primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) -->_1 sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)):4 -->_2 from#(X) -> c_2(from#(s(X))):2 4:S:sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) -->_2 sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)):4 -->_1 filter#(s(s(X)),cons(Y,Z)) -> c_1(if#(divides(s(s(X)),Y) ,filter(s(s(X)),Z) ,cons(Y,filter(X,sieve(Y)))) ,filter#(s(s(X)),Z) ,filter#(X,sieve(Y)) ,sieve#(Y)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: filter#(s(s(X)),cons(Y,Z)) -> c_1(filter#(s(s(X)),Z),filter#(X,sieve(Y)),sieve#(Y)) * Step 6: NaturalMI MAYBE + Considered Problem: - Strict DPs: filter#(s(s(X)),cons(Y,Z)) -> c_1(filter#(s(s(X)),Z),filter#(X,sieve(Y)),sieve#(Y)) from#(X) -> c_2(from#(s(X))) primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) - Weak TRS: filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) from(X) -> cons(X,from(s(X))) sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y))) - Signature: {filter/2,from/1,head/1,if/3,primes/0,sieve/1,tail/1,filter#/2,from#/1,head#/1,if#/3,primes#/0,sieve#/1 ,tail#/1} / {0/0,cons/2,divides/2,false/0,s/1,true/0,c_1/3,c_2/1,c_3/0,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,from#,head#,if#,primes#,sieve# ,tail#} and constructors {0,cons,divides,false,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_1) = {1,2,3}, uargs(c_2) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {1,2} Following symbols are considered usable: {filter#,from#,head#,if#,primes#,sieve#,tail#} TcT has computed the following interpretation: p(0) = [1] p(cons) = [4] p(divides) = [0] p(false) = [1] p(filter) = [6] x2 + [2] p(from) = [1] x1 + [2] p(head) = [1] x1 + [4] p(if) = [4] x3 + [0] p(primes) = [1] p(s) = [2] p(sieve) = [3] x1 + [0] p(tail) = [2] x1 + [1] p(true) = [2] p(filter#) = [0] p(from#) = [0] p(head#) = [1] x1 + [1] p(if#) = [1] x1 + [1] x2 + [1] p(primes#) = [2] p(sieve#) = [0] p(tail#) = [1] p(c_1) = [8] x1 + [8] x2 + [4] x3 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [2] p(c_4) = [1] p(c_5) = [1] p(c_6) = [1] x1 + [8] x2 + [0] p(c_7) = [8] x1 + [1] x2 + [0] p(c_8) = [4] Following rules are strictly oriented: primes#() = [2] > [0] = c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) Following rules are (at-least) weakly oriented: filter#(s(s(X)),cons(Y,Z)) = [0] >= [0] = c_1(filter#(s(s(X)),Z),filter#(X,sieve(Y)),sieve#(Y)) from#(X) = [0] >= [0] = c_2(from#(s(X))) sieve#(cons(X,Y)) = [0] >= [0] = c_7(filter#(X,sieve(Y)),sieve#(Y)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: filter#(s(s(X)),cons(Y,Z)) -> c_1(filter#(s(s(X)),Z),filter#(X,sieve(Y)),sieve#(Y)) from#(X) -> c_2(from#(s(X))) sieve#(cons(X,Y)) -> c_7(filter#(X,sieve(Y)),sieve#(Y)) - Weak DPs: primes#() -> c_6(sieve#(from(s(s(0())))),from#(s(s(0())))) - Weak TRS: filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) from(X) -> cons(X,from(s(X))) sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y))) - Signature: {filter/2,from/1,head/1,if/3,primes/0,sieve/1,tail/1,filter#/2,from#/1,head#/1,if#/3,primes#/0,sieve#/1 ,tail#/1} / {0/0,cons/2,divides/2,false/0,s/1,true/0,c_1/3,c_2/1,c_3/0,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {filter#,from#,head#,if#,primes#,sieve# ,tail#} and constructors {0,cons,divides,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE