YES Time: 7.879089 TRS: { activate X -> X, activate n__filter(X1, X2, X3) -> filter(X1, X2, X3), activate n__sieve X -> sieve X, activate n__nats X -> nats X, filter(X1, X2, X3) -> n__filter(X1, X2, X3), filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, n__filter(activate Y, N, M)), sieve X -> n__sieve X, sieve cons(0(), Y) -> cons(0(), n__sieve activate Y), sieve cons(s N, Y) -> cons(s N, n__sieve filter(activate Y, N, N)), nats X -> n__nats X, nats N -> cons(N, n__nats s N), zprimes() -> sieve nats s s 0()} DP: DP: {activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3), activate# n__sieve X -> sieve# X, activate# n__nats X -> nats# X, filter#(cons(X, Y), 0(), M) -> activate# Y, filter#(cons(X, Y), s N, M) -> activate# Y, sieve# cons(0(), Y) -> activate# Y, sieve# cons(s N, Y) -> activate# Y, sieve# cons(s N, Y) -> filter#(activate Y, N, N), zprimes#() -> sieve# nats s s 0(), zprimes#() -> nats# s s 0()} TRS: { activate X -> X, activate n__filter(X1, X2, X3) -> filter(X1, X2, X3), activate n__sieve X -> sieve X, activate n__nats X -> nats X, filter(X1, X2, X3) -> n__filter(X1, X2, X3), filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, n__filter(activate Y, N, M)), sieve X -> n__sieve X, sieve cons(0(), Y) -> cons(0(), n__sieve activate Y), sieve cons(s N, Y) -> cons(s N, n__sieve filter(activate Y, N, N)), nats X -> n__nats X, nats N -> cons(N, n__nats s N), zprimes() -> sieve nats s s 0()} UR: { activate X -> X, activate n__filter(X1, X2, X3) -> filter(X1, X2, X3), activate n__sieve X -> sieve X, activate n__nats X -> nats X, filter(X1, X2, X3) -> n__filter(X1, X2, X3), filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, n__filter(activate Y, N, M)), sieve X -> n__sieve X, sieve cons(0(), Y) -> cons(0(), n__sieve activate Y), sieve cons(s N, Y) -> cons(s N, n__sieve filter(activate Y, N, N)), nats X -> n__nats X, nats N -> cons(N, n__nats s N), a(x, y) -> x, a(x, y) -> y} EDG: {(activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3), filter#(cons(X, Y), s N, M) -> activate# Y) (activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3), filter#(cons(X, Y), 0(), M) -> activate# Y) (filter#(cons(X, Y), s N, M) -> activate# Y, activate# n__nats X -> nats# X) (filter#(cons(X, Y), s N, M) -> activate# Y, activate# n__sieve X -> sieve# X) (filter#(cons(X, Y), s N, M) -> activate# Y, activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3)) (sieve# cons(s N, Y) -> activate# Y, activate# n__nats X -> nats# X) (sieve# cons(s N, Y) -> activate# Y, activate# n__sieve X -> sieve# X) (sieve# cons(s N, Y) -> activate# Y, activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3)) (sieve# cons(0(), Y) -> activate# Y, activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3)) (sieve# cons(0(), Y) -> activate# Y, activate# n__sieve X -> sieve# X) (sieve# cons(0(), Y) -> activate# Y, activate# n__nats X -> nats# X) (filter#(cons(X, Y), 0(), M) -> activate# Y, activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3)) (filter#(cons(X, Y), 0(), M) -> activate# Y, activate# n__sieve X -> sieve# X) (filter#(cons(X, Y), 0(), M) -> activate# Y, activate# n__nats X -> nats# X) (sieve# cons(s N, Y) -> filter#(activate Y, N, N), filter#(cons(X, Y), 0(), M) -> activate# Y) (sieve# cons(s N, Y) -> filter#(activate Y, N, N), filter#(cons(X, Y), s N, M) -> activate# Y) (zprimes#() -> sieve# nats s s 0(), sieve# cons(0(), Y) -> activate# Y) (zprimes#() -> sieve# nats s s 0(), sieve# cons(s N, Y) -> activate# Y) (zprimes#() -> sieve# nats s s 0(), sieve# cons(s N, Y) -> filter#(activate Y, N, N)) (activate# n__sieve X -> sieve# X, sieve# cons(0(), Y) -> activate# Y) (activate# n__sieve X -> sieve# X, sieve# cons(s N, Y) -> activate# Y) (activate# n__sieve X -> sieve# X, sieve# cons(s N, Y) -> filter#(activate Y, N, N))} STATUS: arrows: 0.780000 SCCS (1): Scc: {activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3), activate# n__sieve X -> sieve# X, filter#(cons(X, Y), 0(), M) -> activate# Y, filter#(cons(X, Y), s N, M) -> activate# Y, sieve# cons(0(), Y) -> activate# Y, sieve# cons(s N, Y) -> activate# Y, sieve# cons(s N, Y) -> filter#(activate Y, N, N)} SCC (7): Strict: {activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3), activate# n__sieve X -> sieve# X, filter#(cons(X, Y), 0(), M) -> activate# Y, filter#(cons(X, Y), s N, M) -> activate# Y, sieve# cons(0(), Y) -> activate# Y, sieve# cons(s N, Y) -> activate# Y, sieve# cons(s N, Y) -> filter#(activate Y, N, N)} Weak: { activate X -> X, activate n__filter(X1, X2, X3) -> filter(X1, X2, X3), activate n__sieve X -> sieve X, activate n__nats X -> nats X, filter(X1, X2, X3) -> n__filter(X1, X2, X3), filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, n__filter(activate Y, N, M)), sieve X -> n__sieve X, sieve cons(0(), Y) -> cons(0(), n__sieve activate Y), sieve cons(s N, Y) -> cons(s N, n__sieve filter(activate Y, N, N)), nats X -> n__nats X, nats N -> cons(N, n__nats s N), zprimes() -> sieve nats s s 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [n__filter](x0, x1, x2) = x0, [filter](x0, x1, x2) = x0, [cons](x0, x1) = x0, [activate](x0) = x0, [s](x0) = 0, [n__sieve](x0) = x0 + 1, [sieve](x0) = x0 + 1, [n__nats](x0) = 0, [nats](x0) = 0, [0] = 0, [zprimes] = 0, [filter#](x0, x1, x2) = x0, [activate#](x0) = x0, [sieve#](x0) = x0 + 1 Strict: sieve# cons(s N, Y) -> filter#(activate Y, N, N) 1 + 1Y + 0N >= 0 + 1Y + 0N sieve# cons(s N, Y) -> activate# Y 1 + 1Y + 0N >= 0 + 1Y sieve# cons(0(), Y) -> activate# Y 1 + 1Y >= 0 + 1Y filter#(cons(X, Y), s N, M) -> activate# Y 0 + 1Y + 0M + 0X + 0N >= 0 + 1Y filter#(cons(X, Y), 0(), M) -> activate# Y 0 + 1Y + 0M + 0X >= 0 + 1Y activate# n__sieve X -> sieve# X 1 + 1X >= 1 + 1X activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: zprimes() -> sieve nats s s 0() 0 >= 1 nats N -> cons(N, n__nats s N) 0 + 0N >= 0 + 0N nats X -> n__nats X 0 + 0X >= 0 + 0X sieve cons(s N, Y) -> cons(s N, n__sieve filter(activate Y, N, N)) 1 + 1Y + 0N >= 1 + 1Y + 0N sieve cons(0(), Y) -> cons(0(), n__sieve activate Y) 1 + 1Y >= 1 + 1Y sieve X -> n__sieve X 1 + 1X >= 1 + 1X filter(cons(X, Y), s N, M) -> cons(X, n__filter(activate Y, N, M)) 0 + 1Y + 0M + 0X + 0N >= 0 + 1Y + 0M + 0X + 0N filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate Y, M, M)) 0 + 1Y + 0M + 0X >= 0 + 1Y + 0M filter(X1, X2, X3) -> n__filter(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 activate n__nats X -> nats X 0 + 0X >= 0 + 0X activate n__sieve X -> sieve X 1 + 1X >= 1 + 1X activate n__filter(X1, X2, X3) -> filter(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 activate X -> X 0 + 1X >= 1X SCCS (1): Scc: {activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3), filter#(cons(X, Y), 0(), M) -> activate# Y, filter#(cons(X, Y), s N, M) -> activate# Y} SCC (3): Strict: {activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3), filter#(cons(X, Y), 0(), M) -> activate# Y, filter#(cons(X, Y), s N, M) -> activate# Y} Weak: { activate X -> X, activate n__filter(X1, X2, X3) -> filter(X1, X2, X3), activate n__sieve X -> sieve X, activate n__nats X -> nats X, filter(X1, X2, X3) -> n__filter(X1, X2, X3), filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate Y, M, M)), filter(cons(X, Y), s N, M) -> cons(X, n__filter(activate Y, N, M)), sieve X -> n__sieve X, sieve cons(0(), Y) -> cons(0(), n__sieve activate Y), sieve cons(s N, Y) -> cons(s N, n__sieve filter(activate Y, N, N)), nats X -> n__nats X, nats N -> cons(N, n__nats s N), zprimes() -> sieve nats s s 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [n__filter](x0, x1, x2) = x0 + x1 + 1, [filter](x0, x1, x2) = 0, [cons](x0, x1) = x0 + x1 + 1, [activate](x0) = x0 + 1, [s](x0) = 0, [n__sieve](x0) = x0 + 1, [sieve](x0) = 0, [n__nats](x0) = 1, [nats](x0) = 0, [0] = 1, [zprimes] = 0, [filter#](x0, x1, x2) = x0 + x1, [activate#](x0) = x0 Strict: filter#(cons(X, Y), s N, M) -> activate# Y 1 + 1Y + 0M + 1X + 0N >= 0 + 1Y filter#(cons(X, Y), 0(), M) -> activate# Y 2 + 1Y + 0M + 1X >= 0 + 1Y activate# n__filter(X1, X2, X3) -> filter#(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 0 + 1X1 + 1X2 + 0X3 Weak: zprimes() -> sieve nats s s 0() 0 >= 0 nats N -> cons(N, n__nats s N) 0 + 0N >= 2 + 1N nats X -> n__nats X 0 + 0X >= 1 + 0X sieve cons(s N, Y) -> cons(s N, n__sieve filter(activate Y, N, N)) 0 + 0Y + 0N >= 2 + 0Y + 0N sieve cons(0(), Y) -> cons(0(), n__sieve activate Y) 0 + 0Y >= 4 + 1Y sieve X -> n__sieve X 0 + 0X >= 1 + 1X filter(cons(X, Y), s N, M) -> cons(X, n__filter(activate Y, N, M)) 0 + 0Y + 0M + 0X + 0N >= 3 + 1Y + 0M + 1X + 1N filter(cons(X, Y), 0(), M) -> cons(0(), n__filter(activate Y, M, M)) 0 + 0Y + 0M + 0X >= 4 + 1Y + 1M filter(X1, X2, X3) -> n__filter(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 activate n__nats X -> nats X 2 + 0X >= 0 + 0X activate n__sieve X -> sieve X 2 + 1X >= 0 + 0X activate n__filter(X1, X2, X3) -> filter(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 activate X -> X 1 + 1X >= 1X Qed