MAYBE Problem: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X Proof: DP Processor: DPs: primes#() -> s#(0()) primes#() -> s#(s(0())) primes#() -> from#(s(s(0()))) primes#() -> sieve#(from(s(s(0())))) from#(X) -> cons#(X,n__from(n__s(X))) tail#(cons(X,Y)) -> activate#(Y) if#(true(),X,Y) -> activate#(X) if#(false(),X,Y) -> activate#(Y) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) filter#(s(s(X)),cons(Y,Z)) -> if#(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y)))) sieve#(cons(X,Y)) -> activate#(Y) sieve#(cons(X,Y)) -> cons#(X,n__filter(X,n__sieve(activate(Y)))) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__sieve(X)) -> activate#(X) activate#(n__sieve(X)) -> sieve#(activate(X)) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X TDG Processor: DPs: primes#() -> s#(0()) primes#() -> s#(s(0())) primes#() -> from#(s(s(0()))) primes#() -> sieve#(from(s(s(0())))) from#(X) -> cons#(X,n__from(n__s(X))) tail#(cons(X,Y)) -> activate#(Y) if#(true(),X,Y) -> activate#(X) if#(false(),X,Y) -> activate#(Y) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) filter#(s(s(X)),cons(Y,Z)) -> if#(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y)))) sieve#(cons(X,Y)) -> activate#(Y) sieve#(cons(X,Y)) -> cons#(X,n__filter(X,n__sieve(activate(Y)))) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__sieve(X)) -> activate#(X) activate#(n__sieve(X)) -> sieve#(activate(X)) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X graph: filter#(s(s(X)),cons(Y,Z)) -> if#(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y)))) -> if#(false(),X,Y) -> activate#(Y) filter#(s(s(X)),cons(Y,Z)) -> if#(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y)))) -> if#(true(),X,Y) -> activate#(X) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__sieve(X)) -> sieve#(activate(X)) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__sieve(X)) -> activate#(X) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> activate#(X1) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__filter(X1,X2)) -> activate#(X1) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__filter(X1,X2)) -> activate#(X2) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> s#(activate(X)) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> activate#(X) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> from#(activate(X)) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__sieve(X)) -> sieve#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__sieve(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) if#(false(),X,Y) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> activate#(X1) if#(false(),X,Y) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X1) if#(false(),X,Y) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X2) if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__from(X)) -> from#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__from(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__sieve(X)) -> sieve#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__sieve(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) if#(true(),X,Y) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) if#(true(),X,Y) -> activate#(X) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) if#(true(),X,Y) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X1) if#(true(),X,Y) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X2) if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> activate#(X) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__sieve(X)) -> sieve#(activate(X)) -> sieve#(cons(X,Y)) -> cons#(X,n__filter(X,n__sieve(activate(Y)))) activate#(n__sieve(X)) -> sieve#(activate(X)) -> sieve#(cons(X,Y)) -> activate#(Y) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) -> filter#(s(s(X)),cons(Y,Z)) -> if#(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y)))) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) -> filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__from(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__from(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__from(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__from(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__from(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) -> from#(X) -> cons#(X,n__from(n__s(X))) activate#(n__s(X)) -> activate#(X) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__s(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__sieve(X)) -> sieve#(activate(X)) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__sieve(X)) -> activate#(X) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> activate#(X1) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X1) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X2) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__from(X)) -> from#(activate(X)) tail#(cons(X,Y)) -> activate#(Y) -> activate#(n__from(X)) -> activate#(X) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__sieve(X)) -> sieve#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__sieve(X)) -> activate#(X) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> activate#(X1) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X1) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X2) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__from(X)) -> from#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__from(X)) -> activate#(X) primes#() -> sieve#(from(s(s(0())))) -> sieve#(cons(X,Y)) -> cons#(X,n__filter(X,n__sieve(activate(Y)))) primes#() -> sieve#(from(s(s(0())))) -> sieve#(cons(X,Y)) -> activate#(Y) primes#() -> from#(s(s(0()))) -> from#(X) -> cons#(X,n__from(n__s(X))) SCC Processor: #sccs: 1 #rules: 13 #arcs: 131/529 DPs: filter#(s(s(X)),cons(Y,Z)) -> if#(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons (Y,n__filter(X,n__sieve(Y)))) if#(true(),X,Y) -> activate#(X) activate#(n__from(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__sieve(X)) -> activate#(X) activate#(n__sieve(X)) -> sieve#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) if#(false(),X,Y) -> activate#(Y) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X EDG Processor: DPs: filter#(s(s(X)),cons(Y,Z)) -> if#(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons (Y,n__filter(X,n__sieve(Y)))) if#(true(),X,Y) -> activate#(X) activate#(n__from(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__sieve(X)) -> activate#(X) activate#(n__sieve(X)) -> sieve#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) if#(false(),X,Y) -> activate#(Y) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons (Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X graph: filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__from(X)) -> activate#(X) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__s(X)) -> activate#(X) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__filter(X1,X2)) -> activate#(X2) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__filter(X1,X2)) -> activate#(X1) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__cons(X1,X2)) -> activate#(X1) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__sieve(X)) -> activate#(X) filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) -> activate#(n__sieve(X)) -> sieve#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__from(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X2) if#(false(),X,Y) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X1) if#(false(),X,Y) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> activate#(X1) if#(false(),X,Y) -> activate#(Y) -> activate#(n__sieve(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__sieve(X)) -> sieve#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X2) if#(true(),X,Y) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X1) if#(true(),X,Y) -> activate#(X) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) if#(true(),X,Y) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) if#(true(),X,Y) -> activate#(X) -> activate#(n__sieve(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__sieve(X)) -> activate#(X) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__sieve(X)) -> sieve#(activate(X)) -> sieve#(cons(X,Y)) -> activate#(Y) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) -> filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) -> filter#(s(s(X)),cons(Y,Z)) -> if#(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons (Y,n__filter(X,n__sieve(Y)))) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X2) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> activate#(X1) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__from(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__from(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__from(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__from(X)) -> activate#(X) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__sieve(X)) -> sieve#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__s(X)) -> activate#(X) -> activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__sieve(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__sieve(X)) -> sieve#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__from(X)) -> activate#(X) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X2) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> activate#(X1) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> activate#(X1) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__sieve(X)) -> activate#(X) sieve#(cons(X,Y)) -> activate#(Y) -> activate#(n__sieve(X)) -> sieve#(activate(X)) SCC Processor: #sccs: 1 #rules: 10 #arcs: 83/169 DPs: filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) activate#(n__sieve(X)) -> sieve#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) activate#(n__sieve(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons (Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [filter#](x0, x1) = x0 + 4x1 + 0, [activate#](x0) = 4x0, [sieve#](x0) = 4x0, [n__cons](x0, x1) = x0 + x1, [n__sieve](x0) = x0 + 0, [n__filter](x0, x1) = x0 + x1 + 0, [divides](x0, x1) = x1, [filter](x0, x1) = x0 + x1 + 0, [false] = 6, [if](x0, x1, x2) = x0 + x1 + x2, [true] = 1, [activate](x0) = x0, [tail](x0) = 7x0 + 12, [head](x0) = 4x0 + 8, [cons](x0, x1) = x0 + x1, [n__from](x0) = 1x0, [n__s](x0) = x0, [sieve](x0) = x0 + 0, [from](x0) = 1x0, [s](x0) = x0, [0] = 1, [primes] = 9 orientation: filter#(s(s(X)),cons(Y,Z)) = X + 4Y + 4Z + 0 >= 4Z = activate#(Z) activate#(n__sieve(X)) = 4X + 4 >= 4X = sieve#(activate(X)) sieve#(cons(X,Y)) = 4X + 4Y >= 4Y = activate#(Y) activate#(n__sieve(X)) = 4X + 4 >= 4X = activate#(X) activate#(n__cons(X1,X2)) = 4X1 + 4X2 >= 4X1 = activate#(X1) activate#(n__filter(X1,X2)) = 4X1 + 4X2 + 4 >= X1 + 4X2 + 0 = filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) = 4X1 + 4X2 + 4 >= 4X1 = activate#(X1) activate#(n__filter(X1,X2)) = 4X1 + 4X2 + 4 >= 4X2 = activate#(X2) activate#(n__s(X)) = 4X >= 4X = activate#(X) activate#(n__from(X)) = 5X >= 4X = activate#(X) primes() = 9 >= 2 = sieve(from(s(s(0())))) from(X) = 1X >= 1X = cons(X,n__from(n__s(X))) head(cons(X,Y)) = 4X + 4Y + 8 >= X = X tail(cons(X,Y)) = 7X + 7Y + 12 >= Y = activate(Y) if(true(),X,Y) = X + Y + 1 >= X = activate(X) if(false(),X,Y) = X + Y + 6 >= Y = activate(Y) filter(s(s(X)),cons(Y,Z)) = X + Y + Z + 0 >= X + Y + Z + 0 = if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y, n__filter (X, n__sieve ( Y)))) sieve(cons(X,Y)) = X + Y + 0 >= X + Y + 0 = cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) = 1X >= 1X = n__from(X) s(X) = X >= X = n__s(X) filter(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__filter(X1,X2) cons(X1,X2) = X1 + X2 >= X1 + X2 = n__cons(X1,X2) sieve(X) = X + 0 >= X + 0 = n__sieve(X) activate(n__from(X)) = 1X >= 1X = from(activate(X)) activate(n__s(X)) = X >= X = s(activate(X)) activate(n__filter(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(activate(X1),X2) activate(n__sieve(X)) = X + 0 >= X + 0 = sieve(activate(X)) activate(X) = X >= X = X problem: DPs: filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) activate#(n__sieve(X)) -> sieve#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) activate#(n__sieve(X)) -> activate#(X) activate#(n__cons(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons ( Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [filter#](x0, x1) = x0 + x1, [activate#](x0) = x0, [sieve#](x0) = x0 + 0, [n__cons](x0, x1) = 1x0 + x1 + 0, [n__sieve](x0) = x0 + 0, [n__filter](x0, x1) = x0 + x1, [divides](x0, x1) = x1 + 0, [filter](x0, x1) = x0 + x1, [false] = 4, [if](x0, x1, x2) = x0 + x1 + x2 + 0, [true] = 1, [activate](x0) = x0, [tail](x0) = x0 + 4, [head](x0) = 6x0 + 1, [cons](x0, x1) = 1x0 + x1 + 0, [n__from](x0) = 1x0 + 1, [n__s](x0) = x0 + 0, [sieve](x0) = x0 + 0, [from](x0) = 1x0 + 1, [s](x0) = x0 + 0, [0] = 3, [primes] = 4 orientation: filter#(s(s(X)),cons(Y,Z)) = X + 1Y + Z + 0 >= Z = activate#(Z) activate#(n__sieve(X)) = X + 0 >= X + 0 = sieve#(activate(X)) sieve#(cons(X,Y)) = 1X + Y + 0 >= Y = activate#(Y) activate#(n__sieve(X)) = X + 0 >= X = activate#(X) activate#(n__cons(X1,X2)) = 1X1 + X2 + 0 >= X1 = activate#(X1) activate#(n__filter(X1,X2)) = X1 + X2 >= X1 + X2 = filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) = X1 + X2 >= X1 = activate#(X1) activate#(n__filter(X1,X2)) = X1 + X2 >= X2 = activate#(X2) activate#(n__s(X)) = X + 0 >= X = activate#(X) primes() = 4 >= 4 = sieve(from(s(s(0())))) from(X) = 1X + 1 >= 1X + 1 = cons(X,n__from(n__s(X))) head(cons(X,Y)) = 7X + 6Y + 6 >= X = X tail(cons(X,Y)) = 1X + Y + 4 >= Y = activate(Y) if(true(),X,Y) = X + Y + 1 >= X = activate(X) if(false(),X,Y) = X + Y + 4 >= Y = activate(Y) filter(s(s(X)),cons(Y,Z)) = X + 1Y + Z + 0 >= X + 1Y + Z + 0 = if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y, n__filter (X, n__sieve ( Y)))) sieve(cons(X,Y)) = 1X + Y + 0 >= 1X + Y + 0 = cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) = 1X + 1 >= 1X + 1 = n__from(X) s(X) = X + 0 >= X + 0 = n__s(X) filter(X1,X2) = X1 + X2 >= X1 + X2 = n__filter(X1,X2) cons(X1,X2) = 1X1 + X2 + 0 >= 1X1 + X2 + 0 = n__cons(X1,X2) sieve(X) = X + 0 >= X + 0 = n__sieve(X) activate(n__from(X)) = 1X + 1 >= 1X + 1 = from(activate(X)) activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__filter(X1,X2)) = X1 + X2 >= X1 + X2 = filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) = 1X1 + X2 + 0 >= 1X1 + X2 + 0 = cons(activate(X1),X2) activate(n__sieve(X)) = X + 0 >= X + 0 = sieve(activate(X)) activate(X) = X >= X = X problem: DPs: filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) activate#(n__sieve(X)) -> sieve#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) activate#(n__sieve(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X1) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)), n__cons(Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [filter#](x0, x1) = x0 + x1 + 1, [activate#](x0) = x0 + 0, [sieve#](x0) = x0 + 0, [n__cons](x0, x1) = 4x0 + x1, [n__sieve](x0) = x0 + 1, [n__filter](x0, x1) = 2x0 + x1 + 1, [divides](x0, x1) = x0, [filter](x0, x1) = 2x0 + x1 + 1, [false] = 0, [if](x0, x1, x2) = x0 + x1 + x2, [true] = 0, [activate](x0) = x0, [tail](x0) = x0 + 9, [head](x0) = 3x0 + 4, [cons](x0, x1) = 4x0 + x1, [n__from](x0) = 4x0, [n__s](x0) = x0, [sieve](x0) = x0 + 1, [from](x0) = 4x0, [s](x0) = x0, [0] = 0, [primes] = 5 orientation: filter#(s(s(X)),cons(Y,Z)) = X + 4Y + Z + 1 >= Z + 0 = activate#(Z) activate#(n__sieve(X)) = X + 1 >= X + 0 = sieve#(activate(X)) sieve#(cons(X,Y)) = 4X + Y + 0 >= Y + 0 = activate#(Y) activate#(n__sieve(X)) = X + 1 >= X + 0 = activate#(X) activate#(n__filter(X1,X2)) = 2X1 + X2 + 1 >= X1 + X2 + 1 = filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) = 2X1 + X2 + 1 >= X1 + 0 = activate#(X1) activate#(n__filter(X1,X2)) = 2X1 + X2 + 1 >= X2 + 0 = activate#(X2) activate#(n__s(X)) = X + 0 >= X + 0 = activate#(X) primes() = 5 >= 4 = sieve(from(s(s(0())))) from(X) = 4X >= 4X = cons(X,n__from(n__s(X))) head(cons(X,Y)) = 7X + 3Y + 4 >= X = X tail(cons(X,Y)) = 4X + Y + 9 >= Y = activate(Y) if(true(),X,Y) = X + Y + 0 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) filter(s(s(X)),cons(Y,Z)) = 2X + 4Y + Z + 1 >= 2X + 4Y + Z + 1 = if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y, n__filter (X, n__sieve ( Y)))) sieve(cons(X,Y)) = 4X + Y + 1 >= 4X + Y + 1 = cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) = 4X >= 4X = n__from(X) s(X) = X >= X = n__s(X) filter(X1,X2) = 2X1 + X2 + 1 >= 2X1 + X2 + 1 = n__filter(X1,X2) cons(X1,X2) = 4X1 + X2 >= 4X1 + X2 = n__cons(X1,X2) sieve(X) = X + 1 >= X + 1 = n__sieve(X) activate(n__from(X)) = 4X >= 4X = from(activate(X)) activate(n__s(X)) = X >= X = s(activate(X)) activate(n__filter(X1,X2)) = 2X1 + X2 + 1 >= 2X1 + X2 + 1 = filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) = 4X1 + X2 >= 4X1 + X2 = cons(activate(X1),X2) activate(n__sieve(X)) = X + 1 >= X + 1 = sieve(activate(X)) activate(X) = X >= X = X problem: DPs: filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) activate#(n__sieve(X)) -> sieve#(activate(X)) sieve#(cons(X,Y)) -> activate#(Y) activate#(n__sieve(X)) -> activate#(X) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)), n__cons(Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [filter#](x0, x1) = 4x1, [activate#](x0) = 4x0, [sieve#](x0) = 4x0, [n__cons](x0, x1) = 1x0 + x1 + 0, [n__sieve](x0) = 1x0, [n__filter](x0, x1) = x0 + x1, [divides](x0, x1) = x0 + x1 + 0, [filter](x0, x1) = x0 + x1, [false] = 0, [if](x0, x1, x2) = x0 + x1 + x2 + 0, [true] = 4, [activate](x0) = x0, [tail](x0) = 3x0 + 1, [head](x0) = 1x0 + 3, [cons](x0, x1) = 1x0 + x1 + 0, [n__from](x0) = 4x0 + 4, [n__s](x0) = x0 + 0, [sieve](x0) = 1x0, [from](x0) = 4x0 + 4, [s](x0) = x0 + 0, [0] = 2, [primes] = 10 orientation: filter#(s(s(X)),cons(Y,Z)) = 5Y + 4Z + 4 >= 4Z = activate#(Z) activate#(n__sieve(X)) = 5X >= 4X = sieve#(activate(X)) sieve#(cons(X,Y)) = 5X + 4Y + 4 >= 4Y = activate#(Y) activate#(n__sieve(X)) = 5X >= 4X = activate#(X) activate#(n__filter(X1,X2)) = 4X1 + 4X2 >= 4X2 = filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) = 4X1 + 4X2 >= 4X2 = activate#(X2) activate#(n__s(X)) = 4X + 4 >= 4X = activate#(X) primes() = 10 >= 7 = sieve(from(s(s(0())))) from(X) = 4X + 4 >= 4X + 4 = cons(X,n__from(n__s(X))) head(cons(X,Y)) = 2X + 1Y + 3 >= X = X tail(cons(X,Y)) = 4X + 3Y + 3 >= Y = activate(Y) if(true(),X,Y) = X + Y + 4 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) filter(s(s(X)),cons(Y,Z)) = X + 1Y + Z + 0 >= X + 1Y + Z + 0 = if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y, n__filter (X, n__sieve ( Y)))) sieve(cons(X,Y)) = 2X + 1Y + 1 >= 1X + 1Y + 0 = cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) = 4X + 4 >= 4X + 4 = n__from(X) s(X) = X + 0 >= X + 0 = n__s(X) filter(X1,X2) = X1 + X2 >= X1 + X2 = n__filter(X1,X2) cons(X1,X2) = 1X1 + X2 + 0 >= 1X1 + X2 + 0 = n__cons(X1,X2) sieve(X) = 1X >= 1X = n__sieve(X) activate(n__from(X)) = 4X + 4 >= 4X + 4 = from(activate(X)) activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__filter(X1,X2)) = X1 + X2 >= X1 + X2 = filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) = 1X1 + X2 + 0 >= 1X1 + X2 + 0 = cons(activate(X1),X2) activate(n__sieve(X)) = 1X >= 1X = sieve(activate(X)) activate(X) = X >= X = X problem: DPs: filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) sieve#(cons(X,Y)) -> activate#(Y) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)), n__cons(Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X SCC Processor: #sccs: 1 #rules: 4 #arcs: 66/25 DPs: filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) activate#(n__filter(X1,X2)) -> filter#(activate(X1),activate(X2)) activate#(n__filter(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) TRS: primes() -> sieve(from(s(s(0())))) from(X) -> cons(X,n__from(n__s(X))) head(cons(X,Y)) -> X tail(cons(X,Y)) -> activate(Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)), n__cons(Y,n__filter(X,n__sieve(Y)))) sieve(cons(X,Y)) -> cons(X,n__filter(X,n__sieve(activate(Y)))) from(X) -> n__from(X) s(X) -> n__s(X) filter(X1,X2) -> n__filter(X1,X2) cons(X1,X2) -> n__cons(X1,X2) sieve(X) -> n__sieve(X) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__filter(X1,X2)) -> filter(activate(X1),activate(X2)) activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__sieve(X)) -> sieve(activate(X)) activate(X) -> X Open