MAYBE Time: 0.082548 TRS: {filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, filter(Y, N, M)), sieve cons(0(), Y) -> cons(0(), sieve Y), sieve cons(s N, Y) -> cons(s N, sieve filter(Y, N, N)), nats N -> cons(N, nats s N), zprimes() -> sieve nats s s 0()} DP: DP: {filter#(cons(X, Y), 0(), M) -> filter#(Y, M, M), filter#(cons(X, Y), s N, M) -> filter#(Y, N, M), sieve# cons(0(), Y) -> sieve# Y, sieve# cons(s N, Y) -> filter#(Y, N, N), sieve# cons(s N, Y) -> sieve# filter(Y, N, N), nats# N -> nats# s N, zprimes#() -> sieve# nats s s 0(), zprimes#() -> nats# s s 0()} TRS: {filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, filter(Y, N, M)), sieve cons(0(), Y) -> cons(0(), sieve Y), sieve cons(s N, Y) -> cons(s N, sieve filter(Y, N, N)), nats N -> cons(N, nats s N), zprimes() -> sieve nats s s 0()} UR: {filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, filter(Y, N, M)), nats N -> cons(N, nats s N), a(x, y) -> x, a(x, y) -> y} EDG: {(filter#(cons(X, Y), s N, M) -> filter#(Y, N, M), filter#(cons(X, Y), s N, M) -> filter#(Y, N, M)) (filter#(cons(X, Y), s N, M) -> filter#(Y, N, M), filter#(cons(X, Y), 0(), M) -> filter#(Y, M, M)) (nats# N -> nats# s N, nats# N -> nats# s N) (sieve# cons(s N, Y) -> filter#(Y, N, N), filter#(cons(X, Y), s N, M) -> filter#(Y, N, M)) (sieve# cons(s N, Y) -> filter#(Y, N, N), filter#(cons(X, Y), 0(), M) -> filter#(Y, M, M)) (zprimes#() -> nats# s s 0(), nats# N -> nats# s N) (zprimes#() -> sieve# nats s s 0(), sieve# cons(0(), Y) -> sieve# Y) (zprimes#() -> sieve# nats s s 0(), sieve# cons(s N, Y) -> filter#(Y, N, N)) (zprimes#() -> sieve# nats s s 0(), sieve# cons(s N, Y) -> sieve# filter(Y, N, N)) (sieve# cons(s N, Y) -> sieve# filter(Y, N, N), sieve# cons(0(), Y) -> sieve# Y) (sieve# cons(s N, Y) -> sieve# filter(Y, N, N), sieve# cons(s N, Y) -> filter#(Y, N, N)) (sieve# cons(s N, Y) -> sieve# filter(Y, N, N), sieve# cons(s N, Y) -> sieve# filter(Y, N, N)) (sieve# cons(0(), Y) -> sieve# Y, sieve# cons(0(), Y) -> sieve# Y) (sieve# cons(0(), Y) -> sieve# Y, sieve# cons(s N, Y) -> filter#(Y, N, N)) (sieve# cons(0(), Y) -> sieve# Y, sieve# cons(s N, Y) -> sieve# filter(Y, N, N)) (filter#(cons(X, Y), 0(), M) -> filter#(Y, M, M), filter#(cons(X, Y), 0(), M) -> filter#(Y, M, M)) (filter#(cons(X, Y), 0(), M) -> filter#(Y, M, M), filter#(cons(X, Y), s N, M) -> filter#(Y, N, M))} STATUS: arrows: 0.734375 SCCS (3): Scc: {nats# N -> nats# s N} Scc: {sieve# cons(0(), Y) -> sieve# Y, sieve# cons(s N, Y) -> sieve# filter(Y, N, N)} Scc: {filter#(cons(X, Y), 0(), M) -> filter#(Y, M, M), filter#(cons(X, Y), s N, M) -> filter#(Y, N, M)} SCC (1): Strict: {nats# N -> nats# s N} Weak: {filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, filter(Y, N, M)), sieve cons(0(), Y) -> cons(0(), sieve Y), sieve cons(s N, Y) -> cons(s N, sieve filter(Y, N, N)), nats N -> cons(N, nats s N), zprimes() -> sieve nats s s 0()} Fail SCC (2): Strict: {sieve# cons(0(), Y) -> sieve# Y, sieve# cons(s N, Y) -> sieve# filter(Y, N, N)} Weak: {filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, filter(Y, N, M)), sieve cons(0(), Y) -> cons(0(), sieve Y), sieve cons(s N, Y) -> cons(s N, sieve filter(Y, N, N)), nats N -> cons(N, nats s N), zprimes() -> sieve nats s s 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [filter](x0, x1, x2) = x0, [cons](x0, x1) = x0 + 1, [s](x0) = 0, [sieve](x0) = 0, [nats](x0) = 0, [0] = 0, [zprimes] = 0, [sieve#](x0) = x0 Strict: sieve# cons(s N, Y) -> sieve# filter(Y, N, N) 1 + 1Y + 0N >= 0 + 1Y + 0N sieve# cons(0(), Y) -> sieve# Y 1 + 1Y >= 0 + 1Y Weak: zprimes() -> sieve nats s s 0() 0 >= 0 nats N -> cons(N, nats s N) 0 + 0N >= 1 + 0N sieve cons(s N, Y) -> cons(s N, sieve filter(Y, N, N)) 0 + 0Y + 0N >= 1 + 0Y + 0N sieve cons(0(), Y) -> cons(0(), sieve Y) 0 + 0Y >= 1 + 0Y filter(cons(X, Y), s N, M) -> cons(X, filter(Y, N, M)) 1 + 1Y + 0M + 0X + 0N >= 1 + 1Y + 0M + 0X + 0N filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 1 + 1Y + 0M + 0X >= 1 + 1Y + 0M Qed SCC (2): Strict: {filter#(cons(X, Y), 0(), M) -> filter#(Y, M, M), filter#(cons(X, Y), s N, M) -> filter#(Y, N, M)} Weak: {filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, filter(Y, N, M)), sieve cons(0(), Y) -> cons(0(), sieve Y), sieve cons(s N, Y) -> cons(s N, sieve filter(Y, N, N)), nats N -> cons(N, nats s N), zprimes() -> sieve nats s s 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [filter](x0, x1, x2) = 0, [cons](x0, x1) = x0 + 1, [s](x0) = 0, [sieve](x0) = 0, [nats](x0) = 0, [0] = 0, [zprimes] = 0, [filter#](x0, x1, x2) = x0 + 1 Strict: filter#(cons(X, Y), s N, M) -> filter#(Y, N, M) 2 + 1Y + 0M + 0X + 0N >= 1 + 1Y + 0M + 0N filter#(cons(X, Y), 0(), M) -> filter#(Y, M, M) 2 + 1Y + 0M + 0X >= 1 + 1Y + 0M Weak: zprimes() -> sieve nats s s 0() 0 >= 0 nats N -> cons(N, nats s N) 0 + 0N >= 1 + 0N sieve cons(s N, Y) -> cons(s N, sieve filter(Y, N, N)) 0 + 0Y + 0N >= 1 + 0Y + 0N sieve cons(0(), Y) -> cons(0(), sieve Y) 0 + 0Y >= 1 + 0Y filter(cons(X, Y), s N, M) -> cons(X, filter(Y, N, M)) 0 + 0Y + 0M + 0X + 0N >= 1 + 0Y + 0M + 0X + 0N filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M)) 0 + 0Y + 0M + 0X >= 1 + 0Y + 0M Qed