MAYBE Time: 1.326938 TRS: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} DP: DP: { sieve# mark X -> sieve# X, sieve# ok X -> sieve# X, from# mark X -> from# X, from# ok X -> from# X, s# mark X -> s# X, s# ok X -> s# X, active# sieve X -> sieve# active X, active# sieve X -> active# X, active# sieve cons(X, Y) -> sieve# Y, active# sieve cons(X, Y) -> cons#(X, filter(X, sieve Y)), active# sieve cons(X, Y) -> filter#(X, sieve Y), active# from X -> from# s X, active# from X -> from# active X, active# from X -> s# X, active# from X -> active# X, active# from X -> cons#(X, from s X), active# s X -> s# active X, active# s X -> active# X, active# primes() -> sieve# from s s 0(), active# primes() -> from# s s 0(), active# primes() -> s# s 0(), active# primes() -> s# 0(), 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# divides(X1, X2) -> active# X1, active# divides(X1, X2) -> active# X2, active# divides(X1, X2) -> divides#(X1, active X2), active# divides(X1, X2) -> divides#(active X1, X2), active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> active# X2, active# filter(X1, X2) -> filter#(X1, active X2), active# filter(X1, X2) -> filter#(active X1, X2), active# filter(s s X, cons(Y, Z)) -> sieve# Y, active# filter(s s X, cons(Y, Z)) -> cons#(Y, filter(X, sieve 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# filter(s s X, cons(Y, Z)) -> divides#(s s X, Y), active# filter(s s X, cons(Y, Z)) -> filter#(X, sieve Y), active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z), cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2), head# mark X -> head# X, head# ok X -> head# X, tail# mark X -> tail# X, tail# ok X -> tail# X, if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), divides#(X1, mark X2) -> divides#(X1, X2), divides#(mark X1, X2) -> divides#(X1, X2), divides#(ok X1, ok X2) -> divides#(X1, X2), filter#(X1, mark X2) -> filter#(X1, X2), filter#(mark X1, X2) -> filter#(X1, X2), filter#(ok X1, ok X2) -> filter#(X1, X2), proper# sieve X -> sieve# proper X, proper# sieve X -> proper# X, proper# from X -> from# proper X, proper# from X -> proper# X, proper# s X -> s# proper X, proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2), proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# head X -> head# proper X, proper# head X -> proper# X, proper# tail X -> tail# proper X, proper# tail X -> proper# X, 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# X2, proper# if(X1, X2, X3) -> proper# X3, proper# divides(X1, X2) -> divides#(proper X1, proper X2), proper# divides(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X2, proper# filter(X1, X2) -> filter#(proper X1, proper X2), proper# filter(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X2, top# mark X -> proper# X, top# mark X -> top# proper X, top# ok X -> active# X, top# ok X -> top# active X} TRS: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} UR: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2)} EDG: { (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# from X -> from# s X, from# ok X -> from# X) (active# from X -> from# s X, from# mark X -> from# X) (active# s X -> s# active X, s# ok X -> s# X) (active# s X -> s# active X, s# mark X -> s# X) (active# tail X -> tail# active X, tail# ok X -> tail# X) (active# tail X -> tail# active X, tail# mark X -> tail# X) (proper# from X -> from# proper X, from# ok X -> from# X) (proper# from X -> from# proper X, from# mark X -> from# X) (proper# head X -> head# proper X, head# ok X -> head# X) (proper# head X -> head# proper X, head# mark X -> head# X) (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) (proper# if(X1, X2, X3) -> proper# X3, proper# filter(X1, X2) -> 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) -> filter#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X3, proper# divides(X1, X2) -> 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) -> divides#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# tail X -> tail# proper X) (proper# if(X1, X2, X3) -> proper# X3, proper# head X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# head X -> head# proper X) (proper# if(X1, X2, X3) -> proper# X3, proper# cons(X1, X2) -> 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) -> cons#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X) (proper# if(X1, X2, X3) -> proper# X3, proper# from X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# from X -> from# proper X) (proper# if(X1, X2, X3) -> proper# X3, proper# sieve X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# sieve X -> sieve# proper 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#(mark X1, X2) -> divides#(X1, X2)) (active# divides(X1, X2) -> divides#(active X1, X2), divides#(X1, mark X2) -> divides#(X1, X2)) (sieve# mark X -> sieve# X, sieve# ok X -> sieve# X) (sieve# mark X -> sieve# X, sieve# mark X -> sieve# X) (from# mark X -> from# X, from# ok X -> from# X) (from# mark X -> from# X, from# mark X -> from# X) (s# mark X -> s# X, s# ok X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# sieve X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (active# sieve X -> active# X, active# primes() -> s# s 0()) (active# sieve X -> active# X, active# primes() -> from# s s 0()) (active# sieve X -> active# X, active# primes() -> sieve# from s s 0()) (active# sieve X -> active# X, active# s X -> active# X) (active# sieve X -> active# X, active# s X -> s# active X) (active# sieve X -> active# X, active# from X -> cons#(X, from s X)) (active# sieve X -> active# X, active# from X -> active# X) (active# sieve X -> active# X, active# from X -> s# X) (active# sieve X -> active# X, active# from X -> from# active X) (active# sieve X -> active# X, active# from X -> from# s X) (active# sieve X -> active# X, active# sieve cons(X, Y) -> filter#(X, sieve Y)) (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) -> sieve# Y) (active# sieve X -> active# X, active# sieve X -> active# X) (active# sieve X -> active# X, active# sieve X -> sieve# active X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# from X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (active# from X -> active# X, active# primes() -> s# s 0()) (active# from X -> active# X, active# primes() -> from# s s 0()) (active# from X -> active# X, active# primes() -> sieve# from s s 0()) (active# from X -> active# X, active# s X -> active# X) (active# from X -> active# X, active# s X -> s# active X) (active# from X -> active# X, active# from X -> cons#(X, from s X)) (active# from X -> active# X, active# from X -> active# X) (active# from X -> active# X, active# from X -> s# X) (active# from X -> active# X, active# from X -> from# active X) (active# from X -> active# X, active# from X -> from# s X) (active# from X -> active# X, active# sieve cons(X, Y) -> filter#(X, sieve Y)) (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) -> sieve# Y) (active# from X -> active# X, active# sieve X -> active# X) (active# from X -> active# X, active# sieve X -> sieve# active X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# head X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (active# head X -> active# X, active# primes() -> s# s 0()) (active# head X -> active# X, active# primes() -> from# s s 0()) (active# head X -> active# X, active# primes() -> sieve# from s s 0()) (active# head X -> active# X, active# s X -> active# X) (active# head X -> active# X, active# s X -> s# active X) (active# head X -> active# X, active# from X -> cons#(X, from s X)) (active# head X -> active# X, active# from X -> active# X) (active# head X -> active# X, active# from X -> s# X) (active# head X -> active# X, active# from X -> from# active X) (active# head X -> active# X, active# from X -> from# s X) (active# head X -> active# X, active# sieve cons(X, Y) -> filter#(X, sieve Y)) (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) -> sieve# Y) (active# head X -> active# X, active# sieve X -> active# X) (active# head X -> active# X, active# sieve X -> sieve# active X) (head# mark X -> head# X, head# ok X -> head# X) (head# mark X -> head# X, head# mark X -> head# X) (tail# mark X -> tail# X, tail# ok X -> tail# X) (tail# mark X -> tail# X, tail# mark X -> tail# X) (proper# sieve X -> proper# X, proper# filter(X1, X2) -> proper# X2) (proper# sieve X -> proper# X, proper# filter(X1, X2) -> proper# X1) (proper# sieve X -> proper# X, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# sieve X -> proper# X, proper# divides(X1, X2) -> proper# X2) (proper# sieve X -> proper# X, proper# divides(X1, X2) -> proper# X1) (proper# sieve X -> proper# X, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# sieve X -> proper# X, proper# if(X1, X2, X3) -> proper# X3) (proper# sieve X -> proper# X, proper# if(X1, X2, X3) -> proper# X2) (proper# sieve X -> 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)) (proper# sieve X -> proper# X, proper# tail X -> proper# X) (proper# sieve X -> proper# X, proper# tail X -> tail# proper X) (proper# sieve X -> proper# X, proper# head X -> proper# X) (proper# sieve X -> proper# X, proper# head X -> head# proper X) (proper# sieve X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# sieve X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# sieve X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# sieve X -> proper# X, proper# s X -> proper# X) (proper# sieve X -> proper# X, proper# s X -> s# proper X) (proper# sieve X -> proper# X, proper# from X -> proper# X) (proper# sieve X -> proper# X, proper# from X -> from# proper X) (proper# sieve X -> proper# X, proper# sieve X -> proper# X) (proper# sieve X -> proper# X, proper# sieve X -> sieve# proper X) (proper# s X -> proper# X, proper# filter(X1, X2) -> proper# X2) (proper# s X -> proper# X, proper# filter(X1, X2) -> proper# X1) (proper# s X -> proper# X, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# s X -> proper# X, proper# divides(X1, X2) -> proper# X2) (proper# s X -> proper# X, proper# divides(X1, X2) -> proper# X1) (proper# s X -> proper# X, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X3) (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X2) (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X1) (proper# s X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3)) (proper# s X -> proper# X, proper# tail X -> proper# X) (proper# s X -> proper# X, proper# tail X -> tail# proper X) (proper# s X -> proper# X, proper# head X -> proper# X) (proper# s X -> proper# X, proper# head X -> head# proper X) (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# s X -> proper# X, proper# s X -> proper# X) (proper# s X -> proper# X, proper# s X -> s# proper X) (proper# s X -> proper# X, proper# from X -> proper# X) (proper# s X -> proper# X, proper# from X -> from# proper X) (proper# s X -> proper# X, proper# sieve X -> proper# X) (proper# s X -> proper# X, proper# sieve X -> sieve# proper X) (proper# tail X -> proper# X, proper# filter(X1, X2) -> proper# X2) (proper# tail X -> proper# X, proper# filter(X1, X2) -> proper# X1) (proper# tail X -> proper# X, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# tail X -> proper# X, proper# divides(X1, X2) -> proper# X2) (proper# tail X -> proper# X, proper# divides(X1, X2) -> proper# X1) (proper# tail X -> proper# X, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# tail X -> proper# X, proper# if(X1, X2, X3) -> proper# X3) (proper# tail X -> proper# X, proper# if(X1, X2, X3) -> proper# X2) (proper# tail X -> proper# X, proper# if(X1, X2, X3) -> proper# X1) (proper# tail X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3)) (proper# tail X -> proper# X, proper# tail X -> proper# X) (proper# tail X -> proper# X, proper# tail X -> tail# proper X) (proper# tail X -> proper# X, proper# head X -> proper# X) (proper# tail X -> proper# X, proper# head X -> head# proper X) (proper# tail X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# tail X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# tail X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# tail X -> proper# X, proper# s X -> proper# X) (proper# tail X -> proper# X, proper# s X -> s# proper X) (proper# tail X -> proper# X, proper# from X -> proper# X) (proper# tail X -> proper# X, proper# from X -> from# proper X) (proper# tail X -> proper# X, proper# sieve X -> proper# X) (proper# tail X -> proper# X, proper# sieve X -> sieve# proper X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (top# ok X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (top# ok X -> active# X, active# primes() -> s# s 0()) (top# ok X -> active# X, active# primes() -> from# s s 0()) (top# ok X -> active# X, active# primes() -> sieve# from s s 0()) (top# ok X -> active# X, active# s X -> active# X) (top# ok X -> active# X, active# s X -> s# active X) (top# ok X -> active# X, active# from X -> cons#(X, from s X)) (top# ok X -> active# X, active# from X -> active# X) (top# ok X -> active# X, active# from X -> s# X) (top# ok X -> active# X, active# from X -> from# active X) (top# ok X -> active# X, active# from X -> from# s X) (top# ok X -> active# X, active# sieve cons(X, Y) -> filter#(X, sieve Y)) (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) -> sieve# Y) (top# ok X -> active# X, active# sieve X -> active# X) (top# ok X -> active# X, active# sieve X -> sieve# active X) (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)) (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#(mark X1, X2) -> filter#(X1, X2)) (active# sieve cons(X, Y) -> filter#(X, sieve Y), filter#(X1, mark 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#(mark X1, X2) -> filter#(X1, X2)) (active# filter(X1, X2) -> filter#(X1, active X2), filter#(X1, mark X2) -> filter#(X1, X2)) (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# 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#(mark X1, X2) -> filter#(X1, X2)) (proper# filter(X1, X2) -> filter#(proper X1, proper X2), filter#(X1, mark 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)) (divides#(mark X1, 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#(mark X1, X2) -> divides#(X1, X2), divides#(X1, mark X2) -> divides#(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#(mark X1, X2) -> filter#(X1, X2)) (filter#(X1, mark X2) -> filter#(X1, X2), filter#(X1, mark X2) -> filter#(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#(mark X1, X2) -> filter#(X1, X2)) (filter#(ok X1, ok X2) -> filter#(X1, X2), filter#(X1, mark X2) -> filter#(X1, X2)) (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)) (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#(mark X1, 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(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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# filter(X1, X2) -> active# X2, active# divides(X1, X2) -> divides#(active 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) -> 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# primes() -> s# 0()) (active# filter(X1, X2) -> active# X2, active# primes() -> s# s 0()) (active# filter(X1, X2) -> active# X2, active# primes() -> from# s s 0()) (active# filter(X1, X2) -> active# X2, active# primes() -> sieve# from s s 0()) (active# filter(X1, X2) -> active# X2, active# s X -> active# X) (active# filter(X1, X2) -> active# X2, active# s X -> s# active X) (active# filter(X1, X2) -> active# X2, active# from X -> cons#(X, from s X)) (active# filter(X1, X2) -> active# X2, active# from X -> active# X) (active# filter(X1, X2) -> active# X2, active# from X -> s# X) (active# filter(X1, X2) -> active# X2, active# from X -> from# active X) (active# filter(X1, X2) -> active# X2, active# from X -> from# s X) (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) -> cons#(X, filter(X, sieve Y))) (active# filter(X1, X2) -> active# X2, active# sieve cons(X, Y) -> sieve# Y) (active# filter(X1, X2) -> active# X2, active# sieve X -> active# X) (active# filter(X1, X2) -> active# X2, active# sieve X -> sieve# active X) (proper# if(X1, X2, X3) -> proper# X2, proper# filter(X1, X2) -> 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) -> filter#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X2, proper# divides(X1, X2) -> 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) -> divides#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# tail X -> tail# proper X) (proper# if(X1, X2, X3) -> proper# X2, proper# head X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# head X -> head# proper X) (proper# if(X1, X2, X3) -> proper# X2, proper# cons(X1, X2) -> 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) -> cons#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X) (proper# if(X1, X2, X3) -> proper# X2, proper# from X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# from X -> from# proper X) (proper# if(X1, X2, X3) -> proper# X2, proper# sieve X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# sieve X -> sieve# proper X) (proper# filter(X1, X2) -> proper# X2, proper# filter(X1, X2) -> proper# X2) (proper# filter(X1, X2) -> proper# X2, proper# filter(X1, X2) -> proper# X1) (proper# filter(X1, X2) -> proper# X2, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# filter(X1, X2) -> proper# X2, proper# divides(X1, X2) -> proper# X2) (proper# filter(X1, X2) -> proper# X2, proper# divides(X1, X2) -> proper# X1) (proper# filter(X1, X2) -> proper# X2, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# filter(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# tail X -> tail# proper X) (proper# filter(X1, X2) -> proper# X2, proper# head X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# head X -> head# proper X) (proper# filter(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2) (proper# filter(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1) (proper# filter(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# filter(X1, X2) -> proper# X2, proper# s X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# s X -> s# proper X) (proper# filter(X1, X2) -> proper# X2, proper# from X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# from X -> from# proper X) (proper# filter(X1, X2) -> proper# X2, proper# sieve X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# sieve X -> sieve# proper X) (active# primes() -> s# 0(), s# ok X -> s# X) (active# primes() -> s# 0(), s# mark X -> s# X) (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# primes() -> from# s s 0(), from# ok X -> from# X) (active# primes() -> from# s s 0(), from# mark X -> from# X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# cons(X1, X2) -> active# X1, active# divides(X1, X2) -> divides#(active 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) -> 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# primes() -> s# 0()) (active# cons(X1, X2) -> active# X1, active# primes() -> s# s 0()) (active# cons(X1, X2) -> active# X1, active# primes() -> from# s s 0()) (active# cons(X1, X2) -> active# X1, active# primes() -> sieve# from s s 0()) (active# cons(X1, X2) -> active# X1, active# s X -> active# X) (active# cons(X1, X2) -> active# X1, active# s X -> s# active X) (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X)) (active# cons(X1, X2) -> active# X1, active# from X -> active# X) (active# cons(X1, X2) -> active# X1, active# from X -> s# X) (active# cons(X1, X2) -> active# X1, active# from X -> from# active X) (active# cons(X1, X2) -> active# X1, active# from X -> from# s X) (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) -> cons#(X, filter(X, sieve Y))) (active# cons(X1, X2) -> active# X1, active# sieve cons(X, Y) -> sieve# Y) (active# cons(X1, X2) -> active# X1, active# sieve X -> active# X) (active# cons(X1, X2) -> active# X1, active# sieve X -> sieve# active X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# divides(X1, X2) -> active# X1, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (active# divides(X1, X2) -> active# X1, active# primes() -> s# s 0()) (active# divides(X1, X2) -> active# X1, active# primes() -> from# s s 0()) (active# divides(X1, X2) -> active# X1, active# primes() -> sieve# from s s 0()) (active# divides(X1, X2) -> active# X1, active# s X -> active# X) (active# divides(X1, X2) -> active# X1, active# s X -> s# active X) (active# divides(X1, X2) -> active# X1, active# from X -> cons#(X, from s X)) (active# divides(X1, X2) -> active# X1, active# from X -> active# X) (active# divides(X1, X2) -> active# X1, active# from X -> s# X) (active# divides(X1, X2) -> active# X1, active# from X -> from# active X) (active# divides(X1, X2) -> active# X1, active# from X -> from# s X) (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) -> cons#(X, filter(X, sieve Y))) (active# divides(X1, X2) -> active# X1, active# sieve cons(X, Y) -> sieve# Y) (active# divides(X1, X2) -> active# X1, active# sieve X -> active# X) (active# divides(X1, X2) -> active# X1, active# sieve X -> sieve# active X) (proper# cons(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X1, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X1, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# tail X -> tail# proper X) (proper# cons(X1, X2) -> proper# X1, proper# head X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# head X -> head# proper X) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X) (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X) (proper# cons(X1, X2) -> proper# X1, proper# sieve X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# sieve X -> sieve# proper X) (proper# divides(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X2) (proper# divides(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X1) (proper# divides(X1, X2) -> proper# X1, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# divides(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X2) (proper# divides(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X1) (proper# divides(X1, X2) -> proper# X1, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# divides(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# tail X -> tail# proper X) (proper# divides(X1, X2) -> proper# X1, proper# head X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# head X -> head# proper X) (proper# divides(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2) (proper# divides(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1) (proper# divides(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# divides(X1, X2) -> proper# X1, proper# s X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# s X -> s# proper X) (proper# divides(X1, X2) -> proper# X1, proper# from X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# from X -> from# proper X) (proper# divides(X1, X2) -> proper# X1, proper# sieve X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# sieve X -> sieve# 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) -> 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# s X -> s# proper X) (proper# filter(X1, X2) -> proper# X1, proper# s 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# head X -> head# proper X) (proper# filter(X1, X2) -> proper# X1, proper# head X -> proper# X) (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# 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# 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# 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) -> 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# 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# 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# 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# 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# 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# 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) (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) -> sieve# Y) (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# from X -> from# s X) (active# filter(X1, X2) -> active# X1, active# from X -> from# active X) (active# filter(X1, X2) -> active# X1, active# from X -> s# X) (active# filter(X1, X2) -> active# X1, active# from X -> active# X) (active# filter(X1, X2) -> active# X1, active# from X -> cons#(X, from s X)) (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# 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# filter(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1) (active# filter(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2)) (active# filter(X1, X2) -> active# X1, active# head X -> active# X) (active# filter(X1, X2) -> active# X1, active# head X -> head# active X) (active# filter(X1, X2) -> active# X1, active# tail X -> active# X) (active# filter(X1, X2) -> active# X1, active# tail X -> tail# active X) (active# filter(X1, X2) -> active# X1, active# if(X1, X2, X3) -> 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# divides(X1, X2) -> active# X1) (active# filter(X1, X2) -> active# X1, active# divides(X1, X2) -> active# X2) (active# filter(X1, X2) -> active# X1, active# divides(X1, X2) -> divides#(X1, active X2)) (active# filter(X1, X2) -> active# X1, active# divides(X1, X2) -> divides#(active X1, X2)) (active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> active# X1) (active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> active# X2) (active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> filter#(X1, active X2)) (active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> filter#(active X1, X2)) (active# filter(X1, X2) -> active# X1, active# filter(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# filter(X1, X2) -> active# X1, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (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) -> sieve# Y) (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# from X -> from# s X) (active# if(X1, X2, X3) -> active# X1, active# from X -> from# active X) (active# if(X1, X2, X3) -> active# X1, active# from X -> s# X) (active# if(X1, X2, X3) -> active# X1, active# from X -> active# X) (active# if(X1, X2, X3) -> active# X1, active# from X -> cons#(X, from s X)) (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# 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# if(X1, X2, X3) -> active# X1, active# cons(X1, X2) -> active# X1) (active# if(X1, X2, X3) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2)) (active# if(X1, X2, X3) -> active# X1, active# head X -> active# X) (active# if(X1, X2, X3) -> active# X1, active# head X -> head# active X) (active# if(X1, X2, X3) -> active# X1, active# tail X -> active# X) (active# if(X1, X2, X3) -> active# X1, active# tail X -> tail# active X) (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> 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# divides(X1, X2) -> active# X1) (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#(X1, 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# filter(X1, X2) -> active# X1) (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#(X1, 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(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# if(X1, X2, X3) -> active# X1, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (active# primes() -> s# s 0(), s# mark X -> s# X) (active# primes() -> s# s 0(), s# ok X -> s# X) (active# primes() -> sieve# from s s 0(), sieve# mark X -> sieve# X) (active# primes() -> sieve# from s s 0(), sieve# ok X -> sieve# X) (active# sieve cons(X, Y) -> sieve# Y, sieve# mark X -> sieve# X) (active# sieve cons(X, Y) -> sieve# Y, sieve# ok X -> sieve# X) (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2)) (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2)) (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# 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# s X -> s# proper X) (proper# divides(X1, X2) -> proper# X2, proper# s 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# head X -> head# proper X) (proper# divides(X1, X2) -> proper# X2, proper# head X -> proper# X) (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# 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# 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# 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# 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# s X -> s# proper X) (proper# cons(X1, X2) -> proper# X2, proper# s 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# head X -> head# proper X) (proper# cons(X1, X2) -> proper# X2, proper# head X -> proper# X) (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# 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# 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) (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) -> sieve# Y) (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# from X -> from# s X) (active# divides(X1, X2) -> active# X2, active# from X -> from# active X) (active# divides(X1, X2) -> active# X2, active# from X -> s# X) (active# divides(X1, X2) -> active# X2, active# from X -> active# X) (active# divides(X1, X2) -> active# X2, active# from X -> cons#(X, from s X)) (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# 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# X2, active# cons(X1, X2) -> active# X1) (active# divides(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2)) (active# divides(X1, X2) -> active# X2, active# head X -> active# X) (active# divides(X1, X2) -> active# X2, active# head X -> head# active X) (active# divides(X1, X2) -> active# X2, active# tail X -> active# X) (active# divides(X1, X2) -> active# X2, active# tail X -> tail# active X) (active# divides(X1, X2) -> active# X2, active# if(X1, X2, X3) -> 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# divides(X1, X2) -> active# X1) (active# divides(X1, X2) -> active# X2, active# divides(X1, X2) -> active# 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) -> divides#(active X1, X2)) (active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> active# X1) (active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> active# X2) (active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> filter#(X1, active X2)) (active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> filter#(active X1, X2)) (active# divides(X1, X2) -> active# X2, active# filter(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# divides(X1, X2) -> active# X2, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (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#(s s X, Z), filter#(ok X1, ok X2) -> filter#(X1, 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))), if#(mark X1, X2, 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#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (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#(mark X1, X2) -> filter#(X1, X2), filter#(ok X1, ok X2) -> filter#(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#(ok X1, ok 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)) (divides#(X1, mark X2) -> divides#(X1, X2), divides#(ok X1, ok X2) -> divides#(X1, X2)) (cons#(mark X1, 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)) (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# divides(X1, X2) -> divides#(proper X1, proper X2), divides#(ok X1, ok X2) -> divides#(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)) -> filter#(X, sieve Y), filter#(ok X1, ok X2) -> filter#(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) -> divides#(X1, active X2), divides#(ok X1, ok X2) -> divides#(X1, X2)) (if#(ok X1, ok X2, ok 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#(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) -> if#(active X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (top# mark X -> proper# X, proper# sieve X -> sieve# proper X) (top# mark X -> proper# X, proper# sieve 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# s X -> s# proper X) (top# mark X -> proper# X, proper# s 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# head X -> head# proper X) (top# mark X -> proper# X, proper# head X -> proper# X) (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# 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# 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) (proper# head X -> proper# X, proper# sieve X -> sieve# proper X) (proper# head X -> proper# X, proper# sieve 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# s X -> s# proper X) (proper# head X -> proper# X, proper# s 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# head X -> head# proper X) (proper# head X -> proper# X, proper# head X -> proper# X) (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# 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# 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# from X -> proper# X, proper# sieve X -> sieve# proper X) (proper# from X -> proper# X, proper# sieve 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# s X -> s# proper X) (proper# from X -> proper# X, proper# s 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# head X -> head# proper X) (proper# from X -> proper# X, proper# head X -> proper# X) (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# 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# 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) (tail# ok X -> tail# X, tail# mark X -> tail# X) (tail# ok X -> tail# X, tail# ok X -> tail# X) (head# ok X -> head# X, head# mark X -> head# X) (head# ok X -> head# X, head# ok X -> head# 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) -> sieve# Y) (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# from X -> from# s X) (active# tail X -> active# X, active# from X -> from# active X) (active# tail X -> active# X, active# from X -> s# X) (active# tail X -> active# X, active# from X -> active# X) (active# tail X -> active# X, active# from X -> cons#(X, from s X)) (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# 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# tail X -> active# X, active# cons(X1, X2) -> active# X1) (active# tail X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2)) (active# tail X -> active# X, active# head X -> active# X) (active# tail X -> active# X, active# head X -> head# active X) (active# tail X -> active# X, active# tail X -> active# X) (active# tail X -> active# X, active# tail X -> tail# active X) (active# tail X -> active# X, active# if(X1, X2, X3) -> active# X1) (active# tail X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3)) (active# tail X -> active# X, active# divides(X1, X2) -> active# X1) (active# tail X -> active# X, active# divides(X1, X2) -> active# X2) (active# tail X -> active# X, active# divides(X1, X2) -> divides#(X1, active X2)) (active# tail X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (active# tail X -> active# X, active# filter(X1, X2) -> active# X1) (active# tail X -> active# X, active# filter(X1, X2) -> active# X2) (active# tail X -> active# X, active# filter(X1, X2) -> filter#(X1, active X2)) (active# tail X -> active# X, active# filter(X1, X2) -> filter#(active X1, X2)) (active# tail X -> active# X, active# filter(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# tail X -> active# X, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (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) -> sieve# Y) (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# from X -> from# s X) (active# s X -> active# X, active# from X -> from# active X) (active# s X -> active# X, active# from X -> s# X) (active# s X -> active# X, active# from X -> active# X) (active# s X -> active# X, active# from X -> cons#(X, from s X)) (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# 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# s X -> active# X, active# cons(X1, X2) -> active# X1) (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2)) (active# s X -> active# X, active# head X -> active# X) (active# s X -> active# X, active# head X -> head# active X) (active# s X -> active# X, active# tail X -> active# X) (active# s X -> active# X, active# tail X -> tail# active X) (active# s X -> active# X, active# if(X1, X2, X3) -> active# X1) (active# s X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3)) (active# s X -> active# X, active# divides(X1, X2) -> active# X1) (active# s X -> active# X, active# divides(X1, X2) -> active# X2) (active# s X -> active# X, active# divides(X1, X2) -> divides#(X1, active X2)) (active# s X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (active# s X -> active# X, active# filter(X1, X2) -> active# X1) (active# s X -> active# X, active# filter(X1, X2) -> active# X2) (active# s X -> active# X, active# filter(X1, X2) -> filter#(X1, active X2)) (active# s X -> active# X, active# filter(X1, X2) -> filter#(active X1, X2)) (active# s X -> active# X, active# filter(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# s X -> active# X, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (active# from X -> s# X, s# mark X -> s# X) (active# from X -> s# X, s# ok X -> s# X) (s# ok X -> s# X, s# mark X -> s# X) (s# ok X -> s# X, s# ok X -> s# X) (from# ok X -> from# X, from# mark X -> from# X) (from# ok X -> from# X, from# ok X -> from# X) (sieve# ok X -> sieve# X, sieve# mark X -> sieve# X) (sieve# ok X -> sieve# X, sieve# ok X -> sieve# X) (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#(active X1, X2), filter#(ok X1, ok X2) -> filter#(X1, X2)) (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2)) (top# ok X -> top# active X, top# mark X -> proper# X) (top# ok X -> top# active X, top# mark X -> top# proper X) (top# ok X -> top# active X, top# ok X -> active# X) (top# ok X -> top# active X, top# ok X -> top# active X) (proper# tail X -> tail# proper X, tail# mark X -> tail# X) (proper# tail X -> tail# proper X, tail# ok X -> tail# X) (proper# s X -> s# proper X, s# mark X -> s# X) (proper# s X -> s# proper X, s# ok X -> s# X) (proper# sieve X -> sieve# proper X, sieve# mark X -> sieve# X) (proper# sieve X -> sieve# proper X, sieve# ok X -> sieve# X) (active# head X -> head# active X, head# mark X -> head# X) (active# head X -> head# active X, head# ok X -> head# X) (active# from X -> from# active X, from# mark X -> from# X) (active# from X -> from# active X, from# ok X -> from# X) (active# sieve X -> sieve# active X, sieve# mark X -> sieve# X) (active# sieve X -> sieve# active X, sieve# ok X -> sieve# X) (active# sieve cons(X, Y) -> cons#(X, filter(X, sieve Y)), cons#(mark X1, X2) -> cons#(X1, X2)) (active# sieve cons(X, Y) -> cons#(X, filter(X, sieve Y)), cons#(ok X1, ok X2) -> cons#(X1, X2)) } EDG: { (active# filter(s s X, cons(Y, Z)) -> cons#(Y, filter(X, sieve Y)), cons#(ok X1, ok 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# s X -> s# active X, s# ok X -> s# X) (active# s X -> s# active X, s# mark X -> s# X) (active# tail X -> tail# active X, tail# ok X -> tail# X) (active# tail X -> tail# active X, tail# mark X -> tail# X) (proper# from X -> from# proper X, from# ok X -> from# X) (proper# from X -> from# proper X, from# mark X -> from# X) (proper# head X -> head# proper X, head# ok X -> head# X) (proper# head X -> head# proper X, head# mark X -> head# X) (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) (proper# if(X1, X2, X3) -> proper# X3, proper# filter(X1, X2) -> 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) -> filter#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X3, proper# divides(X1, X2) -> 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) -> divides#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# tail X -> tail# proper X) (proper# if(X1, X2, X3) -> proper# X3, proper# head X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# head X -> head# proper X) (proper# if(X1, X2, X3) -> proper# X3, proper# cons(X1, X2) -> 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) -> cons#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X) (proper# if(X1, X2, X3) -> proper# X3, proper# from X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# from X -> from# proper X) (proper# if(X1, X2, X3) -> proper# X3, proper# sieve X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# sieve X -> sieve# proper 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#(mark X1, X2) -> divides#(X1, X2)) (sieve# mark X -> sieve# X, sieve# ok X -> sieve# X) (sieve# mark X -> sieve# X, sieve# mark X -> sieve# X) (from# mark X -> from# X, from# ok X -> from# X) (from# mark X -> from# X, from# mark X -> from# X) (s# mark X -> s# X, s# ok X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# sieve X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (active# sieve X -> active# X, active# primes() -> s# s 0()) (active# sieve X -> active# X, active# primes() -> from# s s 0()) (active# sieve X -> active# X, active# primes() -> sieve# from s s 0()) (active# sieve X -> active# X, active# s X -> active# X) (active# sieve X -> active# X, active# s X -> s# active X) (active# sieve X -> active# X, active# from X -> cons#(X, from s X)) (active# sieve X -> active# X, active# from X -> active# X) (active# sieve X -> active# X, active# from X -> s# X) (active# sieve X -> active# X, active# from X -> from# active X) (active# sieve X -> active# X, active# from X -> from# s X) (active# sieve X -> active# X, active# sieve cons(X, Y) -> filter#(X, sieve Y)) (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) -> sieve# Y) (active# sieve X -> active# X, active# sieve X -> active# X) (active# sieve X -> active# X, active# sieve X -> sieve# active X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# from X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (active# from X -> active# X, active# primes() -> s# s 0()) (active# from X -> active# X, active# primes() -> from# s s 0()) (active# from X -> active# X, active# primes() -> sieve# from s s 0()) (active# from X -> active# X, active# s X -> active# X) (active# from X -> active# X, active# s X -> s# active X) (active# from X -> active# X, active# from X -> cons#(X, from s X)) (active# from X -> active# X, active# from X -> active# X) (active# from X -> active# X, active# from X -> s# X) (active# from X -> active# X, active# from X -> from# active X) (active# from X -> active# X, active# from X -> from# s X) (active# from X -> active# X, active# sieve cons(X, Y) -> filter#(X, sieve Y)) (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) -> sieve# Y) (active# from X -> active# X, active# sieve X -> active# X) (active# from X -> active# X, active# sieve X -> sieve# active X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# head X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (active# head X -> active# X, active# primes() -> s# s 0()) (active# head X -> active# X, active# primes() -> from# s s 0()) (active# head X -> active# X, active# primes() -> sieve# from s s 0()) (active# head X -> active# X, active# s X -> active# X) (active# head X -> active# X, active# s X -> s# active X) (active# head X -> active# X, active# from X -> cons#(X, from s X)) (active# head X -> active# X, active# from X -> active# X) (active# head X -> active# X, active# from X -> s# X) (active# head X -> active# X, active# from X -> from# active X) (active# head X -> active# X, active# from X -> from# s X) (active# head X -> active# X, active# sieve cons(X, Y) -> filter#(X, sieve Y)) (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) -> sieve# Y) (active# head X -> active# X, active# sieve X -> active# X) (active# head X -> active# X, active# sieve X -> sieve# active X) (head# mark X -> head# X, head# ok X -> head# X) (head# mark X -> head# X, head# mark X -> head# X) (tail# mark X -> tail# X, tail# ok X -> tail# X) (tail# mark X -> tail# X, tail# mark X -> tail# X) (proper# sieve X -> proper# X, proper# filter(X1, X2) -> proper# X2) (proper# sieve X -> proper# X, proper# filter(X1, X2) -> proper# X1) (proper# sieve X -> proper# X, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# sieve X -> proper# X, proper# divides(X1, X2) -> proper# X2) (proper# sieve X -> proper# X, proper# divides(X1, X2) -> proper# X1) (proper# sieve X -> proper# X, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# sieve X -> proper# X, proper# if(X1, X2, X3) -> proper# X3) (proper# sieve X -> proper# X, proper# if(X1, X2, X3) -> proper# X2) (proper# sieve X -> 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)) (proper# sieve X -> proper# X, proper# tail X -> proper# X) (proper# sieve X -> proper# X, proper# tail X -> tail# proper X) (proper# sieve X -> proper# X, proper# head X -> proper# X) (proper# sieve X -> proper# X, proper# head X -> head# proper X) (proper# sieve X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# sieve X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# sieve X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# sieve X -> proper# X, proper# s X -> proper# X) (proper# sieve X -> proper# X, proper# s X -> s# proper X) (proper# sieve X -> proper# X, proper# from X -> proper# X) (proper# sieve X -> proper# X, proper# from X -> from# proper X) (proper# sieve X -> proper# X, proper# sieve X -> proper# X) (proper# sieve X -> proper# X, proper# sieve X -> sieve# proper X) (proper# s X -> proper# X, proper# filter(X1, X2) -> proper# X2) (proper# s X -> proper# X, proper# filter(X1, X2) -> proper# X1) (proper# s X -> proper# X, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# s X -> proper# X, proper# divides(X1, X2) -> proper# X2) (proper# s X -> proper# X, proper# divides(X1, X2) -> proper# X1) (proper# s X -> proper# X, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X3) (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X2) (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X1) (proper# s X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3)) (proper# s X -> proper# X, proper# tail X -> proper# X) (proper# s X -> proper# X, proper# tail X -> tail# proper X) (proper# s X -> proper# X, proper# head X -> proper# X) (proper# s X -> proper# X, proper# head X -> head# proper X) (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# s X -> proper# X, proper# s X -> proper# X) (proper# s X -> proper# X, proper# s X -> s# proper X) (proper# s X -> proper# X, proper# from X -> proper# X) (proper# s X -> proper# X, proper# from X -> from# proper X) (proper# s X -> proper# X, proper# sieve X -> proper# X) (proper# s X -> proper# X, proper# sieve X -> sieve# proper X) (proper# tail X -> proper# X, proper# filter(X1, X2) -> proper# X2) (proper# tail X -> proper# X, proper# filter(X1, X2) -> proper# X1) (proper# tail X -> proper# X, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# tail X -> proper# X, proper# divides(X1, X2) -> proper# X2) (proper# tail X -> proper# X, proper# divides(X1, X2) -> proper# X1) (proper# tail X -> proper# X, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# tail X -> proper# X, proper# if(X1, X2, X3) -> proper# X3) (proper# tail X -> proper# X, proper# if(X1, X2, X3) -> proper# X2) (proper# tail X -> proper# X, proper# if(X1, X2, X3) -> proper# X1) (proper# tail X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3)) (proper# tail X -> proper# X, proper# tail X -> proper# X) (proper# tail X -> proper# X, proper# tail X -> tail# proper X) (proper# tail X -> proper# X, proper# head X -> proper# X) (proper# tail X -> proper# X, proper# head X -> head# proper X) (proper# tail X -> proper# X, proper# cons(X1, X2) -> proper# X2) (proper# tail X -> proper# X, proper# cons(X1, X2) -> proper# X1) (proper# tail X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# tail X -> proper# X, proper# s X -> proper# X) (proper# tail X -> proper# X, proper# s X -> s# proper X) (proper# tail X -> proper# X, proper# from X -> proper# X) (proper# tail X -> proper# X, proper# from X -> from# proper X) (proper# tail X -> proper# X, proper# sieve X -> proper# X) (proper# tail X -> proper# X, proper# sieve X -> sieve# proper X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (top# ok X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (top# ok X -> active# X, active# primes() -> s# s 0()) (top# ok X -> active# X, active# primes() -> from# s s 0()) (top# ok X -> active# X, active# primes() -> sieve# from s s 0()) (top# ok X -> active# X, active# s X -> active# X) (top# ok X -> active# X, active# s X -> s# active X) (top# ok X -> active# X, active# from X -> cons#(X, from s X)) (top# ok X -> active# X, active# from X -> active# X) (top# ok X -> active# X, active# from X -> s# X) (top# ok X -> active# X, active# from X -> from# active X) (top# ok X -> active# X, active# from X -> from# s X) (top# ok X -> active# X, active# sieve cons(X, Y) -> filter#(X, sieve Y)) (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) -> sieve# Y) (top# ok X -> active# X, active# sieve X -> active# X) (top# ok X -> active# X, active# sieve X -> sieve# active X) (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)) (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# 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)) (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# 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#(mark X1, X2) -> filter#(X1, X2)) (proper# filter(X1, X2) -> filter#(proper X1, proper X2), filter#(X1, mark 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)) (divides#(mark X1, 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#(mark X1, X2) -> divides#(X1, X2), divides#(X1, mark X2) -> divides#(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#(mark X1, X2) -> filter#(X1, X2)) (filter#(X1, mark X2) -> filter#(X1, X2), filter#(X1, mark X2) -> filter#(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#(mark X1, X2) -> filter#(X1, X2)) (filter#(ok X1, ok X2) -> filter#(X1, X2), filter#(X1, mark X2) -> filter#(X1, X2)) (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)) (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#(mark X1, X2) -> divides#(X1, X2)) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# filter(X1, X2) -> active# X2, active# divides(X1, X2) -> divides#(active 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) -> 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# primes() -> s# 0()) (active# filter(X1, X2) -> active# X2, active# primes() -> s# s 0()) (active# filter(X1, X2) -> active# X2, active# primes() -> from# s s 0()) (active# filter(X1, X2) -> active# X2, active# primes() -> sieve# from s s 0()) (active# filter(X1, X2) -> active# X2, active# s X -> active# X) (active# filter(X1, X2) -> active# X2, active# s X -> s# active X) (active# filter(X1, X2) -> active# X2, active# from X -> cons#(X, from s X)) (active# filter(X1, X2) -> active# X2, active# from X -> active# X) (active# filter(X1, X2) -> active# X2, active# from X -> s# X) (active# filter(X1, X2) -> active# X2, active# from X -> from# active X) (active# filter(X1, X2) -> active# X2, active# from X -> from# s X) (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) -> cons#(X, filter(X, sieve Y))) (active# filter(X1, X2) -> active# X2, active# sieve cons(X, Y) -> sieve# Y) (active# filter(X1, X2) -> active# X2, active# sieve X -> active# X) (active# filter(X1, X2) -> active# X2, active# sieve X -> sieve# active X) (proper# if(X1, X2, X3) -> proper# X2, proper# filter(X1, X2) -> 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) -> filter#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X2, proper# divides(X1, X2) -> 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) -> divides#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# tail X -> tail# proper X) (proper# if(X1, X2, X3) -> proper# X2, proper# head X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# head X -> head# proper X) (proper# if(X1, X2, X3) -> proper# X2, proper# cons(X1, X2) -> 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) -> cons#(proper X1, proper X2)) (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X) (proper# if(X1, X2, X3) -> proper# X2, proper# from X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# from X -> from# proper X) (proper# if(X1, X2, X3) -> proper# X2, proper# sieve X -> proper# X) (proper# if(X1, X2, X3) -> proper# X2, proper# sieve X -> sieve# proper X) (proper# filter(X1, X2) -> proper# X2, proper# filter(X1, X2) -> proper# X2) (proper# filter(X1, X2) -> proper# X2, proper# filter(X1, X2) -> proper# X1) (proper# filter(X1, X2) -> proper# X2, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# filter(X1, X2) -> proper# X2, proper# divides(X1, X2) -> proper# X2) (proper# filter(X1, X2) -> proper# X2, proper# divides(X1, X2) -> proper# X1) (proper# filter(X1, X2) -> proper# X2, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# filter(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# tail X -> tail# proper X) (proper# filter(X1, X2) -> proper# X2, proper# head X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# head X -> head# proper X) (proper# filter(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2) (proper# filter(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1) (proper# filter(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# filter(X1, X2) -> proper# X2, proper# s X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# s X -> s# proper X) (proper# filter(X1, X2) -> proper# X2, proper# from X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# from X -> from# proper X) (proper# filter(X1, X2) -> proper# X2, proper# sieve X -> proper# X) (proper# filter(X1, X2) -> proper# X2, proper# sieve X -> sieve# proper X) (active# filter(s s X, cons(Y, Z)) -> sieve# Y, sieve# ok X -> sieve# X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# cons(X1, X2) -> active# X1, active# divides(X1, X2) -> divides#(active 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) -> 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# primes() -> s# 0()) (active# cons(X1, X2) -> active# X1, active# primes() -> s# s 0()) (active# cons(X1, X2) -> active# X1, active# primes() -> from# s s 0()) (active# cons(X1, X2) -> active# X1, active# primes() -> sieve# from s s 0()) (active# cons(X1, X2) -> active# X1, active# s X -> active# X) (active# cons(X1, X2) -> active# X1, active# s X -> s# active X) (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X)) (active# cons(X1, X2) -> active# X1, active# from X -> active# X) (active# cons(X1, X2) -> active# X1, active# from X -> s# X) (active# cons(X1, X2) -> active# X1, active# from X -> from# active X) (active# cons(X1, X2) -> active# X1, active# from X -> from# s X) (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) -> cons#(X, filter(X, sieve Y))) (active# cons(X1, X2) -> active# X1, active# sieve cons(X, Y) -> sieve# Y) (active# cons(X1, X2) -> active# X1, active# sieve X -> active# X) (active# cons(X1, X2) -> active# X1, active# sieve X -> sieve# active X) (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)) -> 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)) -> 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)) -> cons#(Y, 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# filter(X1, X2) -> filter#(active X1, X2)) (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) -> active# X1) (active# divides(X1, X2) -> active# X1, active# divides(X1, X2) -> divides#(active X1, X2)) (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) -> 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# primes() -> s# 0()) (active# divides(X1, X2) -> active# X1, active# primes() -> s# s 0()) (active# divides(X1, X2) -> active# X1, active# primes() -> from# s s 0()) (active# divides(X1, X2) -> active# X1, active# primes() -> sieve# from s s 0()) (active# divides(X1, X2) -> active# X1, active# s X -> active# X) (active# divides(X1, X2) -> active# X1, active# s X -> s# active X) (active# divides(X1, X2) -> active# X1, active# from X -> cons#(X, from s X)) (active# divides(X1, X2) -> active# X1, active# from X -> active# X) (active# divides(X1, X2) -> active# X1, active# from X -> s# X) (active# divides(X1, X2) -> active# X1, active# from X -> from# active X) (active# divides(X1, X2) -> active# X1, active# from X -> from# s X) (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) -> cons#(X, filter(X, sieve Y))) (active# divides(X1, X2) -> active# X1, active# sieve cons(X, Y) -> sieve# Y) (active# divides(X1, X2) -> active# X1, active# sieve X -> active# X) (active# divides(X1, X2) -> active# X1, active# sieve X -> sieve# active X) (proper# cons(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X1, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X1, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# tail X -> tail# proper X) (proper# cons(X1, X2) -> proper# X1, proper# head X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# head X -> head# proper X) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1) (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X) (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X) (proper# cons(X1, X2) -> proper# X1, proper# sieve X -> proper# X) (proper# cons(X1, X2) -> proper# X1, proper# sieve X -> sieve# proper X) (proper# divides(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X2) (proper# divides(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X1) (proper# divides(X1, X2) -> proper# X1, proper# filter(X1, X2) -> filter#(proper X1, proper X2)) (proper# divides(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X2) (proper# divides(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X1) (proper# divides(X1, X2) -> proper# X1, proper# divides(X1, X2) -> divides#(proper X1, proper X2)) (proper# divides(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3) (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# X1) (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# tail X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# tail X -> tail# proper X) (proper# divides(X1, X2) -> proper# X1, proper# head X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# head X -> head# proper X) (proper# divides(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2) (proper# divides(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1) (proper# divides(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2)) (proper# divides(X1, X2) -> proper# X1, proper# s X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# s X -> s# proper X) (proper# divides(X1, X2) -> proper# X1, proper# from X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# from X -> from# proper X) (proper# divides(X1, X2) -> proper# X1, proper# sieve X -> proper# X) (proper# divides(X1, X2) -> proper# X1, proper# sieve X -> sieve# 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) -> 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# s X -> s# proper X) (proper# filter(X1, X2) -> proper# X1, proper# s 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# head X -> head# proper X) (proper# filter(X1, X2) -> proper# X1, proper# head X -> proper# X) (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# 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# 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# 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) -> 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# 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# 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# 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# 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# 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# 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) (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) -> sieve# Y) (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# from X -> from# s X) (active# filter(X1, X2) -> active# X1, active# from X -> from# active X) (active# filter(X1, X2) -> active# X1, active# from X -> s# X) (active# filter(X1, X2) -> active# X1, active# from X -> active# X) (active# filter(X1, X2) -> active# X1, active# from X -> cons#(X, from s X)) (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# 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# filter(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1) (active# filter(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2)) (active# filter(X1, X2) -> active# X1, active# head X -> active# X) (active# filter(X1, X2) -> active# X1, active# head X -> head# active X) (active# filter(X1, X2) -> active# X1, active# tail X -> active# X) (active# filter(X1, X2) -> active# X1, active# tail X -> tail# active X) (active# filter(X1, X2) -> active# X1, active# if(X1, X2, X3) -> 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# divides(X1, X2) -> active# X1) (active# filter(X1, X2) -> active# X1, active# divides(X1, X2) -> active# X2) (active# filter(X1, X2) -> active# X1, active# divides(X1, X2) -> divides#(X1, active X2)) (active# filter(X1, X2) -> active# X1, active# divides(X1, X2) -> divides#(active X1, X2)) (active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> active# X1) (active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> active# X2) (active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> filter#(X1, active X2)) (active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> filter#(active X1, X2)) (active# filter(X1, X2) -> active# X1, active# filter(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# filter(X1, X2) -> active# X1, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (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) -> sieve# Y) (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# from X -> from# s X) (active# if(X1, X2, X3) -> active# X1, active# from X -> from# active X) (active# if(X1, X2, X3) -> active# X1, active# from X -> s# X) (active# if(X1, X2, X3) -> active# X1, active# from X -> active# X) (active# if(X1, X2, X3) -> active# X1, active# from X -> cons#(X, from s X)) (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# 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# if(X1, X2, X3) -> active# X1, active# cons(X1, X2) -> active# X1) (active# if(X1, X2, X3) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2)) (active# if(X1, X2, X3) -> active# X1, active# head X -> active# X) (active# if(X1, X2, X3) -> active# X1, active# head X -> head# active X) (active# if(X1, X2, X3) -> active# X1, active# tail X -> active# X) (active# if(X1, X2, X3) -> active# X1, active# tail X -> tail# active X) (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> 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# divides(X1, X2) -> active# X1) (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#(X1, 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# filter(X1, X2) -> active# X1) (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#(X1, 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(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# if(X1, X2, X3) -> active# X1, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (active# sieve cons(X, Y) -> sieve# Y, sieve# mark X -> sieve# X) (active# sieve cons(X, Y) -> sieve# Y, sieve# ok X -> sieve# 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# 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# s X -> s# proper X) (proper# divides(X1, X2) -> proper# X2, proper# s 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# head X -> head# proper X) (proper# divides(X1, X2) -> proper# X2, proper# head X -> proper# X) (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# 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# 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# 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# 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# s X -> s# proper X) (proper# cons(X1, X2) -> proper# X2, proper# s 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# head X -> head# proper X) (proper# cons(X1, X2) -> proper# X2, proper# head X -> proper# X) (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# 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# 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) (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) -> sieve# Y) (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# from X -> from# s X) (active# divides(X1, X2) -> active# X2, active# from X -> from# active X) (active# divides(X1, X2) -> active# X2, active# from X -> s# X) (active# divides(X1, X2) -> active# X2, active# from X -> active# X) (active# divides(X1, X2) -> active# X2, active# from X -> cons#(X, from s X)) (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# 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# X2, active# cons(X1, X2) -> active# X1) (active# divides(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2)) (active# divides(X1, X2) -> active# X2, active# head X -> active# X) (active# divides(X1, X2) -> active# X2, active# head X -> head# active X) (active# divides(X1, X2) -> active# X2, active# tail X -> active# X) (active# divides(X1, X2) -> active# X2, active# tail X -> tail# active X) (active# divides(X1, X2) -> active# X2, active# if(X1, X2, X3) -> 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# divides(X1, X2) -> active# X1) (active# divides(X1, X2) -> active# X2, active# divides(X1, X2) -> active# 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) -> divides#(active X1, X2)) (active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> active# X1) (active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> active# X2) (active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> filter#(X1, active X2)) (active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> filter#(active X1, X2)) (active# divides(X1, X2) -> active# X2, active# filter(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# divides(X1, X2) -> active# X2, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (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#(s s X, Z), filter#(ok X1, ok X2) -> filter#(X1, 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))), if#(mark X1, X2, 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#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (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#(mark X1, X2) -> filter#(X1, X2), filter#(ok X1, ok X2) -> filter#(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#(ok X1, ok 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)) (divides#(X1, mark X2) -> divides#(X1, X2), divides#(ok X1, ok X2) -> divides#(X1, X2)) (cons#(mark X1, 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)) (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# divides(X1, X2) -> divides#(proper X1, proper X2), divides#(ok X1, ok X2) -> divides#(X1, X2)) (active# filter(s s X, cons(Y, Z)) -> filter#(X, sieve Y), filter#(X1, mark X2) -> filter#(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#(ok X1, ok X2) -> divides#(X1, X2)) (if#(ok X1, ok X2, ok 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#(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) -> if#(active X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (top# mark X -> proper# X, proper# sieve X -> sieve# proper X) (top# mark X -> proper# X, proper# sieve 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# s X -> s# proper X) (top# mark X -> proper# X, proper# s 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# head X -> head# proper X) (top# mark X -> proper# X, proper# head X -> proper# X) (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# 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# 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) (proper# head X -> proper# X, proper# sieve X -> sieve# proper X) (proper# head X -> proper# X, proper# sieve 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# s X -> s# proper X) (proper# head X -> proper# X, proper# s 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# head X -> head# proper X) (proper# head X -> proper# X, proper# head X -> proper# X) (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# 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# 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# from X -> proper# X, proper# sieve X -> sieve# proper X) (proper# from X -> proper# X, proper# sieve 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# s X -> s# proper X) (proper# from X -> proper# X, proper# s 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# head X -> head# proper X) (proper# from X -> proper# X, proper# head X -> proper# X) (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# 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# 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) (tail# ok X -> tail# X, tail# mark X -> tail# X) (tail# ok X -> tail# X, tail# ok X -> tail# X) (head# ok X -> head# X, head# mark X -> head# X) (head# ok X -> head# X, head# ok X -> head# 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) -> sieve# Y) (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# from X -> from# s X) (active# tail X -> active# X, active# from X -> from# active X) (active# tail X -> active# X, active# from X -> s# X) (active# tail X -> active# X, active# from X -> active# X) (active# tail X -> active# X, active# from X -> cons#(X, from s X)) (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# 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# tail X -> active# X, active# cons(X1, X2) -> active# X1) (active# tail X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2)) (active# tail X -> active# X, active# head X -> active# X) (active# tail X -> active# X, active# head X -> head# active X) (active# tail X -> active# X, active# tail X -> active# X) (active# tail X -> active# X, active# tail X -> tail# active X) (active# tail X -> active# X, active# if(X1, X2, X3) -> active# X1) (active# tail X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3)) (active# tail X -> active# X, active# divides(X1, X2) -> active# X1) (active# tail X -> active# X, active# divides(X1, X2) -> active# X2) (active# tail X -> active# X, active# divides(X1, X2) -> divides#(X1, active X2)) (active# tail X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (active# tail X -> active# X, active# filter(X1, X2) -> active# X1) (active# tail X -> active# X, active# filter(X1, X2) -> active# X2) (active# tail X -> active# X, active# filter(X1, X2) -> filter#(X1, active X2)) (active# tail X -> active# X, active# filter(X1, X2) -> filter#(active X1, X2)) (active# tail X -> active# X, active# filter(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# tail X -> active# X, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (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) -> sieve# Y) (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# from X -> from# s X) (active# s X -> active# X, active# from X -> from# active X) (active# s X -> active# X, active# from X -> s# X) (active# s X -> active# X, active# from X -> active# X) (active# s X -> active# X, active# from X -> cons#(X, from s X)) (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# 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# s X -> active# X, active# cons(X1, X2) -> active# X1) (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2)) (active# s X -> active# X, active# head X -> active# X) (active# s X -> active# X, active# head X -> head# active X) (active# s X -> active# X, active# tail X -> active# X) (active# s X -> active# X, active# tail X -> tail# active X) (active# s X -> active# X, active# if(X1, X2, X3) -> active# X1) (active# s X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3)) (active# s X -> active# X, active# divides(X1, X2) -> active# X1) (active# s X -> active# X, active# divides(X1, X2) -> active# X2) (active# s X -> active# X, active# divides(X1, X2) -> divides#(X1, active X2)) (active# s X -> active# X, active# divides(X1, X2) -> divides#(active X1, X2)) (active# s X -> active# X, active# filter(X1, X2) -> active# X1) (active# s X -> active# X, active# filter(X1, X2) -> active# X2) (active# s X -> active# X, active# filter(X1, X2) -> filter#(X1, active X2)) (active# s X -> active# X, active# filter(X1, X2) -> filter#(active X1, X2)) (active# s X -> active# X, active# filter(s s X, cons(Y, Z)) -> sieve# Y) (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)) -> 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#(X, sieve Y)) (active# s X -> active# X, active# filter(s s X, cons(Y, Z)) -> filter#(s s X, Z)) (s# ok X -> s# X, s# mark X -> s# X) (s# ok X -> s# X, s# ok X -> s# X) (from# ok X -> from# X, from# mark X -> from# X) (from# ok X -> from# X, from# ok X -> from# X) (sieve# ok X -> sieve# X, sieve# mark X -> sieve# X) (sieve# ok X -> sieve# X, sieve# ok X -> sieve# X) (active# filter(X1, X2) -> filter#(active X1, X2), filter#(mark X1, X2) -> filter#(X1, X2)) (active# filter(X1, X2) -> filter#(active X1, X2), filter#(ok X1, ok X2) -> filter#(X1, X2)) (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2)) (top# ok X -> top# active X, top# mark X -> proper# X) (top# ok X -> top# active X, top# mark X -> top# proper X) (top# ok X -> top# active X, top# ok X -> active# X) (top# ok X -> top# active X, top# ok X -> top# active X) (proper# tail X -> tail# proper X, tail# mark X -> tail# X) (proper# tail X -> tail# proper X, tail# ok X -> tail# X) (proper# s X -> s# proper X, s# mark X -> s# X) (proper# s X -> s# proper X, s# ok X -> s# X) (proper# sieve X -> sieve# proper X, sieve# mark X -> sieve# X) (proper# sieve X -> sieve# proper X, sieve# ok X -> sieve# X) (active# head X -> head# active X, head# mark X -> head# X) (active# head X -> head# active X, head# ok X -> head# X) (active# from X -> from# active X, from# mark X -> from# X) (active# from X -> from# active X, from# ok X -> from# X) (active# sieve X -> sieve# active X, sieve# mark X -> sieve# X) (active# sieve X -> sieve# active X, sieve# ok X -> sieve# X) (active# sieve cons(X, Y) -> cons#(X, filter(X, sieve Y)), cons#(ok X1, ok X2) -> cons#(X1, X2)) } STATUS: arrows: 0.873495 SCCS (12): Scc: {top# mark X -> top# proper X, top# ok X -> top# active X} Scc: { 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# divides(X1, X2) -> active# X1, active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> active# X2} Scc: { proper# sieve X -> proper# X, proper# from X -> proper# X, proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# head X -> proper# X, proper# tail X -> proper# X, proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3, proper# divides(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X2, proper# filter(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X2} Scc: { filter#(X1, mark X2) -> filter#(X1, X2), filter#(mark X1, X2) -> filter#(X1, X2), filter#(ok X1, ok X2) -> filter#(X1, X2)} Scc: { divides#(X1, mark X2) -> divides#(X1, X2), divides#(mark X1, X2) -> divides#(X1, X2), divides#(ok X1, ok X2) -> divides#(X1, X2)} Scc: { if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)} Scc: {tail# mark X -> tail# X, tail# ok X -> tail# X} Scc: {head# mark X -> head# X, head# ok X -> head# X} Scc: {s# mark X -> s# X, s# ok X -> s# X} Scc: {from# mark X -> from# X, from# ok X -> from# X} Scc: {sieve# mark X -> sieve# X, sieve# ok X -> sieve# X} Scc: { cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2)} SCC (2): Strict: {top# mark X -> top# proper X, top# ok X -> top# active X} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (11): Strict: { 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# divides(X1, X2) -> active# X1, active# divides(X1, X2) -> active# X2, active# filter(X1, X2) -> active# X1, active# filter(X1, X2) -> active# X2} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (14): Strict: { proper# sieve X -> proper# X, proper# from X -> proper# X, proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2, proper# head X -> proper# X, proper# tail X -> proper# X, proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3, proper# divides(X1, X2) -> proper# X1, proper# divides(X1, X2) -> proper# X2, proper# filter(X1, X2) -> proper# X1, proper# filter(X1, X2) -> proper# X2} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (3): Strict: { filter#(X1, mark X2) -> filter#(X1, X2), filter#(mark X1, X2) -> filter#(X1, X2), filter#(ok X1, ok X2) -> filter#(X1, X2)} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (3): Strict: { divides#(X1, mark X2) -> divides#(X1, X2), divides#(mark X1, X2) -> divides#(X1, X2), divides#(ok X1, ok X2) -> divides#(X1, X2)} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (2): Strict: { if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (2): Strict: {tail# mark X -> tail# X, tail# ok X -> tail# X} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (2): Strict: {head# mark X -> head# X, head# ok X -> head# X} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (2): Strict: {s# mark X -> s# X, s# ok X -> s# X} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (2): Strict: {from# mark X -> from# X, from# ok X -> from# X} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (2): Strict: {sieve# mark X -> sieve# X, sieve# ok X -> sieve# X} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open SCC (2): Strict: { cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2)} Weak: { sieve mark X -> mark sieve X, sieve ok X -> ok sieve X, from mark X -> mark from X, from ok X -> ok from X, s mark X -> mark s X, s ok X -> ok s X, active sieve X -> sieve active X, active sieve cons(X, Y) -> mark cons(X, filter(X, sieve Y)), active from X -> mark cons(X, from s X), active from X -> from active X, active s X -> s active X, active primes() -> mark sieve from s s 0(), active cons(X1, X2) -> cons(active X1, X2), active head X -> head active X, active head cons(X, Y) -> mark X, active tail X -> tail active X, active tail cons(X, Y) -> mark Y, active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active divides(X1, X2) -> divides(X1, active X2), active divides(X1, X2) -> divides(active X1, X2), active filter(X1, X2) -> filter(X1, active X2), active filter(X1, X2) -> filter(active X1, X2), 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))), cons(mark X1, X2) -> mark cons(X1, X2), cons(ok X1, ok X2) -> ok cons(X1, X2), head mark X -> mark head X, head ok X -> ok head X, tail mark X -> mark tail X, tail ok X -> ok tail X, if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), divides(X1, mark X2) -> mark divides(X1, X2), divides(mark X1, X2) -> mark divides(X1, X2), divides(ok X1, ok X2) -> ok divides(X1, X2), filter(X1, mark X2) -> mark filter(X1, X2), filter(mark X1, X2) -> mark filter(X1, X2), filter(ok X1, ok X2) -> ok filter(X1, X2), proper sieve X -> sieve proper X, proper from X -> from proper X, proper s X -> s proper X, proper 0() -> ok 0(), proper primes() -> ok primes(), 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 divides(X1, X2) -> divides(proper X1, proper X2), proper filter(X1, X2) -> filter(proper X1, proper X2), top mark X -> top proper X, top ok X -> top active X} Open