MAYBE
Problem:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Proof:
DP Processor:
DPs:
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
active#(sieve(cons(0(),Y))) -> sieve#(Y)
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
active#(nats(N)) -> s#(N)
active#(nats(N)) -> nats#(s(N))
active#(nats(N)) -> cons#(N,nats(s(N)))
active#(zprimes()) -> s#(0())
active#(zprimes()) -> s#(s(0()))
active#(zprimes()) -> nats#(s(s(0())))
active#(zprimes()) -> sieve#(nats(s(s(0()))))
active#(filter(X1,X2,X3)) -> active#(X1)
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
active#(filter(X1,X2,X3)) -> active#(X2)
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
active#(filter(X1,X2,X3)) -> active#(X3)
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
active#(cons(X1,X2)) -> active#(X1)
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(s(X)) -> active#(X)
active#(s(X)) -> s#(active(X))
active#(sieve(X)) -> active#(X)
active#(sieve(X)) -> sieve#(active(X))
active#(nats(X)) -> active#(X)
active#(nats(X)) -> nats#(active(X))
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
cons#(mark(X1),X2) -> cons#(X1,X2)
s#(mark(X)) -> s#(X)
sieve#(mark(X)) -> sieve#(X)
nats#(mark(X)) -> nats#(X)
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
proper#(cons(X1,X2)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X1)
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(s(X)) -> proper#(X)
proper#(s(X)) -> s#(proper(X))
proper#(sieve(X)) -> proper#(X)
proper#(sieve(X)) -> sieve#(proper(X))
proper#(nats(X)) -> proper#(X)
proper#(nats(X)) -> nats#(proper(X))
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
s#(ok(X)) -> s#(X)
sieve#(ok(X)) -> sieve#(X)
nats#(ok(X)) -> nats#(X)
top#(mark(X)) -> proper#(X)
top#(mark(X)) -> top#(proper(X))
top#(ok(X)) -> active#(X)
top#(ok(X)) -> top#(active(X))
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
CDG Processor:
DPs:
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
active#(sieve(cons(0(),Y))) -> sieve#(Y)
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
active#(nats(N)) -> s#(N)
active#(nats(N)) -> nats#(s(N))
active#(nats(N)) -> cons#(N,nats(s(N)))
active#(zprimes()) -> s#(0())
active#(zprimes()) -> s#(s(0()))
active#(zprimes()) -> nats#(s(s(0())))
active#(zprimes()) -> sieve#(nats(s(s(0()))))
active#(filter(X1,X2,X3)) -> active#(X1)
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
active#(filter(X1,X2,X3)) -> active#(X2)
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
active#(filter(X1,X2,X3)) -> active#(X3)
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
active#(cons(X1,X2)) -> active#(X1)
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(s(X)) -> active#(X)
active#(s(X)) -> s#(active(X))
active#(sieve(X)) -> active#(X)
active#(sieve(X)) -> sieve#(active(X))
active#(nats(X)) -> active#(X)
active#(nats(X)) -> nats#(active(X))
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
cons#(mark(X1),X2) -> cons#(X1,X2)
s#(mark(X)) -> s#(X)
sieve#(mark(X)) -> sieve#(X)
nats#(mark(X)) -> nats#(X)
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
proper#(cons(X1,X2)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X1)
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(s(X)) -> proper#(X)
proper#(s(X)) -> s#(proper(X))
proper#(sieve(X)) -> proper#(X)
proper#(sieve(X)) -> sieve#(proper(X))
proper#(nats(X)) -> proper#(X)
proper#(nats(X)) -> nats#(proper(X))
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
s#(ok(X)) -> s#(X)
sieve#(ok(X)) -> sieve#(X)
nats#(ok(X)) -> nats#(X)
top#(mark(X)) -> proper#(X)
top#(mark(X)) -> top#(proper(X))
top#(ok(X)) -> active#(X)
top#(ok(X)) -> top#(active(X))
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
graph:
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))
top#(ok(X)) -> active#(X) ->
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
top#(ok(X)) -> active#(X) ->
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
top#(ok(X)) -> active#(X) ->
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
top#(ok(X)) -> active#(X) ->
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
top#(ok(X)) -> active#(X) -> active#(sieve(cons(0(),Y))) -> sieve#(Y)
top#(ok(X)) -> active#(X) ->
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
top#(ok(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
top#(ok(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
top#(ok(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
top#(ok(X)) -> active#(X) -> active#(nats(N)) -> s#(N)
top#(ok(X)) -> active#(X) -> active#(nats(N)) -> nats#(s(N))
top#(ok(X)) -> active#(X) -> active#(nats(N)) -> cons#(N,nats(s(N)))
top#(ok(X)) -> active#(X) -> active#(zprimes()) -> s#(0())
top#(ok(X)) -> active#(X) -> active#(zprimes()) -> s#(s(0()))
top#(ok(X)) -> active#(X) -> active#(zprimes()) -> nats#(s(s(0())))
top#(ok(X)) -> active#(X) ->
active#(zprimes()) -> sieve#(nats(s(s(0()))))
top#(ok(X)) -> active#(X) -> active#(filter(X1,X2,X3)) -> active#(X1)
top#(ok(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
top#(ok(X)) -> active#(X) -> active#(filter(X1,X2,X3)) -> active#(X2)
top#(ok(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
top#(ok(X)) -> active#(X) -> active#(filter(X1,X2,X3)) -> active#(X3)
top#(ok(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
top#(ok(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
top#(ok(X)) -> active#(X) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
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#(sieve(X)) -> active#(X)
top#(ok(X)) -> active#(X) -> active#(sieve(X)) -> sieve#(active(X))
top#(ok(X)) -> active#(X) -> active#(nats(X)) -> active#(X)
top#(ok(X)) -> active#(X) ->
active#(nats(X)) -> nats#(active(X))
top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X)
top#(mark(X)) -> top#(proper(X)) ->
top#(mark(X)) -> top#(proper(X))
top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X))
top#(mark(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X3)
top#(mark(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X2)
top#(mark(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X1)
top#(mark(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
top#(mark(X)) -> proper#(X) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
top#(mark(X)) -> proper#(X) -> proper#(sieve(X)) -> proper#(X)
top#(mark(X)) -> proper#(X) ->
proper#(sieve(X)) -> sieve#(proper(X))
top#(mark(X)) -> proper#(X) -> proper#(nats(X)) -> proper#(X)
top#(mark(X)) -> proper#(X) ->
proper#(nats(X)) -> nats#(proper(X))
proper#(nats(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(nats(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(nats(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(nats(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
proper#(nats(X)) -> proper#(X) ->
proper#(cons(X1,X2)) -> proper#(X2)
proper#(nats(X)) -> proper#(X) ->
proper#(cons(X1,X2)) -> proper#(X1)
proper#(nats(X)) -> proper#(X) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(nats(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
proper#(nats(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
proper#(nats(X)) -> proper#(X) -> proper#(sieve(X)) -> proper#(X)
proper#(nats(X)) -> proper#(X) ->
proper#(sieve(X)) -> sieve#(proper(X))
proper#(nats(X)) -> proper#(X) -> proper#(nats(X)) -> proper#(X)
proper#(nats(X)) -> proper#(X) ->
proper#(nats(X)) -> nats#(proper(X))
proper#(nats(X)) -> nats#(proper(X)) ->
nats#(mark(X)) -> nats#(X)
proper#(nats(X)) -> nats#(proper(X)) -> nats#(ok(X)) -> nats#(X)
proper#(sieve(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(sieve(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(sieve(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(sieve(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
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#(sieve(X)) -> proper#(X)
proper#(sieve(X)) -> proper#(X) ->
proper#(sieve(X)) -> sieve#(proper(X))
proper#(sieve(X)) -> proper#(X) ->
proper#(nats(X)) -> proper#(X)
proper#(sieve(X)) -> proper#(X) ->
proper#(nats(X)) -> nats#(proper(X))
proper#(sieve(X)) -> sieve#(proper(X)) ->
sieve#(mark(X)) -> sieve#(X)
proper#(sieve(X)) -> sieve#(proper(X)) -> sieve#(ok(X)) -> sieve#(X)
proper#(s(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(s(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(s(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(s(X)) -> proper#(X) ->
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
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#(sieve(X)) -> proper#(X)
proper#(s(X)) -> proper#(X) ->
proper#(sieve(X)) -> sieve#(proper(X))
proper#(s(X)) -> proper#(X) -> proper#(nats(X)) -> proper#(X)
proper#(s(X)) -> proper#(X) ->
proper#(nats(X)) -> nats#(proper(X))
proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(cons(X1,X2)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(cons(X1,X2)) -> proper#(X1)
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(s(X)) -> proper#(X)
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(s(X)) -> s#(proper(X))
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(sieve(X)) -> proper#(X)
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(sieve(X)) -> sieve#(proper(X))
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(nats(X)) -> proper#(X)
proper#(filter(X1,X2,X3)) -> proper#(X3) ->
proper#(nats(X)) -> nats#(proper(X))
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(cons(X1,X2)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(cons(X1,X2)) -> proper#(X1)
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(s(X)) -> proper#(X)
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(s(X)) -> s#(proper(X))
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(sieve(X)) -> proper#(X)
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(sieve(X)) -> sieve#(proper(X))
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(nats(X)) -> proper#(X)
proper#(filter(X1,X2,X3)) -> proper#(X2) ->
proper#(nats(X)) -> nats#(proper(X))
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(cons(X1,X2)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(cons(X1,X2)) -> proper#(X1)
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(s(X)) -> proper#(X)
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(s(X)) -> s#(proper(X))
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(sieve(X)) -> proper#(X)
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(sieve(X)) -> sieve#(proper(X))
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(nats(X)) -> proper#(X)
proper#(filter(X1,X2,X3)) -> proper#(X1) ->
proper#(nats(X)) -> nats#(proper(X))
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3)) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3)) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3)) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3)) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(cons(X1,X2)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(cons(X1,X2)) -> proper#(X1)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(s(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(s(X)) -> s#(proper(X))
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(sieve(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(sieve(X)) -> sieve#(proper(X))
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(nats(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X2) ->
proper#(nats(X)) -> nats#(proper(X))
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(filter(X1,X2,X3)) -> proper#(X3)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
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#(sieve(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(sieve(X)) -> sieve#(proper(X))
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(nats(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X1) ->
proper#(nats(X)) -> nats#(proper(X))
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
nats#(ok(X)) -> nats#(X) -> nats#(mark(X)) -> nats#(X)
nats#(ok(X)) -> nats#(X) -> nats#(ok(X)) -> nats#(X)
nats#(mark(X)) -> nats#(X) -> nats#(mark(X)) -> nats#(X)
nats#(mark(X)) -> nats#(X) -> nats#(ok(X)) -> nats#(X)
s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
sieve#(ok(X)) -> sieve#(X) -> sieve#(mark(X)) -> sieve#(X)
sieve#(ok(X)) -> sieve#(X) -> sieve#(ok(X)) -> sieve#(X)
sieve#(mark(X)) -> sieve#(X) -> sieve#(mark(X)) -> sieve#(X)
sieve#(mark(X)) -> sieve#(X) -> sieve#(ok(X)) -> sieve#(X)
cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
cons#(mark(X1),X2) -> cons#(X1,X2) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
cons#(mark(X1),X2) -> cons#(X1,X2) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
active#(nats(N)) -> nats#(s(N)) -> nats#(mark(X)) -> nats#(X)
active#(nats(N)) -> nats#(s(N)) -> nats#(ok(X)) -> nats#(X)
active#(nats(N)) -> s#(N) -> s#(mark(X)) -> s#(X)
active#(nats(N)) -> s#(N) -> s#(ok(X)) -> s#(X)
active#(nats(N)) -> cons#(N,nats(s(N))) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
active#(nats(N)) -> cons#(N,nats(s(N))) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
active#(nats(X)) -> nats#(active(X)) ->
nats#(mark(X)) -> nats#(X)
active#(nats(X)) -> nats#(active(X)) -> nats#(ok(X)) -> nats#(X)
active#(nats(X)) -> active#(X) ->
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
active#(nats(X)) -> active#(X) ->
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
active#(nats(X)) -> active#(X) ->
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
active#(nats(X)) -> active#(X) ->
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
active#(nats(X)) -> active#(X) ->
active#(sieve(cons(0(),Y))) -> sieve#(Y)
active#(nats(X)) -> active#(X) ->
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
active#(nats(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
active#(nats(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
active#(nats(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
active#(nats(X)) -> active#(X) -> active#(nats(N)) -> s#(N)
active#(nats(X)) -> active#(X) -> active#(nats(N)) -> nats#(s(N))
active#(nats(X)) -> active#(X) ->
active#(nats(N)) -> cons#(N,nats(s(N)))
active#(nats(X)) -> active#(X) -> active#(zprimes()) -> s#(0())
active#(nats(X)) -> active#(X) ->
active#(zprimes()) -> s#(s(0()))
active#(nats(X)) -> active#(X) ->
active#(zprimes()) -> nats#(s(s(0())))
active#(nats(X)) -> active#(X) ->
active#(zprimes()) -> sieve#(nats(s(s(0()))))
active#(nats(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> active#(X1)
active#(nats(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
active#(nats(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> active#(X2)
active#(nats(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
active#(nats(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> active#(X3)
active#(nats(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
active#(nats(X)) -> active#(X) ->
active#(cons(X1,X2)) -> active#(X1)
active#(nats(X)) -> active#(X) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(nats(X)) -> active#(X) -> active#(s(X)) -> active#(X)
active#(nats(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
active#(nats(X)) -> active#(X) -> active#(sieve(X)) -> active#(X)
active#(nats(X)) -> active#(X) ->
active#(sieve(X)) -> sieve#(active(X))
active#(nats(X)) -> active#(X) -> active#(nats(X)) -> active#(X)
active#(nats(X)) -> active#(X) ->
active#(nats(X)) -> nats#(active(X))
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N)) ->
sieve#(mark(X)) -> sieve#(X)
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N)) ->
sieve#(ok(X)) -> sieve#(X)
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N))) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N))) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
active#(sieve(cons(0(),Y))) -> sieve#(Y) ->
sieve#(mark(X)) -> sieve#(X)
active#(sieve(cons(0(),Y))) -> sieve#(Y) ->
sieve#(ok(X)) -> sieve#(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(X)) -> active#(X) ->
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
active#(sieve(X)) -> active#(X) ->
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
active#(sieve(X)) -> active#(X) ->
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
active#(sieve(X)) -> active#(X) ->
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
active#(sieve(X)) -> active#(X) ->
active#(sieve(cons(0(),Y))) -> sieve#(Y)
active#(sieve(X)) -> active#(X) ->
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
active#(sieve(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
active#(sieve(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
active#(sieve(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
active#(sieve(X)) -> active#(X) -> active#(nats(N)) -> s#(N)
active#(sieve(X)) -> active#(X) ->
active#(nats(N)) -> nats#(s(N))
active#(sieve(X)) -> active#(X) ->
active#(nats(N)) -> cons#(N,nats(s(N)))
active#(sieve(X)) -> active#(X) -> active#(zprimes()) -> s#(0())
active#(sieve(X)) -> active#(X) ->
active#(zprimes()) -> s#(s(0()))
active#(sieve(X)) -> active#(X) ->
active#(zprimes()) -> nats#(s(s(0())))
active#(sieve(X)) -> active#(X) ->
active#(zprimes()) -> sieve#(nats(s(s(0()))))
active#(sieve(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> active#(X1)
active#(sieve(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
active#(sieve(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> active#(X2)
active#(sieve(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
active#(sieve(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> active#(X3)
active#(sieve(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
active#(sieve(X)) -> active#(X) ->
active#(cons(X1,X2)) -> active#(X1)
active#(sieve(X)) -> active#(X) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
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#(sieve(X)) -> active#(X)
active#(sieve(X)) -> active#(X) ->
active#(sieve(X)) -> sieve#(active(X))
active#(sieve(X)) -> active#(X) ->
active#(nats(X)) -> active#(X)
active#(sieve(X)) -> active#(X) ->
active#(nats(X)) -> nats#(active(X))
active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X)
active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X)
active#(s(X)) -> active#(X) ->
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
active#(s(X)) -> active#(X) ->
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
active#(s(X)) -> active#(X) ->
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
active#(s(X)) -> active#(X) ->
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
active#(s(X)) -> active#(X) ->
active#(sieve(cons(0(),Y))) -> sieve#(Y)
active#(s(X)) -> active#(X) ->
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
active#(s(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
active#(s(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
active#(s(X)) -> active#(X) ->
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
active#(s(X)) -> active#(X) -> active#(nats(N)) -> s#(N)
active#(s(X)) -> active#(X) -> active#(nats(N)) -> nats#(s(N))
active#(s(X)) -> active#(X) ->
active#(nats(N)) -> cons#(N,nats(s(N)))
active#(s(X)) -> active#(X) -> active#(zprimes()) -> s#(0())
active#(s(X)) -> active#(X) -> active#(zprimes()) -> s#(s(0()))
active#(s(X)) -> active#(X) ->
active#(zprimes()) -> nats#(s(s(0())))
active#(s(X)) -> active#(X) ->
active#(zprimes()) -> sieve#(nats(s(s(0()))))
active#(s(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> active#(X1)
active#(s(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
active#(s(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> active#(X2)
active#(s(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
active#(s(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> active#(X3)
active#(s(X)) -> active#(X) ->
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
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#(s(X)) -> active#(X)
active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
active#(s(X)) -> active#(X) -> active#(sieve(X)) -> active#(X)
active#(s(X)) -> active#(X) ->
active#(sieve(X)) -> sieve#(active(X))
active#(s(X)) -> active#(X) -> active#(nats(X)) -> active#(X)
active#(s(X)) -> active#(X) ->
active#(nats(X)) -> nats#(active(X))
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M)) ->
cons#(mark(X1),X2) -> cons#(X1,X2)
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M)) ->
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3)) ->
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3)) ->
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3)) ->
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3)) ->
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(sieve(cons(0(),Y))) -> sieve#(Y)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(nats(N)) -> s#(N)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(nats(N)) -> nats#(s(N))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(nats(N)) -> cons#(N,nats(s(N)))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(zprimes()) -> s#(0())
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(zprimes()) -> s#(s(0()))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(zprimes()) -> nats#(s(s(0())))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(zprimes()) -> sieve#(nats(s(s(0()))))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(X1,X2,X3)) -> active#(X1)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(X1,X2,X3)) -> active#(X2)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(X1,X2,X3)) -> active#(X3)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(cons(X1,X2)) -> active#(X1)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(s(X)) -> active#(X)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(s(X)) -> s#(active(X))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(sieve(X)) -> active#(X)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(sieve(X)) -> sieve#(active(X))
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(nats(X)) -> active#(X)
active#(filter(X1,X2,X3)) -> active#(X3) ->
active#(nats(X)) -> nats#(active(X))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(sieve(cons(0(),Y))) -> sieve#(Y)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(nats(N)) -> s#(N)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(nats(N)) -> nats#(s(N))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(nats(N)) -> cons#(N,nats(s(N)))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(zprimes()) -> s#(0())
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(zprimes()) -> s#(s(0()))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(zprimes()) -> nats#(s(s(0())))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(zprimes()) -> sieve#(nats(s(s(0()))))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(X1,X2,X3)) -> active#(X1)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(X1,X2,X3)) -> active#(X2)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(X1,X2,X3)) -> active#(X3)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(cons(X1,X2)) -> active#(X1)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(s(X)) -> active#(X)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(s(X)) -> s#(active(X))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(sieve(X)) -> active#(X)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(sieve(X)) -> sieve#(active(X))
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(nats(X)) -> active#(X)
active#(filter(X1,X2,X3)) -> active#(X2) ->
active#(nats(X)) -> nats#(active(X))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(sieve(cons(0(),Y))) -> sieve#(Y)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(nats(N)) -> s#(N)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(nats(N)) -> nats#(s(N))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(nats(N)) -> cons#(N,nats(s(N)))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(zprimes()) -> s#(0())
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(zprimes()) -> s#(s(0()))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(zprimes()) -> nats#(s(s(0())))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(zprimes()) -> sieve#(nats(s(s(0()))))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> active#(X1)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> active#(X2)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> active#(X3)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(cons(X1,X2)) -> active#(X1)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(s(X)) -> active#(X)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(s(X)) -> s#(active(X))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(sieve(X)) -> active#(X)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(sieve(X)) -> sieve#(active(X))
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(nats(X)) -> active#(X)
active#(filter(X1,X2,X3)) -> active#(X1) ->
active#(nats(X)) -> nats#(active(X))
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)
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(cons(X,Y),0(),M)) -> filter#(Y,M,M)
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(cons(X,Y),0(),M)) -> cons#(0(),filter(Y,M,M))
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
active#(cons(X1,X2)) -> active#(X1) ->
active#(sieve(cons(0(),Y))) -> sieve#(Y)
active#(cons(X1,X2)) -> active#(X1) ->
active#(sieve(cons(0(),Y))) -> cons#(0(),sieve(Y))
active#(cons(X1,X2)) -> active#(X1) ->
active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
active#(cons(X1,X2)) -> active#(X1) ->
active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
active#(cons(X1,X2)) -> active#(X1) ->
active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
active#(cons(X1,X2)) -> active#(X1) ->
active#(nats(N)) -> s#(N)
active#(cons(X1,X2)) -> active#(X1) ->
active#(nats(N)) -> nats#(s(N))
active#(cons(X1,X2)) -> active#(X1) ->
active#(nats(N)) -> cons#(N,nats(s(N)))
active#(cons(X1,X2)) -> active#(X1) ->
active#(zprimes()) -> s#(0())
active#(cons(X1,X2)) -> active#(X1) ->
active#(zprimes()) -> s#(s(0()))
active#(cons(X1,X2)) -> active#(X1) ->
active#(zprimes()) -> nats#(s(s(0())))
active#(cons(X1,X2)) -> active#(X1) ->
active#(zprimes()) -> sieve#(nats(s(s(0()))))
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> active#(X1)
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> active#(X2)
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> active#(X3)
active#(cons(X1,X2)) -> active#(X1) ->
active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
active#(cons(X1,X2)) -> active#(X1) ->
active#(cons(X1,X2)) -> active#(X1)
active#(cons(X1,X2)) -> active#(X1) ->
active#(cons(X1,X2)) -> cons#(active(X1),X2)
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#(sieve(X)) -> active#(X)
active#(cons(X1,X2)) -> active#(X1) ->
active#(sieve(X)) -> sieve#(active(X))
active#(cons(X1,X2)) -> active#(X1) ->
active#(nats(X)) -> active#(X)
active#(cons(X1,X2)) -> active#(X1) -> active#(nats(X)) -> nats#(active(X))
SCC Processor:
#sccs: 8
#rules: 29
#arcs: 455/3481
DPs:
top#(ok(X)) -> top#(active(X))
top#(mark(X)) -> top#(proper(X))
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Open
DPs:
proper#(nats(X)) -> proper#(X)
proper#(sieve(X)) -> proper#(X)
proper#(s(X)) -> proper#(X)
proper#(cons(X1,X2)) -> proper#(X1)
proper#(cons(X1,X2)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X1)
proper#(filter(X1,X2,X3)) -> proper#(X2)
proper#(filter(X1,X2,X3)) -> proper#(X3)
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Open
DPs:
active#(nats(X)) -> active#(X)
active#(sieve(X)) -> active#(X)
active#(s(X)) -> active#(X)
active#(cons(X1,X2)) -> active#(X1)
active#(filter(X1,X2,X3)) -> active#(X3)
active#(filter(X1,X2,X3)) -> active#(X2)
active#(filter(X1,X2,X3)) -> active#(X1)
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Open
DPs:
filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Open
DPs:
cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
cons#(mark(X1),X2) -> cons#(X1,X2)
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Open
DPs:
s#(ok(X)) -> s#(X)
s#(mark(X)) -> s#(X)
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Open
DPs:
sieve#(ok(X)) -> sieve#(X)
sieve#(mark(X)) -> sieve#(X)
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Open
DPs:
nats#(ok(X)) -> nats#(X)
nats#(mark(X)) -> nats#(X)
TRS:
active(filter(cons(X,Y),0(),M)) -> mark(cons(0(),filter(Y,M,M)))
active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
active(sieve(cons(0(),Y))) -> mark(cons(0(),sieve(Y)))
active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
active(nats(N)) -> mark(cons(N,nats(s(N))))
active(zprimes()) -> mark(sieve(nats(s(s(0())))))
active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
active(cons(X1,X2)) -> cons(active(X1),X2)
active(s(X)) -> s(active(X))
active(sieve(X)) -> sieve(active(X))
active(nats(X)) -> nats(active(X))
filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
cons(mark(X1),X2) -> mark(cons(X1,X2))
s(mark(X)) -> mark(s(X))
sieve(mark(X)) -> mark(sieve(X))
nats(mark(X)) -> mark(nats(X))
proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(s(X)) -> s(proper(X))
proper(sieve(X)) -> sieve(proper(X))
proper(nats(X)) -> nats(proper(X))
proper(zprimes()) -> ok(zprimes())
filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
s(ok(X)) -> ok(s(X))
sieve(ok(X)) -> ok(sieve(X))
nats(ok(X)) -> ok(nats(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Open