MAYBE Problem: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: DP Processor: DPs: active#(primes()) -> s#(0()) active#(primes()) -> s#(s(0())) active#(primes()) -> from#(s(s(0()))) active#(primes()) -> sieve#(from(s(s(0())))) active#(from(X)) -> s#(X) active#(from(X)) -> from#(s(X)) active#(from(X)) -> cons#(X,from(s(X))) active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(sieve(cons(X,Y))) -> sieve#(Y) active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(sieve(X)) -> active#(X) active#(sieve(X)) -> sieve#(active(X)) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(head(X)) -> active#(X) active#(head(X)) -> head#(active(X)) active#(tail(X)) -> active#(X) active#(tail(X)) -> tail#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(filter(X1,X2)) -> active#(X1) active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(filter(X1,X2)) -> active#(X2) active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(divides(X1,X2)) -> active#(X1) active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(divides(X1,X2)) -> active#(X2) active#(divides(X1,X2)) -> divides#(X1,active(X2)) sieve#(mark(X)) -> sieve#(X) from#(mark(X)) -> from#(X) s#(mark(X)) -> s#(X) cons#(mark(X1),X2) -> cons#(X1,X2) head#(mark(X)) -> head#(X) tail#(mark(X)) -> tail#(X) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) filter#(mark(X1),X2) -> filter#(X1,X2) filter#(X1,mark(X2)) -> filter#(X1,X2) divides#(mark(X1),X2) -> divides#(X1,X2) divides#(X1,mark(X2)) -> divides#(X1,X2) proper#(sieve(X)) -> proper#(X) proper#(sieve(X)) -> sieve#(proper(X)) proper#(from(X)) -> proper#(X) proper#(from(X)) -> from#(proper(X)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(head(X)) -> proper#(X) proper#(head(X)) -> head#(proper(X)) proper#(tail(X)) -> proper#(X) proper#(tail(X)) -> tail#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(filter(X1,X2)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X1) proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(divides(X1,X2)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X1) proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) sieve#(ok(X)) -> sieve#(X) from#(ok(X)) -> from#(X) s#(ok(X)) -> s#(X) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) head#(ok(X)) -> head#(X) tail#(ok(X)) -> tail#(X) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) filter#(ok(X1),ok(X2)) -> filter#(X1,X2) divides#(ok(X1),ok(X2)) -> divides#(X1,X2) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) TDG Processor: DPs: active#(primes()) -> s#(0()) active#(primes()) -> s#(s(0())) active#(primes()) -> from#(s(s(0()))) active#(primes()) -> sieve#(from(s(s(0())))) active#(from(X)) -> s#(X) active#(from(X)) -> from#(s(X)) active#(from(X)) -> cons#(X,from(s(X))) active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(sieve(cons(X,Y))) -> sieve#(Y) active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(sieve(X)) -> active#(X) active#(sieve(X)) -> sieve#(active(X)) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(head(X)) -> active#(X) active#(head(X)) -> head#(active(X)) active#(tail(X)) -> active#(X) active#(tail(X)) -> tail#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(filter(X1,X2)) -> active#(X1) active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(filter(X1,X2)) -> active#(X2) active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(divides(X1,X2)) -> active#(X1) active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(divides(X1,X2)) -> active#(X2) active#(divides(X1,X2)) -> divides#(X1,active(X2)) sieve#(mark(X)) -> sieve#(X) from#(mark(X)) -> from#(X) s#(mark(X)) -> s#(X) cons#(mark(X1),X2) -> cons#(X1,X2) head#(mark(X)) -> head#(X) tail#(mark(X)) -> tail#(X) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) filter#(mark(X1),X2) -> filter#(X1,X2) filter#(X1,mark(X2)) -> filter#(X1,X2) divides#(mark(X1),X2) -> divides#(X1,X2) divides#(X1,mark(X2)) -> divides#(X1,X2) proper#(sieve(X)) -> proper#(X) proper#(sieve(X)) -> sieve#(proper(X)) proper#(from(X)) -> proper#(X) proper#(from(X)) -> from#(proper(X)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(head(X)) -> proper#(X) proper#(head(X)) -> head#(proper(X)) proper#(tail(X)) -> proper#(X) proper#(tail(X)) -> tail#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(filter(X1,X2)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X1) proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(divides(X1,X2)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X1) proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) sieve#(ok(X)) -> sieve#(X) from#(ok(X)) -> from#(X) s#(ok(X)) -> s#(X) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) head#(ok(X)) -> head#(X) tail#(ok(X)) -> tail#(X) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) filter#(ok(X1),ok(X2)) -> filter#(X1,X2) divides#(ok(X1),ok(X2)) -> divides#(X1,X2) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) graph: top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X)) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X) top#(ok(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) top#(ok(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X2) top#(ok(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) top#(ok(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X2) top#(ok(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) top#(ok(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(tail(X)) -> tail#(active(X)) top#(ok(X)) -> active#(X) -> active#(tail(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(head(X)) -> head#(active(X)) top#(ok(X)) -> active#(X) -> active#(head(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(from(X)) -> from#(active(X)) top#(ok(X)) -> active#(X) -> active#(from(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(sieve(X)) -> sieve#(active(X)) top#(ok(X)) -> active#(X) -> active#(sieve(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) top#(ok(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) top#(ok(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> sieve#(Y) top#(ok(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) top#(ok(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) top#(ok(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) top#(ok(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) top#(ok(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) top#(ok(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) top#(ok(X)) -> active#(X) -> active#(from(X)) -> cons#(X,from(s(X))) top#(ok(X)) -> active#(X) -> active#(from(X)) -> from#(s(X)) top#(ok(X)) -> active#(X) -> active#(from(X)) -> s#(X) top#(ok(X)) -> active#(X) -> active#(primes()) -> sieve#(from(s(s(0())))) top#(ok(X)) -> active#(X) -> active#(primes()) -> from#(s(s(0()))) top#(ok(X)) -> active#(X) -> active#(primes()) -> s#(s(0())) top#(ok(X)) -> active#(X) -> active#(primes()) -> s#(0()) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> top#(proper(X)) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) top#(mark(X)) -> proper#(X) -> proper#(tail(X)) -> tail#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(head(X)) -> head#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(head(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(from(X)) -> from#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(from(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(sieve(X)) -> sieve#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(sieve(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(tail(X)) -> tail#(proper(X)) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(tail(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(head(X)) -> head#(proper(X)) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(head(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(from(X)) -> from#(proper(X)) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(from(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(divides(X1,X2)) -> proper#(X2) -> proper#(sieve(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(tail(X)) -> tail#(proper(X)) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(tail(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(head(X)) -> head#(proper(X)) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(head(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(from(X)) -> from#(proper(X)) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(from(X)) -> proper#(X) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(divides(X1,X2)) -> proper#(X1) -> proper#(sieve(X)) -> proper#(X) proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) -> divides#(ok(X1),ok(X2)) -> divides#(X1,X2) proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) -> divides#(X1,mark(X2)) -> divides#(X1,X2) proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) -> divides#(mark(X1),X2) -> divides#(X1,X2) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(tail(X)) -> tail#(proper(X)) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(tail(X)) -> proper#(X) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(head(X)) -> head#(proper(X)) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(head(X)) -> proper#(X) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(from(X)) -> from#(proper(X)) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(from(X)) -> proper#(X) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(filter(X1,X2)) -> proper#(X2) -> proper#(sieve(X)) -> proper#(X) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(tail(X)) -> tail#(proper(X)) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(tail(X)) -> proper#(X) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(head(X)) -> head#(proper(X)) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(head(X)) -> proper#(X) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(from(X)) -> from#(proper(X)) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(from(X)) -> proper#(X) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(filter(X1,X2)) -> proper#(X1) -> proper#(sieve(X)) -> proper#(X) proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) -> filter#(ok(X1),ok(X2)) -> filter#(X1,X2) proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) -> filter#(X1,mark(X2)) -> filter#(X1,X2) proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) -> filter#(mark(X1),X2) -> filter#(X1,X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(tail(X)) -> tail#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(tail(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(head(X)) -> head#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(head(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(from(X)) -> from#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(from(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X3) -> proper#(sieve(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(tail(X)) -> tail#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(tail(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(head(X)) -> head#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(head(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(from(X)) -> from#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(from(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X2) -> proper#(sieve(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(tail(X)) -> tail#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(tail(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(head(X)) -> head#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(head(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(from(X)) -> from#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(from(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(if(X1,X2,X3)) -> proper#(X1) -> proper#(sieve(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) proper#(tail(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(tail(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(tail(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(tail(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(tail(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(tail(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(tail(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(tail(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(tail(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(tail(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(tail(X)) -> proper#(X) -> proper#(tail(X)) -> tail#(proper(X)) proper#(tail(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X) proper#(tail(X)) -> proper#(X) -> proper#(head(X)) -> head#(proper(X)) proper#(tail(X)) -> proper#(X) -> proper#(head(X)) -> proper#(X) proper#(tail(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(tail(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(tail(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(tail(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(tail(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(tail(X)) -> proper#(X) -> proper#(from(X)) -> from#(proper(X)) proper#(tail(X)) -> proper#(X) -> proper#(from(X)) -> proper#(X) proper#(tail(X)) -> proper#(X) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(tail(X)) -> proper#(X) -> proper#(sieve(X)) -> proper#(X) proper#(tail(X)) -> tail#(proper(X)) -> tail#(ok(X)) -> tail#(X) proper#(tail(X)) -> tail#(proper(X)) -> tail#(mark(X)) -> tail#(X) proper#(head(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(head(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(head(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(head(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(head(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(head(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(head(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(head(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(head(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(head(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(head(X)) -> proper#(X) -> proper#(tail(X)) -> tail#(proper(X)) proper#(head(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X) proper#(head(X)) -> proper#(X) -> proper#(head(X)) -> head#(proper(X)) proper#(head(X)) -> proper#(X) -> proper#(head(X)) -> proper#(X) proper#(head(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(head(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(head(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(head(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(head(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(head(X)) -> proper#(X) -> proper#(from(X)) -> from#(proper(X)) proper#(head(X)) -> proper#(X) -> proper#(from(X)) -> proper#(X) proper#(head(X)) -> proper#(X) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(head(X)) -> proper#(X) -> proper#(sieve(X)) -> proper#(X) proper#(head(X)) -> head#(proper(X)) -> head#(ok(X)) -> head#(X) proper#(head(X)) -> head#(proper(X)) -> head#(mark(X)) -> head#(X) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(tail(X)) -> tail#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(tail(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(head(X)) -> head#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(head(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(from(X)) -> from#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(from(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) -> proper#(sieve(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(tail(X)) -> tail#(proper(X)) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(tail(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(head(X)) -> head#(proper(X)) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(head(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(from(X)) -> from#(proper(X)) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(from(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(cons(X1,X2)) -> proper#(X1) -> proper#(sieve(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) -> cons#(ok(X1),ok(X2)) -> cons#(X1,X2) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) -> cons#(mark(X1),X2) -> cons#(X1,X2) proper#(sieve(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(sieve(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(sieve(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(sieve(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(sieve(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(sieve(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(sieve(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(sieve(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(sieve(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(sieve(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(sieve(X)) -> proper#(X) -> proper#(tail(X)) -> tail#(proper(X)) proper#(sieve(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X) proper#(sieve(X)) -> proper#(X) -> proper#(head(X)) -> head#(proper(X)) proper#(sieve(X)) -> proper#(X) -> proper#(head(X)) -> proper#(X) proper#(sieve(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(sieve(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(sieve(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(sieve(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(sieve(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(sieve(X)) -> proper#(X) -> proper#(from(X)) -> from#(proper(X)) proper#(sieve(X)) -> proper#(X) -> proper#(from(X)) -> proper#(X) proper#(sieve(X)) -> proper#(X) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(sieve(X)) -> proper#(X) -> proper#(sieve(X)) -> proper#(X) proper#(sieve(X)) -> sieve#(proper(X)) -> sieve#(ok(X)) -> sieve#(X) proper#(sieve(X)) -> sieve#(proper(X)) -> sieve#(mark(X)) -> sieve#(X) proper#(from(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(from(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(from(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(from(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(from(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(from(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(from(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(from(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(from(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(from(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(from(X)) -> proper#(X) -> proper#(tail(X)) -> tail#(proper(X)) proper#(from(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X) proper#(from(X)) -> proper#(X) -> proper#(head(X)) -> head#(proper(X)) proper#(from(X)) -> proper#(X) -> proper#(head(X)) -> proper#(X) proper#(from(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(from(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(from(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(from(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(from(X)) -> proper#(X) -> proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) -> proper#(from(X)) -> proper#(X) proper#(from(X)) -> proper#(X) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(from(X)) -> proper#(X) -> proper#(sieve(X)) -> proper#(X) proper#(from(X)) -> from#(proper(X)) -> from#(ok(X)) -> from#(X) proper#(from(X)) -> from#(proper(X)) -> from#(mark(X)) -> from#(X) proper#(s(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> divides#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(divides(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> filter#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(filter(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3)) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(if(X1,X2,X3)) -> proper#(X3) proper#(s(X)) -> proper#(X) -> proper#(tail(X)) -> tail#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(head(X)) -> head#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(head(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(from(X)) -> from#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(sieve(X)) -> sieve#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(sieve(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X) proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X) tail#(ok(X)) -> tail#(X) -> tail#(ok(X)) -> tail#(X) tail#(ok(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X) tail#(mark(X)) -> tail#(X) -> tail#(ok(X)) -> tail#(X) tail#(mark(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X) head#(ok(X)) -> head#(X) -> head#(ok(X)) -> head#(X) head#(ok(X)) -> head#(X) -> head#(mark(X)) -> head#(X) head#(mark(X)) -> head#(X) -> head#(ok(X)) -> head#(X) head#(mark(X)) -> head#(X) -> head#(mark(X)) -> head#(X) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) divides#(ok(X1),ok(X2)) -> divides#(X1,X2) -> divides#(ok(X1),ok(X2)) -> divides#(X1,X2) divides#(ok(X1),ok(X2)) -> divides#(X1,X2) -> divides#(X1,mark(X2)) -> divides#(X1,X2) divides#(ok(X1),ok(X2)) -> divides#(X1,X2) -> divides#(mark(X1),X2) -> divides#(X1,X2) divides#(mark(X1),X2) -> divides#(X1,X2) -> divides#(ok(X1),ok(X2)) -> divides#(X1,X2) divides#(mark(X1),X2) -> divides#(X1,X2) -> divides#(X1,mark(X2)) -> divides#(X1,X2) divides#(mark(X1),X2) -> divides#(X1,X2) -> divides#(mark(X1),X2) -> divides#(X1,X2) divides#(X1,mark(X2)) -> divides#(X1,X2) -> divides#(ok(X1),ok(X2)) -> divides#(X1,X2) divides#(X1,mark(X2)) -> divides#(X1,X2) -> divides#(X1,mark(X2)) -> divides#(X1,X2) divides#(X1,mark(X2)) -> divides#(X1,X2) -> divides#(mark(X1),X2) -> divides#(X1,X2) filter#(ok(X1),ok(X2)) -> filter#(X1,X2) -> filter#(ok(X1),ok(X2)) -> filter#(X1,X2) filter#(ok(X1),ok(X2)) -> filter#(X1,X2) -> filter#(X1,mark(X2)) -> filter#(X1,X2) filter#(ok(X1),ok(X2)) -> filter#(X1,X2) -> filter#(mark(X1),X2) -> filter#(X1,X2) filter#(mark(X1),X2) -> filter#(X1,X2) -> filter#(ok(X1),ok(X2)) -> filter#(X1,X2) filter#(mark(X1),X2) -> filter#(X1,X2) -> filter#(X1,mark(X2)) -> filter#(X1,X2) filter#(mark(X1),X2) -> filter#(X1,X2) -> filter#(mark(X1),X2) -> filter#(X1,X2) filter#(X1,mark(X2)) -> filter#(X1,X2) -> filter#(ok(X1),ok(X2)) -> filter#(X1,X2) filter#(X1,mark(X2)) -> filter#(X1,X2) -> filter#(X1,mark(X2)) -> filter#(X1,X2) filter#(X1,mark(X2)) -> filter#(X1,X2) -> filter#(mark(X1),X2) -> filter#(X1,X2) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) -> cons#(ok(X1),ok(X2)) -> cons#(X1,X2) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(ok(X1),ok(X2)) -> cons#(X1,X2) cons#(mark(X1),X2) -> cons#(X1,X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) sieve#(ok(X)) -> sieve#(X) -> sieve#(ok(X)) -> sieve#(X) sieve#(ok(X)) -> sieve#(X) -> sieve#(mark(X)) -> sieve#(X) sieve#(mark(X)) -> sieve#(X) -> sieve#(ok(X)) -> sieve#(X) sieve#(mark(X)) -> sieve#(X) -> sieve#(mark(X)) -> sieve#(X) from#(ok(X)) -> from#(X) -> from#(ok(X)) -> from#(X) from#(ok(X)) -> from#(X) -> from#(mark(X)) -> from#(X) from#(mark(X)) -> from#(X) -> from#(ok(X)) -> from#(X) from#(mark(X)) -> from#(X) -> from#(mark(X)) -> from#(X) s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X) active#(divides(X1,X2)) -> divides#(active(X1),X2) -> divides#(ok(X1),ok(X2)) -> divides#(X1,X2) active#(divides(X1,X2)) -> divides#(active(X1),X2) -> divides#(X1,mark(X2)) -> divides#(X1,X2) active#(divides(X1,X2)) -> divides#(active(X1),X2) -> divides#(mark(X1),X2) -> divides#(X1,X2) active#(divides(X1,X2)) -> divides#(X1,active(X2)) -> divides#(ok(X1),ok(X2)) -> divides#(X1,X2) active#(divides(X1,X2)) -> divides#(X1,active(X2)) -> divides#(X1,mark(X2)) -> divides#(X1,X2) active#(divides(X1,X2)) -> divides#(X1,active(X2)) -> divides#(mark(X1),X2) -> divides#(X1,X2) active#(divides(X1,X2)) -> active#(X2) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(divides(X1,X2)) -> active#(X2) -> active#(divides(X1,X2)) -> active#(X2) active#(divides(X1,X2)) -> active#(X2) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(divides(X1,X2)) -> active#(X2) -> active#(divides(X1,X2)) -> active#(X1) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(X1,X2)) -> active#(X2) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(X1,X2)) -> active#(X1) active#(divides(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(divides(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> active#(X1) active#(divides(X1,X2)) -> active#(X2) -> active#(tail(X)) -> tail#(active(X)) active#(divides(X1,X2)) -> active#(X2) -> active#(tail(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X2) -> active#(head(X)) -> head#(active(X)) active#(divides(X1,X2)) -> active#(X2) -> active#(head(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X2) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(divides(X1,X2)) -> active#(X2) -> active#(cons(X1,X2)) -> active#(X1) active#(divides(X1,X2)) -> active#(X2) -> active#(s(X)) -> s#(active(X)) active#(divides(X1,X2)) -> active#(X2) -> active#(s(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X2) -> active#(from(X)) -> from#(active(X)) active#(divides(X1,X2)) -> active#(X2) -> active#(from(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X2) -> active#(sieve(X)) -> sieve#(active(X)) active#(divides(X1,X2)) -> active#(X2) -> active#(sieve(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X2) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(divides(X1,X2)) -> active#(X2) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(divides(X1,X2)) -> active#(X2) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(divides(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(divides(X1,X2)) -> active#(X2) -> active#(from(X)) -> cons#(X,from(s(X))) active#(divides(X1,X2)) -> active#(X2) -> active#(from(X)) -> from#(s(X)) active#(divides(X1,X2)) -> active#(X2) -> active#(from(X)) -> s#(X) active#(divides(X1,X2)) -> active#(X2) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(divides(X1,X2)) -> active#(X2) -> active#(primes()) -> from#(s(s(0()))) active#(divides(X1,X2)) -> active#(X2) -> active#(primes()) -> s#(s(0())) active#(divides(X1,X2)) -> active#(X2) -> active#(primes()) -> s#(0()) active#(divides(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(divides(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> active#(X2) active#(divides(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(divides(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> active#(X1) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> active#(X2) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> active#(X1) active#(divides(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(divides(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(divides(X1,X2)) -> active#(X1) -> active#(tail(X)) -> tail#(active(X)) active#(divides(X1,X2)) -> active#(X1) -> active#(tail(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X1) -> active#(head(X)) -> head#(active(X)) active#(divides(X1,X2)) -> active#(X1) -> active#(head(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X1) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(divides(X1,X2)) -> active#(X1) -> active#(cons(X1,X2)) -> active#(X1) active#(divides(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(divides(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X1) -> active#(from(X)) -> from#(active(X)) active#(divides(X1,X2)) -> active#(X1) -> active#(from(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X1) -> active#(sieve(X)) -> sieve#(active(X)) active#(divides(X1,X2)) -> active#(X1) -> active#(sieve(X)) -> active#(X) active#(divides(X1,X2)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(divides(X1,X2)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(divides(X1,X2)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(divides(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(divides(X1,X2)) -> active#(X1) -> active#(from(X)) -> cons#(X,from(s(X))) active#(divides(X1,X2)) -> active#(X1) -> active#(from(X)) -> from#(s(X)) active#(divides(X1,X2)) -> active#(X1) -> active#(from(X)) -> s#(X) active#(divides(X1,X2)) -> active#(X1) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(divides(X1,X2)) -> active#(X1) -> active#(primes()) -> from#(s(s(0()))) active#(divides(X1,X2)) -> active#(X1) -> active#(primes()) -> s#(s(0())) active#(divides(X1,X2)) -> active#(X1) -> active#(primes()) -> s#(0()) active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) -> divides#(ok(X1),ok(X2)) -> divides#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) -> divides#(X1,mark(X2)) -> divides#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) -> divides#(mark(X1),X2) -> divides#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) -> filter#(ok(X1),ok(X2)) -> filter#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) -> filter#(X1,mark(X2)) -> filter#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) -> filter#(mark(X1),X2) -> filter#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) -> filter#(ok(X1),ok(X2)) -> filter#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) -> filter#(X1,mark(X2)) -> filter#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) -> filter#(mark(X1),X2) -> filter#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) -> cons#(ok(X1),ok(X2)) -> cons#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) -> cons#(mark(X1),X2) -> cons#(X1,X2) active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) -> sieve#(ok(X)) -> sieve#(X) active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) -> sieve#(mark(X)) -> sieve#(X) active#(filter(X1,X2)) -> filter#(active(X1),X2) -> filter#(ok(X1),ok(X2)) -> filter#(X1,X2) active#(filter(X1,X2)) -> filter#(active(X1),X2) -> filter#(X1,mark(X2)) -> filter#(X1,X2) active#(filter(X1,X2)) -> filter#(active(X1),X2) -> filter#(mark(X1),X2) -> filter#(X1,X2) active#(filter(X1,X2)) -> filter#(X1,active(X2)) -> filter#(ok(X1),ok(X2)) -> filter#(X1,X2) active#(filter(X1,X2)) -> filter#(X1,active(X2)) -> filter#(X1,mark(X2)) -> filter#(X1,X2) active#(filter(X1,X2)) -> filter#(X1,active(X2)) -> filter#(mark(X1),X2) -> filter#(X1,X2) active#(filter(X1,X2)) -> active#(X2) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(filter(X1,X2)) -> active#(X2) -> active#(divides(X1,X2)) -> active#(X2) active#(filter(X1,X2)) -> active#(X2) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(filter(X1,X2)) -> active#(X2) -> active#(divides(X1,X2)) -> active#(X1) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(X1,X2)) -> active#(X2) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(X1,X2)) -> active#(X1) active#(filter(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(filter(X1,X2)) -> active#(X2) -> active#(if(X1,X2,X3)) -> active#(X1) active#(filter(X1,X2)) -> active#(X2) -> active#(tail(X)) -> tail#(active(X)) active#(filter(X1,X2)) -> active#(X2) -> active#(tail(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X2) -> active#(head(X)) -> head#(active(X)) active#(filter(X1,X2)) -> active#(X2) -> active#(head(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X2) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(filter(X1,X2)) -> active#(X2) -> active#(cons(X1,X2)) -> active#(X1) active#(filter(X1,X2)) -> active#(X2) -> active#(s(X)) -> s#(active(X)) active#(filter(X1,X2)) -> active#(X2) -> active#(s(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X2) -> active#(from(X)) -> from#(active(X)) active#(filter(X1,X2)) -> active#(X2) -> active#(from(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X2) -> active#(sieve(X)) -> sieve#(active(X)) active#(filter(X1,X2)) -> active#(X2) -> active#(sieve(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X2) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(filter(X1,X2)) -> active#(X2) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(filter(X1,X2)) -> active#(X2) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(filter(X1,X2)) -> active#(X2) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(filter(X1,X2)) -> active#(X2) -> active#(from(X)) -> cons#(X,from(s(X))) active#(filter(X1,X2)) -> active#(X2) -> active#(from(X)) -> from#(s(X)) active#(filter(X1,X2)) -> active#(X2) -> active#(from(X)) -> s#(X) active#(filter(X1,X2)) -> active#(X2) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(filter(X1,X2)) -> active#(X2) -> active#(primes()) -> from#(s(s(0()))) active#(filter(X1,X2)) -> active#(X2) -> active#(primes()) -> s#(s(0())) active#(filter(X1,X2)) -> active#(X2) -> active#(primes()) -> s#(0()) active#(filter(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(filter(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> active#(X2) active#(filter(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(filter(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> active#(X1) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> active#(X2) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> active#(X1) active#(filter(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(filter(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(filter(X1,X2)) -> active#(X1) -> active#(tail(X)) -> tail#(active(X)) active#(filter(X1,X2)) -> active#(X1) -> active#(tail(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X1) -> active#(head(X)) -> head#(active(X)) active#(filter(X1,X2)) -> active#(X1) -> active#(head(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X1) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(filter(X1,X2)) -> active#(X1) -> active#(cons(X1,X2)) -> active#(X1) active#(filter(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(filter(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X1) -> active#(from(X)) -> from#(active(X)) active#(filter(X1,X2)) -> active#(X1) -> active#(from(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X1) -> active#(sieve(X)) -> sieve#(active(X)) active#(filter(X1,X2)) -> active#(X1) -> active#(sieve(X)) -> active#(X) active#(filter(X1,X2)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(filter(X1,X2)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(filter(X1,X2)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(filter(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(filter(X1,X2)) -> active#(X1) -> active#(from(X)) -> cons#(X,from(s(X))) active#(filter(X1,X2)) -> active#(X1) -> active#(from(X)) -> from#(s(X)) active#(filter(X1,X2)) -> active#(X1) -> active#(from(X)) -> s#(X) active#(filter(X1,X2)) -> active#(X1) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(filter(X1,X2)) -> active#(X1) -> active#(primes()) -> from#(s(s(0()))) active#(filter(X1,X2)) -> active#(X1) -> active#(primes()) -> s#(s(0())) active#(filter(X1,X2)) -> active#(X1) -> active#(primes()) -> s#(0()) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(if(X1,X2,X3)) -> active#(X1) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(divides(X1,X2)) -> active#(X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(divides(X1,X2)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(X1,X2)) -> active#(X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(X1,X2)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(if(X1,X2,X3)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(tail(X)) -> tail#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(tail(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(head(X)) -> head#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(head(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(if(X1,X2,X3)) -> active#(X1) -> active#(cons(X1,X2)) -> active#(X1) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(from(X)) -> from#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(from(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(sieve(X)) -> sieve#(active(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(sieve(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(if(X1,X2,X3)) -> active#(X1) -> active#(from(X)) -> cons#(X,from(s(X))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(from(X)) -> from#(s(X)) active#(if(X1,X2,X3)) -> active#(X1) -> active#(from(X)) -> s#(X) active#(if(X1,X2,X3)) -> active#(X1) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(primes()) -> from#(s(s(0()))) active#(if(X1,X2,X3)) -> active#(X1) -> active#(primes()) -> s#(s(0())) active#(if(X1,X2,X3)) -> active#(X1) -> active#(primes()) -> s#(0()) active#(tail(X)) -> tail#(active(X)) -> tail#(ok(X)) -> tail#(X) active#(tail(X)) -> tail#(active(X)) -> tail#(mark(X)) -> tail#(X) active#(tail(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(tail(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X2) active#(tail(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(tail(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X1) active#(tail(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(tail(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X2) active#(tail(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(tail(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X1) active#(tail(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(tail(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(tail(X)) -> active#(X) -> active#(tail(X)) -> tail#(active(X)) active#(tail(X)) -> active#(X) -> active#(tail(X)) -> active#(X) active#(tail(X)) -> active#(X) -> active#(head(X)) -> head#(active(X)) active#(tail(X)) -> active#(X) -> active#(head(X)) -> active#(X) active#(tail(X)) -> active#(X) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(tail(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1) active#(tail(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(tail(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(tail(X)) -> active#(X) -> active#(from(X)) -> from#(active(X)) active#(tail(X)) -> active#(X) -> active#(from(X)) -> active#(X) active#(tail(X)) -> active#(X) -> active#(sieve(X)) -> sieve#(active(X)) active#(tail(X)) -> active#(X) -> active#(sieve(X)) -> active#(X) active#(tail(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(tail(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(tail(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(tail(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(tail(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(tail(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(tail(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(tail(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(tail(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(tail(X)) -> active#(X) -> active#(from(X)) -> cons#(X,from(s(X))) active#(tail(X)) -> active#(X) -> active#(from(X)) -> from#(s(X)) active#(tail(X)) -> active#(X) -> active#(from(X)) -> s#(X) active#(tail(X)) -> active#(X) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(tail(X)) -> active#(X) -> active#(primes()) -> from#(s(s(0()))) active#(tail(X)) -> active#(X) -> active#(primes()) -> s#(s(0())) active#(tail(X)) -> active#(X) -> active#(primes()) -> s#(0()) active#(head(X)) -> head#(active(X)) -> head#(ok(X)) -> head#(X) active#(head(X)) -> head#(active(X)) -> head#(mark(X)) -> head#(X) active#(head(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(head(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X2) active#(head(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(head(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X1) active#(head(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(head(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X2) active#(head(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(head(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X1) active#(head(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(head(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(head(X)) -> active#(X) -> active#(tail(X)) -> tail#(active(X)) active#(head(X)) -> active#(X) -> active#(tail(X)) -> active#(X) active#(head(X)) -> active#(X) -> active#(head(X)) -> head#(active(X)) active#(head(X)) -> active#(X) -> active#(head(X)) -> active#(X) active#(head(X)) -> active#(X) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(head(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1) active#(head(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(head(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(head(X)) -> active#(X) -> active#(from(X)) -> from#(active(X)) active#(head(X)) -> active#(X) -> active#(from(X)) -> active#(X) active#(head(X)) -> active#(X) -> active#(sieve(X)) -> sieve#(active(X)) active#(head(X)) -> active#(X) -> active#(sieve(X)) -> active#(X) active#(head(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(head(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(head(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(head(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(head(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(head(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(head(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(head(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(head(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(head(X)) -> active#(X) -> active#(from(X)) -> cons#(X,from(s(X))) active#(head(X)) -> active#(X) -> active#(from(X)) -> from#(s(X)) active#(head(X)) -> active#(X) -> active#(from(X)) -> s#(X) active#(head(X)) -> active#(X) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(head(X)) -> active#(X) -> active#(primes()) -> from#(s(s(0()))) active#(head(X)) -> active#(X) -> active#(primes()) -> s#(s(0())) active#(head(X)) -> active#(X) -> active#(primes()) -> s#(0()) active#(cons(X1,X2)) -> cons#(active(X1),X2) -> cons#(ok(X1),ok(X2)) -> cons#(X1,X2) active#(cons(X1,X2)) -> cons#(active(X1),X2) -> cons#(mark(X1),X2) -> cons#(X1,X2) active#(cons(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(cons(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> active#(X2) active#(cons(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(cons(X1,X2)) -> active#(X1) -> active#(divides(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> active#(X2) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(cons(X1,X2)) -> active#(X1) -> active#(if(X1,X2,X3)) -> active#(X1) active#(cons(X1,X2)) -> active#(X1) -> active#(tail(X)) -> tail#(active(X)) active#(cons(X1,X2)) -> active#(X1) -> active#(tail(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) -> active#(head(X)) -> head#(active(X)) active#(cons(X1,X2)) -> active#(X1) -> active#(head(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(cons(X1,X2)) -> active#(X1) -> active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(cons(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) -> active#(from(X)) -> from#(active(X)) active#(cons(X1,X2)) -> active#(X1) -> active#(from(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) -> active#(sieve(X)) -> sieve#(active(X)) active#(cons(X1,X2)) -> active#(X1) -> active#(sieve(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(cons(X1,X2)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(cons(X1,X2)) -> active#(X1) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(cons(X1,X2)) -> active#(X1) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(cons(X1,X2)) -> active#(X1) -> active#(from(X)) -> cons#(X,from(s(X))) active#(cons(X1,X2)) -> active#(X1) -> active#(from(X)) -> from#(s(X)) active#(cons(X1,X2)) -> active#(X1) -> active#(from(X)) -> s#(X) active#(cons(X1,X2)) -> active#(X1) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(cons(X1,X2)) -> active#(X1) -> active#(primes()) -> from#(s(s(0()))) active#(cons(X1,X2)) -> active#(X1) -> active#(primes()) -> s#(s(0())) active#(cons(X1,X2)) -> active#(X1) -> active#(primes()) -> s#(0()) active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) -> filter#(ok(X1),ok(X2)) -> filter#(X1,X2) active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) -> filter#(X1,mark(X2)) -> filter#(X1,X2) active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) -> filter#(mark(X1),X2) -> filter#(X1,X2) active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) -> cons#(ok(X1),ok(X2)) -> cons#(X1,X2) active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) -> cons#(mark(X1),X2) -> cons#(X1,X2) active#(sieve(cons(X,Y))) -> sieve#(Y) -> sieve#(ok(X)) -> sieve#(X) active#(sieve(cons(X,Y))) -> sieve#(Y) -> sieve#(mark(X)) -> sieve#(X) active#(sieve(X)) -> sieve#(active(X)) -> sieve#(ok(X)) -> sieve#(X) active#(sieve(X)) -> sieve#(active(X)) -> sieve#(mark(X)) -> sieve#(X) active#(sieve(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(sieve(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X2) active#(sieve(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(sieve(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X1) active#(sieve(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(sieve(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X2) active#(sieve(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(sieve(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X1) active#(sieve(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(sieve(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(sieve(X)) -> active#(X) -> active#(tail(X)) -> tail#(active(X)) active#(sieve(X)) -> active#(X) -> active#(tail(X)) -> active#(X) active#(sieve(X)) -> active#(X) -> active#(head(X)) -> head#(active(X)) active#(sieve(X)) -> active#(X) -> active#(head(X)) -> active#(X) active#(sieve(X)) -> active#(X) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(sieve(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1) active#(sieve(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(sieve(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(sieve(X)) -> active#(X) -> active#(from(X)) -> from#(active(X)) active#(sieve(X)) -> active#(X) -> active#(from(X)) -> active#(X) active#(sieve(X)) -> active#(X) -> active#(sieve(X)) -> sieve#(active(X)) active#(sieve(X)) -> active#(X) -> active#(sieve(X)) -> active#(X) active#(sieve(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(sieve(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(sieve(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(sieve(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(sieve(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(sieve(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(sieve(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(sieve(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(sieve(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(sieve(X)) -> active#(X) -> active#(from(X)) -> cons#(X,from(s(X))) active#(sieve(X)) -> active#(X) -> active#(from(X)) -> from#(s(X)) active#(sieve(X)) -> active#(X) -> active#(from(X)) -> s#(X) active#(sieve(X)) -> active#(X) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(sieve(X)) -> active#(X) -> active#(primes()) -> from#(s(s(0()))) active#(sieve(X)) -> active#(X) -> active#(primes()) -> s#(s(0())) active#(sieve(X)) -> active#(X) -> active#(primes()) -> s#(0()) active#(from(X)) -> cons#(X,from(s(X))) -> cons#(ok(X1),ok(X2)) -> cons#(X1,X2) active#(from(X)) -> cons#(X,from(s(X))) -> cons#(mark(X1),X2) -> cons#(X1,X2) active#(from(X)) -> from#(s(X)) -> from#(ok(X)) -> from#(X) active#(from(X)) -> from#(s(X)) -> from#(mark(X)) -> from#(X) active#(from(X)) -> from#(active(X)) -> from#(ok(X)) -> from#(X) active#(from(X)) -> from#(active(X)) -> from#(mark(X)) -> from#(X) active#(from(X)) -> s#(X) -> s#(ok(X)) -> s#(X) active#(from(X)) -> s#(X) -> s#(mark(X)) -> s#(X) active#(from(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(from(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X2) active#(from(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(from(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X1) active#(from(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(from(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X2) active#(from(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(from(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X1) active#(from(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(from(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(from(X)) -> active#(X) -> active#(tail(X)) -> tail#(active(X)) active#(from(X)) -> active#(X) -> active#(tail(X)) -> active#(X) active#(from(X)) -> active#(X) -> active#(head(X)) -> head#(active(X)) active#(from(X)) -> active#(X) -> active#(head(X)) -> active#(X) active#(from(X)) -> active#(X) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1) active#(from(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(from(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(from(X)) -> active#(X) -> active#(from(X)) -> from#(active(X)) active#(from(X)) -> active#(X) -> active#(from(X)) -> active#(X) active#(from(X)) -> active#(X) -> active#(sieve(X)) -> sieve#(active(X)) active#(from(X)) -> active#(X) -> active#(sieve(X)) -> active#(X) active#(from(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(from(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(from(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(from(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(from(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(from(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(from(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(from(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(from(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(from(X)) -> active#(X) -> active#(from(X)) -> cons#(X,from(s(X))) active#(from(X)) -> active#(X) -> active#(from(X)) -> from#(s(X)) active#(from(X)) -> active#(X) -> active#(from(X)) -> s#(X) active#(from(X)) -> active#(X) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(from(X)) -> active#(X) -> active#(primes()) -> from#(s(s(0()))) active#(from(X)) -> active#(X) -> active#(primes()) -> s#(s(0())) active#(from(X)) -> active#(X) -> active#(primes()) -> s#(0()) active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X) active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X) active#(s(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(X1,active(X2)) active#(s(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X2) active#(s(X)) -> active#(X) -> active#(divides(X1,X2)) -> divides#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(divides(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(X1,active(X2)) active#(s(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X2) active#(s(X)) -> active#(X) -> active#(filter(X1,X2)) -> filter#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(filter(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3) active#(s(X)) -> active#(X) -> active#(if(X1,X2,X3)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(tail(X)) -> tail#(active(X)) active#(s(X)) -> active#(X) -> active#(tail(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(head(X)) -> head#(active(X)) active#(s(X)) -> active#(X) -> active#(head(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(from(X)) -> from#(active(X)) active#(s(X)) -> active#(X) -> active#(from(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(sieve(X)) -> sieve#(active(X)) active#(s(X)) -> active#(X) -> active#(sieve(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y))) active#(s(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y)) active#(s(X)) -> active#(X) -> active#(sieve(cons(X,Y))) -> sieve#(Y) active#(s(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) active#(s(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),Y) active#(s(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z) active#(s(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y))) active#(s(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y)) active#(s(X)) -> active#(X) -> active#(filter(s(s(X)),cons(Y,Z))) -> sieve#(Y) active#(s(X)) -> active#(X) -> active#(from(X)) -> cons#(X,from(s(X))) active#(s(X)) -> active#(X) -> active#(from(X)) -> from#(s(X)) active#(s(X)) -> active#(X) -> active#(from(X)) -> s#(X) active#(s(X)) -> active#(X) -> active#(primes()) -> sieve#(from(s(s(0())))) active#(s(X)) -> active#(X) -> active#(primes()) -> from#(s(s(0()))) active#(s(X)) -> active#(X) -> active#(primes()) -> s#(s(0())) active#(s(X)) -> active#(X) -> active#(primes()) -> s#(0()) active#(primes()) -> sieve#(from(s(s(0())))) -> sieve#(ok(X)) -> sieve#(X) active#(primes()) -> sieve#(from(s(s(0())))) -> sieve#(mark(X)) -> sieve#(X) active#(primes()) -> from#(s(s(0()))) -> from#(ok(X)) -> from#(X) active#(primes()) -> from#(s(s(0()))) -> from#(mark(X)) -> from#(X) active#(primes()) -> s#(s(0())) -> s#(ok(X)) -> s#(X) active#(primes()) -> s#(s(0())) -> s#(mark(X)) -> s#(X) active#(primes()) -> s#(0()) -> s#(ok(X)) -> s#(X) active#(primes()) -> s#(0()) -> s#(mark(X)) -> s#(X) SCC Processor: #sccs: 12 #rules: 47 #arcs: 937/7225 DPs: top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Open DPs: active#(sieve(X)) -> active#(X) active#(from(X)) -> active#(X) active#(s(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(head(X)) -> active#(X) active#(tail(X)) -> active#(X) active#(if(X1,X2,X3)) -> active#(X1) active#(filter(X1,X2)) -> active#(X1) active#(filter(X1,X2)) -> active#(X2) active#(divides(X1,X2)) -> active#(X1) active#(divides(X1,X2)) -> active#(X2) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(active#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: proper#(sieve(X)) -> proper#(X) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(head(X)) -> proper#(X) proper#(tail(X)) -> proper#(X) proper#(if(X1,X2,X3)) -> proper#(X3) proper#(if(X1,X2,X3)) -> proper#(X2) proper#(if(X1,X2,X3)) -> proper#(X1) proper#(filter(X1,X2)) -> proper#(X2) proper#(filter(X1,X2)) -> proper#(X1) proper#(divides(X1,X2)) -> proper#(X2) proper#(divides(X1,X2)) -> proper#(X1) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(proper#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: divides#(mark(X1),X2) -> divides#(X1,X2) divides#(X1,mark(X2)) -> divides#(X1,X2) divides#(ok(X1),ok(X2)) -> divides#(X1,X2) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(divides#) = 1 problem: DPs: divides#(mark(X1),X2) -> divides#(X1,X2) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(divides#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: filter#(mark(X1),X2) -> filter#(X1,X2) filter#(X1,mark(X2)) -> filter#(X1,X2) filter#(ok(X1),ok(X2)) -> filter#(X1,X2) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(filter#) = 1 problem: DPs: filter#(mark(X1),X2) -> filter#(X1,X2) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(filter#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(if#) = 2 problem: DPs: if#(mark(X1),X2,X3) -> if#(X1,X2,X3) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(if#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: tail#(mark(X)) -> tail#(X) tail#(ok(X)) -> tail#(X) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(tail#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: head#(mark(X)) -> head#(X) head#(ok(X)) -> head#(X) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(head#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: cons#(mark(X1),X2) -> cons#(X1,X2) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(cons#) = 1 problem: DPs: cons#(mark(X1),X2) -> cons#(X1,X2) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(cons#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: s#(mark(X)) -> s#(X) s#(ok(X)) -> s#(X) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(s#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: from#(mark(X)) -> from#(X) from#(ok(X)) -> from#(X) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(from#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: sieve#(mark(X)) -> sieve#(X) sieve#(ok(X)) -> sieve#(X) TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(sieve#) = 0 problem: DPs: TRS: active(primes()) -> mark(sieve(from(s(s(0()))))) active(from(X)) -> mark(cons(X,from(s(X)))) active(head(cons(X,Y))) -> mark(X) active(tail(cons(X,Y))) -> mark(Y) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))) active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y)))) active(sieve(X)) -> sieve(active(X)) active(from(X)) -> from(active(X)) active(s(X)) -> s(active(X)) active(cons(X1,X2)) -> cons(active(X1),X2) active(head(X)) -> head(active(X)) active(tail(X)) -> tail(active(X)) active(if(X1,X2,X3)) -> if(active(X1),X2,X3) active(filter(X1,X2)) -> filter(active(X1),X2) active(filter(X1,X2)) -> filter(X1,active(X2)) active(divides(X1,X2)) -> divides(active(X1),X2) active(divides(X1,X2)) -> divides(X1,active(X2)) sieve(mark(X)) -> mark(sieve(X)) from(mark(X)) -> mark(from(X)) s(mark(X)) -> mark(s(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) head(mark(X)) -> mark(head(X)) tail(mark(X)) -> mark(tail(X)) if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) filter(mark(X1),X2) -> mark(filter(X1,X2)) filter(X1,mark(X2)) -> mark(filter(X1,X2)) divides(mark(X1),X2) -> mark(divides(X1,X2)) divides(X1,mark(X2)) -> mark(divides(X1,X2)) proper(primes()) -> ok(primes()) proper(sieve(X)) -> sieve(proper(X)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(head(X)) -> head(proper(X)) proper(tail(X)) -> tail(proper(X)) proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) proper(true()) -> ok(true()) proper(false()) -> ok(false()) proper(filter(X1,X2)) -> filter(proper(X1),proper(X2)) proper(divides(X1,X2)) -> divides(proper(X1),proper(X2)) sieve(ok(X)) -> ok(sieve(X)) from(ok(X)) -> ok(from(X)) s(ok(X)) -> ok(s(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) head(ok(X)) -> ok(head(X)) tail(ok(X)) -> ok(tail(X)) if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) filter(ok(X1),ok(X2)) -> ok(filter(X1,X2)) divides(ok(X1),ok(X2)) -> ok(divides(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed