YES Time: 0.246670 TRS: { a__filter(X1, X2, X3) -> filter(X1, X2, X3), a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3), mark s X -> s mark X, mark sieve X -> a__sieve mark X, mark nats X -> a__nats mark X, mark zprimes() -> a__zprimes(), a__sieve X -> sieve X, a__sieve cons(0(), Y) -> cons(0(), sieve Y), a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)), a__nats X -> nats X, a__nats N -> cons(mark N, nats s N), a__zprimes() -> a__sieve a__nats s s 0(), a__zprimes() -> zprimes()} DP: DP: {a__filter#(cons(X, Y), s N, M) -> mark# X, mark# cons(X1, X2) -> mark# X1, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3), mark# filter(X1, X2, X3) -> mark# X1, mark# filter(X1, X2, X3) -> mark# X2, mark# filter(X1, X2, X3) -> mark# X3, mark# s X -> mark# X, mark# sieve X -> mark# X, mark# sieve X -> a__sieve# mark X, mark# nats X -> mark# X, mark# nats X -> a__nats# mark X, mark# zprimes() -> a__zprimes#(), a__sieve# cons(s N, Y) -> mark# N, a__nats# N -> mark# N, a__zprimes#() -> a__sieve# a__nats s s 0(), a__zprimes#() -> a__nats# s s 0()} TRS: { a__filter(X1, X2, X3) -> filter(X1, X2, X3), a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3), mark s X -> s mark X, mark sieve X -> a__sieve mark X, mark nats X -> a__nats mark X, mark zprimes() -> a__zprimes(), a__sieve X -> sieve X, a__sieve cons(0(), Y) -> cons(0(), sieve Y), a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)), a__nats X -> nats X, a__nats N -> cons(mark N, nats s N), a__zprimes() -> a__sieve a__nats s s 0(), a__zprimes() -> zprimes()} EDG: {(mark# nats X -> a__nats# mark X, a__nats# N -> mark# N) (mark# filter(X1, X2, X3) -> mark# X1, mark# zprimes() -> a__zprimes#()) (mark# filter(X1, X2, X3) -> mark# X1, mark# nats X -> a__nats# mark X) (mark# filter(X1, X2, X3) -> mark# X1, mark# nats X -> mark# X) (mark# filter(X1, X2, X3) -> mark# X1, mark# sieve X -> a__sieve# mark X) (mark# filter(X1, X2, X3) -> mark# X1, mark# sieve X -> mark# X) (mark# filter(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# filter(X1, X2, X3) -> mark# X1, mark# filter(X1, X2, X3) -> mark# X3) (mark# filter(X1, X2, X3) -> mark# X1, mark# filter(X1, X2, X3) -> mark# X2) (mark# filter(X1, X2, X3) -> mark# X1, mark# filter(X1, X2, X3) -> mark# X1) (mark# filter(X1, X2, X3) -> mark# X1, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (mark# filter(X1, X2, X3) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3), a__filter#(cons(X, Y), s N, M) -> mark# X) (a__zprimes#() -> a__nats# s s 0(), a__nats# N -> mark# N) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# zprimes() -> a__zprimes#()) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# nats X -> a__nats# mark X) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# nats X -> mark# X) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# sieve X -> a__sieve# mark X) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# sieve X -> mark# X) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# s X -> mark# X) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# filter(X1, X2, X3) -> mark# X3) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# filter(X1, X2, X3) -> mark# X2) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# filter(X1, X2, X3) -> mark# X1) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (a__filter#(cons(X, Y), s N, M) -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# sieve X -> mark# X, mark# zprimes() -> a__zprimes#()) (mark# sieve X -> mark# X, mark# nats X -> a__nats# mark X) (mark# sieve X -> mark# X, mark# nats X -> mark# X) (mark# sieve X -> mark# X, mark# sieve X -> a__sieve# mark X) (mark# sieve X -> mark# X, mark# sieve X -> mark# X) (mark# sieve X -> mark# X, mark# s X -> mark# X) (mark# sieve X -> mark# X, mark# filter(X1, X2, X3) -> mark# X3) (mark# sieve X -> mark# X, mark# filter(X1, X2, X3) -> mark# X2) (mark# sieve X -> mark# X, mark# filter(X1, X2, X3) -> mark# X1) (mark# sieve X -> mark# X, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (mark# sieve X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# filter(X1, X2, X3) -> mark# X3, mark# zprimes() -> a__zprimes#()) (mark# filter(X1, X2, X3) -> mark# X3, mark# nats X -> a__nats# mark X) (mark# filter(X1, X2, X3) -> mark# X3, mark# nats X -> mark# X) (mark# filter(X1, X2, X3) -> mark# X3, mark# sieve X -> a__sieve# mark X) (mark# filter(X1, X2, X3) -> mark# X3, mark# sieve X -> mark# X) (mark# filter(X1, X2, X3) -> mark# X3, mark# s X -> mark# X) (mark# filter(X1, X2, X3) -> mark# X3, mark# filter(X1, X2, X3) -> mark# X3) (mark# filter(X1, X2, X3) -> mark# X3, mark# filter(X1, X2, X3) -> mark# X2) (mark# filter(X1, X2, X3) -> mark# X3, mark# filter(X1, X2, X3) -> mark# X1) (mark# filter(X1, X2, X3) -> mark# X3, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (mark# filter(X1, X2, X3) -> mark# X3, mark# cons(X1, X2) -> mark# X1) (a__nats# N -> mark# N, mark# zprimes() -> a__zprimes#()) (a__nats# N -> mark# N, mark# nats X -> a__nats# mark X) (a__nats# N -> mark# N, mark# nats X -> mark# X) (a__nats# N -> mark# N, mark# sieve X -> a__sieve# mark X) (a__nats# N -> mark# N, mark# sieve X -> mark# X) (a__nats# N -> mark# N, mark# s X -> mark# X) (a__nats# N -> mark# N, mark# filter(X1, X2, X3) -> mark# X3) (a__nats# N -> mark# N, mark# filter(X1, X2, X3) -> mark# X2) (a__nats# N -> mark# N, mark# filter(X1, X2, X3) -> mark# X1) (a__nats# N -> mark# N, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (a__nats# N -> mark# N, mark# cons(X1, X2) -> mark# X1) (a__sieve# cons(s N, Y) -> mark# N, mark# cons(X1, X2) -> mark# X1) (a__sieve# cons(s N, Y) -> mark# N, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (a__sieve# cons(s N, Y) -> mark# N, mark# filter(X1, X2, X3) -> mark# X1) (a__sieve# cons(s N, Y) -> mark# N, mark# filter(X1, X2, X3) -> mark# X2) (a__sieve# cons(s N, Y) -> mark# N, mark# filter(X1, X2, X3) -> mark# X3) (a__sieve# cons(s N, Y) -> mark# N, mark# s X -> mark# X) (a__sieve# cons(s N, Y) -> mark# N, mark# sieve X -> mark# X) (a__sieve# cons(s N, Y) -> mark# N, mark# sieve X -> a__sieve# mark X) (a__sieve# cons(s N, Y) -> mark# N, mark# nats X -> mark# X) (a__sieve# cons(s N, Y) -> mark# N, mark# nats X -> a__nats# mark X) (a__sieve# cons(s N, Y) -> mark# N, mark# zprimes() -> a__zprimes#()) (mark# nats X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# nats X -> mark# X, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (mark# nats X -> mark# X, mark# filter(X1, X2, X3) -> mark# X1) (mark# nats X -> mark# X, mark# filter(X1, X2, X3) -> mark# X2) (mark# nats X -> mark# X, mark# filter(X1, X2, X3) -> mark# X3) (mark# nats X -> mark# X, mark# s X -> mark# X) (mark# nats X -> mark# X, mark# sieve X -> mark# X) (mark# nats X -> mark# X, mark# sieve X -> a__sieve# mark X) (mark# nats X -> mark# X, mark# nats X -> mark# X) (mark# nats X -> mark# X, mark# nats X -> a__nats# mark X) (mark# nats X -> mark# X, mark# zprimes() -> a__zprimes#()) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (mark# s X -> mark# X, mark# filter(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# filter(X1, X2, X3) -> mark# X2) (mark# s X -> mark# X, mark# filter(X1, X2, X3) -> mark# X3) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# sieve X -> mark# X) (mark# s X -> mark# X, mark# sieve X -> a__sieve# mark X) (mark# s X -> mark# X, mark# nats X -> mark# X) (mark# s X -> mark# X, mark# nats X -> a__nats# mark X) (mark# s X -> mark# X, mark# zprimes() -> a__zprimes#()) (mark# filter(X1, X2, X3) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# filter(X1, X2, X3) -> mark# X2, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (mark# filter(X1, X2, X3) -> mark# X2, mark# filter(X1, X2, X3) -> mark# X1) (mark# filter(X1, X2, X3) -> mark# X2, mark# filter(X1, X2, X3) -> mark# X2) (mark# filter(X1, X2, X3) -> mark# X2, mark# filter(X1, X2, X3) -> mark# X3) (mark# filter(X1, X2, X3) -> mark# X2, mark# s X -> mark# X) (mark# filter(X1, X2, X3) -> mark# X2, mark# sieve X -> mark# X) (mark# filter(X1, X2, X3) -> mark# X2, mark# sieve X -> a__sieve# mark X) (mark# filter(X1, X2, X3) -> mark# X2, mark# nats X -> mark# X) (mark# filter(X1, X2, X3) -> mark# X2, mark# nats X -> a__nats# mark X) (mark# filter(X1, X2, X3) -> mark# X2, mark# zprimes() -> a__zprimes#()) (a__zprimes#() -> a__sieve# a__nats s s 0(), a__sieve# cons(s N, Y) -> mark# N) (mark# zprimes() -> a__zprimes#(), a__zprimes#() -> a__sieve# a__nats s s 0()) (mark# zprimes() -> a__zprimes#(), a__zprimes#() -> a__nats# s s 0()) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3)) (mark# cons(X1, X2) -> mark# X1, mark# filter(X1, X2, X3) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# filter(X1, X2, X3) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# filter(X1, X2, X3) -> mark# X3) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sieve X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# sieve X -> a__sieve# mark X) (mark# cons(X1, X2) -> mark# X1, mark# nats X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# nats X -> a__nats# mark X) (mark# cons(X1, X2) -> mark# X1, mark# zprimes() -> a__zprimes#()) (mark# sieve X -> a__sieve# mark X, a__sieve# cons(s N, Y) -> mark# N)} STATUS: arrows: 0.542969 SCCS (1): Scc: {a__filter#(cons(X, Y), s N, M) -> mark# X, mark# cons(X1, X2) -> mark# X1, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3), mark# filter(X1, X2, X3) -> mark# X1, mark# filter(X1, X2, X3) -> mark# X2, mark# filter(X1, X2, X3) -> mark# X3, mark# s X -> mark# X, mark# sieve X -> mark# X, mark# sieve X -> a__sieve# mark X, mark# nats X -> mark# X, mark# nats X -> a__nats# mark X, mark# zprimes() -> a__zprimes#(), a__sieve# cons(s N, Y) -> mark# N, a__nats# N -> mark# N, a__zprimes#() -> a__sieve# a__nats s s 0(), a__zprimes#() -> a__nats# s s 0()} SCC (16): Strict: {a__filter#(cons(X, Y), s N, M) -> mark# X, mark# cons(X1, X2) -> mark# X1, mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3), mark# filter(X1, X2, X3) -> mark# X1, mark# filter(X1, X2, X3) -> mark# X2, mark# filter(X1, X2, X3) -> mark# X3, mark# s X -> mark# X, mark# sieve X -> mark# X, mark# sieve X -> a__sieve# mark X, mark# nats X -> mark# X, mark# nats X -> a__nats# mark X, mark# zprimes() -> a__zprimes#(), a__sieve# cons(s N, Y) -> mark# N, a__nats# N -> mark# N, a__zprimes#() -> a__sieve# a__nats s s 0(), a__zprimes#() -> a__nats# s s 0()} Weak: { a__filter(X1, X2, X3) -> filter(X1, X2, X3), a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3), mark s X -> s mark X, mark sieve X -> a__sieve mark X, mark nats X -> a__nats mark X, mark zprimes() -> a__zprimes(), a__sieve X -> sieve X, a__sieve cons(0(), Y) -> cons(0(), sieve Y), a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)), a__nats X -> nats X, a__nats N -> cons(mark N, nats s N), a__zprimes() -> a__sieve a__nats s s 0(), a__zprimes() -> zprimes()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [filter](x0, x1, x2) = x0 + x1 + x2 + 1, [a__filter](x0, x1, x2) = x0 + x1 + x2 + 1, [cons](x0, x1) = x0, [mark](x0) = x0, [s](x0) = x0, [sieve](x0) = x0, [a__sieve](x0) = x0, [nats](x0) = x0, [a__nats](x0) = x0, [0] = 1, [a__zprimes] = 1, [zprimes] = 1, [a__filter#](x0, x1, x2) = x0 + x1 + x2 + 1, [mark#](x0) = x0, [a__sieve#](x0) = x0, [a__nats#](x0) = x0, [a__zprimes#] = 1 Strict: a__zprimes#() -> a__nats# s s 0() 1 >= 1 a__zprimes#() -> a__sieve# a__nats s s 0() 1 >= 1 a__nats# N -> mark# N 0 + 1N >= 0 + 1N a__sieve# cons(s N, Y) -> mark# N 0 + 0Y + 1N >= 0 + 1N mark# zprimes() -> a__zprimes#() 1 >= 1 mark# nats X -> a__nats# mark X 0 + 1X >= 0 + 1X mark# nats X -> mark# X 0 + 1X >= 0 + 1X mark# sieve X -> a__sieve# mark X 0 + 1X >= 0 + 1X mark# sieve X -> mark# X 0 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# filter(X1, X2, X3) -> mark# X3 1 + 1X1 + 1X2 + 1X3 >= 0 + 1X3 mark# filter(X1, X2, X3) -> mark# X2 1 + 1X1 + 1X2 + 1X3 >= 0 + 1X2 mark# filter(X1, X2, X3) -> mark# X1 1 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 mark# filter(X1, X2, X3) -> a__filter#(mark X1, mark X2, mark X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 0X2 >= 0 + 1X1 a__filter#(cons(X, Y), s N, M) -> mark# X 1 + 0Y + 1M + 1X + 1N >= 0 + 1X Weak: a__zprimes() -> zprimes() 1 >= 1 a__zprimes() -> a__sieve a__nats s s 0() 1 >= 1 a__nats N -> cons(mark N, nats s N) 0 + 1N >= 0 + 1N a__nats X -> nats X 0 + 1X >= 0 + 1X a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)) 0 + 0Y + 1N >= 0 + 0Y + 1N a__sieve cons(0(), Y) -> cons(0(), sieve Y) 1 + 0Y >= 1 + 0Y a__sieve X -> sieve X 0 + 1X >= 0 + 1X mark zprimes() -> a__zprimes() 1 >= 1 mark nats X -> a__nats mark X 0 + 1X >= 0 + 1X mark sieve X -> a__sieve mark X 0 + 1X >= 0 + 1X mark s X -> s mark X 0 + 1X >= 0 + 1X mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> 0() 1 >= 1 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)) 1 + 0Y + 1M + 1X + 1N >= 0 + 0Y + 0M + 1X + 0N a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 2 + 0Y + 1M + 1X >= 1 + 0Y + 0M a__filter(X1, X2, X3) -> filter(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# sieve X -> mark# X, mark# sieve X -> a__sieve# mark X, mark# nats X -> mark# X, mark# nats X -> a__nats# mark X, mark# zprimes() -> a__zprimes#(), a__sieve# cons(s N, Y) -> mark# N, a__nats# N -> mark# N, a__zprimes#() -> a__sieve# a__nats s s 0(), a__zprimes#() -> a__nats# s s 0()} SCC (11): Strict: { mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# sieve X -> mark# X, mark# sieve X -> a__sieve# mark X, mark# nats X -> mark# X, mark# nats X -> a__nats# mark X, mark# zprimes() -> a__zprimes#(), a__sieve# cons(s N, Y) -> mark# N, a__nats# N -> mark# N, a__zprimes#() -> a__sieve# a__nats s s 0(), a__zprimes#() -> a__nats# s s 0()} Weak: { a__filter(X1, X2, X3) -> filter(X1, X2, X3), a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3), mark s X -> s mark X, mark sieve X -> a__sieve mark X, mark nats X -> a__nats mark X, mark zprimes() -> a__zprimes(), a__sieve X -> sieve X, a__sieve cons(0(), Y) -> cons(0(), sieve Y), a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)), a__nats X -> nats X, a__nats N -> cons(mark N, nats s N), a__zprimes() -> a__sieve a__nats s s 0(), a__zprimes() -> zprimes()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [filter](x0, x1, x2) = x0, [a__filter](x0, x1, x2) = x0, [cons](x0, x1) = x0, [mark](x0) = x0, [s](x0) = x0, [sieve](x0) = x0 + 1, [a__sieve](x0) = x0 + 1, [nats](x0) = x0, [a__nats](x0) = x0, [0] = 0, [a__zprimes] = 1, [zprimes] = 1, [mark#](x0) = x0, [a__sieve#](x0) = x0 + 1, [a__nats#](x0) = x0, [a__zprimes#] = 1 Strict: a__zprimes#() -> a__nats# s s 0() 1 >= 0 a__zprimes#() -> a__sieve# a__nats s s 0() 1 >= 1 a__nats# N -> mark# N 0 + 1N >= 0 + 1N a__sieve# cons(s N, Y) -> mark# N 1 + 0Y + 1N >= 0 + 1N mark# zprimes() -> a__zprimes#() 1 >= 1 mark# nats X -> a__nats# mark X 0 + 1X >= 0 + 1X mark# nats X -> mark# X 0 + 1X >= 0 + 1X mark# sieve X -> a__sieve# mark X 1 + 1X >= 1 + 1X mark# sieve X -> mark# X 1 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 0X2 >= 0 + 1X1 Weak: a__zprimes() -> zprimes() 1 >= 1 a__zprimes() -> a__sieve a__nats s s 0() 1 >= 1 a__nats N -> cons(mark N, nats s N) 0 + 1N >= 0 + 1N a__nats X -> nats X 0 + 1X >= 0 + 1X a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)) 1 + 0Y + 1N >= 0 + 0Y + 1N a__sieve cons(0(), Y) -> cons(0(), sieve Y) 1 + 0Y >= 0 + 0Y a__sieve X -> sieve X 1 + 1X >= 1 + 1X mark zprimes() -> a__zprimes() 1 >= 1 mark nats X -> a__nats mark X 0 + 1X >= 0 + 1X mark sieve X -> a__sieve mark X 1 + 1X >= 1 + 1X mark s X -> s mark X 0 + 1X >= 0 + 1X mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark 0() -> 0() 0 >= 0 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)) 0 + 0Y + 0M + 1X + 0N >= 0 + 0Y + 0M + 1X + 0N a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 0 + 0Y + 0M + 1X >= 0 + 0Y + 0M a__filter(X1, X2, X3) -> filter(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 SCCS (1): Scc: {mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# nats X -> mark# X, mark# nats X -> a__nats# mark X, a__nats# N -> mark# N} SCC (5): Strict: {mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# nats X -> mark# X, mark# nats X -> a__nats# mark X, a__nats# N -> mark# N} Weak: { a__filter(X1, X2, X3) -> filter(X1, X2, X3), a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3), mark s X -> s mark X, mark sieve X -> a__sieve mark X, mark nats X -> a__nats mark X, mark zprimes() -> a__zprimes(), a__sieve X -> sieve X, a__sieve cons(0(), Y) -> cons(0(), sieve Y), a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)), a__nats X -> nats X, a__nats N -> cons(mark N, nats s N), a__zprimes() -> a__sieve a__nats s s 0(), a__zprimes() -> zprimes()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [filter](x0, x1, x2) = x0, [a__filter](x0, x1, x2) = x0, [cons](x0, x1) = x0, [mark](x0) = x0, [s](x0) = x0, [sieve](x0) = x0, [a__sieve](x0) = x0, [nats](x0) = x0 + 1, [a__nats](x0) = x0 + 1, [0] = 0, [a__zprimes] = 1, [zprimes] = 1, [mark#](x0) = x0, [a__nats#](x0) = x0 + 1 Strict: a__nats# N -> mark# N 1 + 1N >= 0 + 1N mark# nats X -> a__nats# mark X 1 + 1X >= 1 + 1X mark# nats X -> mark# X 1 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 0X2 >= 0 + 1X1 Weak: a__zprimes() -> zprimes() 1 >= 1 a__zprimes() -> a__sieve a__nats s s 0() 1 >= 1 a__nats N -> cons(mark N, nats s N) 1 + 1N >= 0 + 1N a__nats X -> nats X 1 + 1X >= 1 + 1X a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)) 0 + 0Y + 1N >= 0 + 0Y + 1N a__sieve cons(0(), Y) -> cons(0(), sieve Y) 0 + 0Y >= 0 + 0Y a__sieve X -> sieve X 0 + 1X >= 0 + 1X mark zprimes() -> a__zprimes() 1 >= 1 mark nats X -> a__nats mark X 1 + 1X >= 1 + 1X mark sieve X -> a__sieve mark X 0 + 1X >= 0 + 1X mark s X -> s mark X 0 + 1X >= 0 + 1X mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark 0() -> 0() 0 >= 0 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)) 0 + 0Y + 0M + 1X + 0N >= 0 + 0Y + 0M + 1X + 0N a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 0 + 0Y + 0M + 1X >= 0 + 0Y + 0M a__filter(X1, X2, X3) -> filter(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 SCCS (1): Scc: {mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X} SCC (2): Strict: {mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X} Weak: { a__filter(X1, X2, X3) -> filter(X1, X2, X3), a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3), mark s X -> s mark X, mark sieve X -> a__sieve mark X, mark nats X -> a__nats mark X, mark zprimes() -> a__zprimes(), a__sieve X -> sieve X, a__sieve cons(0(), Y) -> cons(0(), sieve Y), a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)), a__nats X -> nats X, a__nats N -> cons(mark N, nats s N), a__zprimes() -> a__sieve a__nats s s 0(), a__zprimes() -> zprimes()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [filter](x0, x1, x2) = x0, [a__filter](x0, x1, x2) = x0 + 1, [cons](x0, x1) = x0 + x1 + 1, [mark](x0) = 0, [s](x0) = x0, [sieve](x0) = x0, [a__sieve](x0) = 0, [nats](x0) = 0, [a__nats](x0) = 0, [0] = 0, [a__zprimes] = 0, [zprimes] = 0, [mark#](x0) = x0 Strict: mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 1 + 1X1 + 1X2 >= 0 + 1X1 Weak: a__zprimes() -> zprimes() 0 >= 0 a__zprimes() -> a__sieve a__nats s s 0() 0 >= 0 a__nats N -> cons(mark N, nats s N) 0 + 0N >= 1 + 0N a__nats X -> nats X 0 + 0X >= 0 + 0X a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)) 0 + 0Y + 0N >= 1 + 0Y + 1N a__sieve cons(0(), Y) -> cons(0(), sieve Y) 0 + 0Y >= 1 + 1Y a__sieve X -> sieve X 0 + 0X >= 0 + 1X mark zprimes() -> a__zprimes() 0 >= 0 mark nats X -> a__nats mark X 0 + 0X >= 0 + 0X mark sieve X -> a__sieve mark X 0 + 0X >= 0 + 0X mark s X -> s mark X 0 + 0X >= 0 + 0X mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark 0() -> 0() 0 >= 0 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)) 2 + 1Y + 0M + 1X + 0N >= 1 + 0Y + 0M + 0X + 1N a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 2 + 1Y + 0M + 1X >= 1 + 0Y + 1M a__filter(X1, X2, X3) -> filter(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 SCCS (1): Scc: {mark# s X -> mark# X} SCC (1): Strict: {mark# s X -> mark# X} Weak: { a__filter(X1, X2, X3) -> filter(X1, X2, X3), a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3), mark s X -> s mark X, mark sieve X -> a__sieve mark X, mark nats X -> a__nats mark X, mark zprimes() -> a__zprimes(), a__sieve X -> sieve X, a__sieve cons(0(), Y) -> cons(0(), sieve Y), a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)), a__nats X -> nats X, a__nats N -> cons(mark N, nats s N), a__zprimes() -> a__sieve a__nats s s 0(), a__zprimes() -> zprimes()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [filter](x0, x1, x2) = 1, [a__filter](x0, x1, x2) = x0 + 1, [cons](x0, x1) = 1, [mark](x0) = x0 + 1, [s](x0) = x0 + 1, [sieve](x0) = 1, [a__sieve](x0) = x0 + 1, [nats](x0) = x0 + 1, [a__nats](x0) = 0, [0] = 1, [a__zprimes] = 0, [zprimes] = 0, [mark#](x0) = x0 + 1 Strict: mark# s X -> mark# X 2 + 1X >= 1 + 1X Weak: a__zprimes() -> zprimes() 0 >= 0 a__zprimes() -> a__sieve a__nats s s 0() 0 >= 1 a__nats N -> cons(mark N, nats s N) 0 + 0N >= 1 + 0N a__nats X -> nats X 0 + 0X >= 1 + 1X a__sieve cons(s N, Y) -> cons(s mark N, sieve filter(Y, N, N)) 2 + 0Y + 0N >= 1 + 0Y + 0N a__sieve cons(0(), Y) -> cons(0(), sieve Y) 2 + 0Y >= 1 + 0Y a__sieve X -> sieve X 1 + 1X >= 1 + 0X mark zprimes() -> a__zprimes() 1 >= 0 mark nats X -> a__nats mark X 2 + 1X >= 0 + 0X mark sieve X -> a__sieve mark X 2 + 0X >= 2 + 1X mark s X -> s mark X 2 + 1X >= 2 + 1X mark filter(X1, X2, X3) -> a__filter(mark X1, mark X2, mark X3) 2 + 0X1 + 0X2 + 0X3 >= 2 + 1X1 + 0X2 + 0X3 mark 0() -> 0() 2 >= 1 mark cons(X1, X2) -> cons(mark X1, X2) 2 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 a__filter(cons(X, Y), s N, M) -> cons(mark X, filter(Y, N, M)) 2 + 0Y + 0M + 0X + 0N >= 1 + 0Y + 0M + 0X + 0N a__filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 2 + 0Y + 0M + 0X >= 1 + 0Y + 0M a__filter(X1, X2, X3) -> filter(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 Qed