YES

We show the termination of the TRS R:

  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|())))))
  mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
  mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
  mark(|0|()) -> active(|0|())
  mark(s(X)) -> active(s(mark(X)))
  mark(sieve(X)) -> active(sieve(mark(X)))
  mark(nats(X)) -> active(nats(mark(X)))
  mark(zprimes()) -> active(zprimes())
  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)
  filter(active(X1),X2,X3) -> filter(X1,X2,X3)
  filter(X1,active(X2),X3) -> filter(X1,X2,X3)
  filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
  cons(mark(X1),X2) -> cons(X1,X2)
  cons(X1,mark(X2)) -> cons(X1,X2)
  cons(active(X1),X2) -> cons(X1,X2)
  cons(X1,active(X2)) -> cons(X1,X2)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(X)
  sieve(mark(X)) -> sieve(X)
  sieve(active(X)) -> sieve(X)
  nats(mark(X)) -> nats(X)
  nats(active(X)) -> nats(X)

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(filter(cons(X,Y),|0|(),M)) -> mark#(cons(|0|(),filter(Y,M,M)))
p2: active#(filter(cons(X,Y),|0|(),M)) -> cons#(|0|(),filter(Y,M,M))
p3: active#(filter(cons(X,Y),|0|(),M)) -> filter#(Y,M,M)
p4: active#(filter(cons(X,Y),s(N),M)) -> mark#(cons(X,filter(Y,N,M)))
p5: active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
p6: active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
p7: active#(sieve(cons(|0|(),Y))) -> mark#(cons(|0|(),sieve(Y)))
p8: active#(sieve(cons(|0|(),Y))) -> cons#(|0|(),sieve(Y))
p9: active#(sieve(cons(|0|(),Y))) -> sieve#(Y)
p10: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p11: active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
p12: active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
p13: active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
p14: active#(nats(N)) -> mark#(cons(N,nats(s(N))))
p15: active#(nats(N)) -> cons#(N,nats(s(N)))
p16: active#(nats(N)) -> nats#(s(N))
p17: active#(nats(N)) -> s#(N)
p18: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p19: active#(zprimes()) -> sieve#(nats(s(s(|0|()))))
p20: active#(zprimes()) -> nats#(s(s(|0|())))
p21: active#(zprimes()) -> s#(s(|0|()))
p22: active#(zprimes()) -> s#(|0|())
p23: mark#(filter(X1,X2,X3)) -> active#(filter(mark(X1),mark(X2),mark(X3)))
p24: mark#(filter(X1,X2,X3)) -> filter#(mark(X1),mark(X2),mark(X3))
p25: mark#(filter(X1,X2,X3)) -> mark#(X1)
p26: mark#(filter(X1,X2,X3)) -> mark#(X2)
p27: mark#(filter(X1,X2,X3)) -> mark#(X3)
p28: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p29: mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
p30: mark#(cons(X1,X2)) -> mark#(X1)
p31: mark#(|0|()) -> active#(|0|())
p32: mark#(s(X)) -> active#(s(mark(X)))
p33: mark#(s(X)) -> s#(mark(X))
p34: mark#(s(X)) -> mark#(X)
p35: mark#(sieve(X)) -> active#(sieve(mark(X)))
p36: mark#(sieve(X)) -> sieve#(mark(X))
p37: mark#(sieve(X)) -> mark#(X)
p38: mark#(nats(X)) -> active#(nats(mark(X)))
p39: mark#(nats(X)) -> nats#(mark(X))
p40: mark#(nats(X)) -> mark#(X)
p41: mark#(zprimes()) -> active#(zprimes())
p42: filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
p43: filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
p44: filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
p45: filter#(active(X1),X2,X3) -> filter#(X1,X2,X3)
p46: filter#(X1,active(X2),X3) -> filter#(X1,X2,X3)
p47: filter#(X1,X2,active(X3)) -> filter#(X1,X2,X3)
p48: cons#(mark(X1),X2) -> cons#(X1,X2)
p49: cons#(X1,mark(X2)) -> cons#(X1,X2)
p50: cons#(active(X1),X2) -> cons#(X1,X2)
p51: cons#(X1,active(X2)) -> cons#(X1,X2)
p52: s#(mark(X)) -> s#(X)
p53: s#(active(X)) -> s#(X)
p54: sieve#(mark(X)) -> sieve#(X)
p55: sieve#(active(X)) -> sieve#(X)
p56: nats#(mark(X)) -> nats#(X)
p57: nats#(active(X)) -> nats#(X)

and R consists of:

r1: active(filter(cons(X,Y),|0|(),M)) -> mark(cons(|0|(),filter(Y,M,M)))
r2: active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
r3: active(sieve(cons(|0|(),Y))) -> mark(cons(|0|(),sieve(Y)))
r4: active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
r5: active(nats(N)) -> mark(cons(N,nats(s(N))))
r6: active(zprimes()) -> mark(sieve(nats(s(s(|0|())))))
r7: mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
r8: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r9: mark(|0|()) -> active(|0|())
r10: mark(s(X)) -> active(s(mark(X)))
r11: mark(sieve(X)) -> active(sieve(mark(X)))
r12: mark(nats(X)) -> active(nats(mark(X)))
r13: mark(zprimes()) -> active(zprimes())
r14: filter(mark(X1),X2,X3) -> filter(X1,X2,X3)
r15: filter(X1,mark(X2),X3) -> filter(X1,X2,X3)
r16: filter(X1,X2,mark(X3)) -> filter(X1,X2,X3)
r17: filter(active(X1),X2,X3) -> filter(X1,X2,X3)
r18: filter(X1,active(X2),X3) -> filter(X1,X2,X3)
r19: filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
r20: cons(mark(X1),X2) -> cons(X1,X2)
r21: cons(X1,mark(X2)) -> cons(X1,X2)
r22: cons(active(X1),X2) -> cons(X1,X2)
r23: cons(X1,active(X2)) -> cons(X1,X2)
r24: s(mark(X)) -> s(X)
r25: s(active(X)) -> s(X)
r26: sieve(mark(X)) -> sieve(X)
r27: sieve(active(X)) -> sieve(X)
r28: nats(mark(X)) -> nats(X)
r29: nats(active(X)) -> nats(X)

The estimated dependency graph contains the following SCCs:

  {p1, p4, p7, p10, p14, p18, p23, p25, p26, p27, p28, p30, p32, p34, p35, p37, p38, p40, p41}
  {p48, p49, p50, p51}
  {p42, p43, p44, p45, p46, p47}
  {p54, p55}
  {p56, p57}
  {p52, p53}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(filter(cons(X,Y),|0|(),M)) -> mark#(cons(|0|(),filter(Y,M,M)))
p2: mark#(zprimes()) -> active#(zprimes())
p3: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p4: mark#(sieve(X)) -> mark#(X)
p5: mark#(nats(X)) -> mark#(X)
p6: mark#(nats(X)) -> active#(nats(mark(X)))
p7: active#(nats(N)) -> mark#(cons(N,nats(s(N))))
p8: mark#(sieve(X)) -> active#(sieve(mark(X)))
p9: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p10: mark#(s(X)) -> mark#(X)
p11: mark#(s(X)) -> active#(s(mark(X)))
p12: active#(sieve(cons(|0|(),Y))) -> mark#(cons(|0|(),sieve(Y)))
p13: mark#(cons(X1,X2)) -> mark#(X1)
p14: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p15: active#(filter(cons(X,Y),s(N),M)) -> mark#(cons(X,filter(Y,N,M)))
p16: mark#(filter(X1,X2,X3)) -> mark#(X3)
p17: mark#(filter(X1,X2,X3)) -> mark#(X2)
p18: mark#(filter(X1,X2,X3)) -> mark#(X1)
p19: mark#(filter(X1,X2,X3)) -> active#(filter(mark(X1),mark(X2),mark(X3)))

and R consists of:

r1: active(filter(cons(X,Y),|0|(),M)) -> mark(cons(|0|(),filter(Y,M,M)))
r2: active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
r3: active(sieve(cons(|0|(),Y))) -> mark(cons(|0|(),sieve(Y)))
r4: active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
r5: active(nats(N)) -> mark(cons(N,nats(s(N))))
r6: active(zprimes()) -> mark(sieve(nats(s(s(|0|())))))
r7: mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
r8: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r9: mark(|0|()) -> active(|0|())
r10: mark(s(X)) -> active(s(mark(X)))
r11: mark(sieve(X)) -> active(sieve(mark(X)))
r12: mark(nats(X)) -> active(nats(mark(X)))
r13: mark(zprimes()) -> active(zprimes())
r14: filter(mark(X1),X2,X3) -> filter(X1,X2,X3)
r15: filter(X1,mark(X2),X3) -> filter(X1,X2,X3)
r16: filter(X1,X2,mark(X3)) -> filter(X1,X2,X3)
r17: filter(active(X1),X2,X3) -> filter(X1,X2,X3)
r18: filter(X1,active(X2),X3) -> filter(X1,X2,X3)
r19: filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
r20: cons(mark(X1),X2) -> cons(X1,X2)
r21: cons(X1,mark(X2)) -> cons(X1,X2)
r22: cons(active(X1),X2) -> cons(X1,X2)
r23: cons(X1,active(X2)) -> cons(X1,X2)
r24: s(mark(X)) -> s(X)
r25: s(active(X)) -> s(X)
r26: sieve(mark(X)) -> sieve(X)
r27: sieve(active(X)) -> sieve(X)
r28: nats(mark(X)) -> nats(X)
r29: nats(active(X)) -> nats(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      active#_A(x1) = ((0,0),(1,0)) x1
      filter_A(x1,x2,x3) = (2,1)
      cons_A(x1,x2) = (1,1)
      |0|_A() = (1,0)
      mark#_A(x1) = (0,2)
      zprimes_A() = (2,0)
      sieve_A(x1) = (2,1)
      nats_A(x1) = (2,1)
      s_A(x1) = (1,1)
      mark_A(x1) = ((0,0),(1,0)) x1 + (3,1)
      active_A(x1) = ((1,0),(1,0)) x1 + (1,1)

The next rules are strictly ordered:

  p11, p14

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(filter(cons(X,Y),|0|(),M)) -> mark#(cons(|0|(),filter(Y,M,M)))
p2: mark#(zprimes()) -> active#(zprimes())
p3: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p4: mark#(sieve(X)) -> mark#(X)
p5: mark#(nats(X)) -> mark#(X)
p6: mark#(nats(X)) -> active#(nats(mark(X)))
p7: active#(nats(N)) -> mark#(cons(N,nats(s(N))))
p8: mark#(sieve(X)) -> active#(sieve(mark(X)))
p9: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p10: mark#(s(X)) -> mark#(X)
p11: active#(sieve(cons(|0|(),Y))) -> mark#(cons(|0|(),sieve(Y)))
p12: mark#(cons(X1,X2)) -> mark#(X1)
p13: active#(filter(cons(X,Y),s(N),M)) -> mark#(cons(X,filter(Y,N,M)))
p14: mark#(filter(X1,X2,X3)) -> mark#(X3)
p15: mark#(filter(X1,X2,X3)) -> mark#(X2)
p16: mark#(filter(X1,X2,X3)) -> mark#(X1)
p17: mark#(filter(X1,X2,X3)) -> active#(filter(mark(X1),mark(X2),mark(X3)))

and R consists of:

r1: active(filter(cons(X,Y),|0|(),M)) -> mark(cons(|0|(),filter(Y,M,M)))
r2: active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
r3: active(sieve(cons(|0|(),Y))) -> mark(cons(|0|(),sieve(Y)))
r4: active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
r5: active(nats(N)) -> mark(cons(N,nats(s(N))))
r6: active(zprimes()) -> mark(sieve(nats(s(s(|0|())))))
r7: mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
r8: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r9: mark(|0|()) -> active(|0|())
r10: mark(s(X)) -> active(s(mark(X)))
r11: mark(sieve(X)) -> active(sieve(mark(X)))
r12: mark(nats(X)) -> active(nats(mark(X)))
r13: mark(zprimes()) -> active(zprimes())
r14: filter(mark(X1),X2,X3) -> filter(X1,X2,X3)
r15: filter(X1,mark(X2),X3) -> filter(X1,X2,X3)
r16: filter(X1,X2,mark(X3)) -> filter(X1,X2,X3)
r17: filter(active(X1),X2,X3) -> filter(X1,X2,X3)
r18: filter(X1,active(X2),X3) -> filter(X1,X2,X3)
r19: filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
r20: cons(mark(X1),X2) -> cons(X1,X2)
r21: cons(X1,mark(X2)) -> cons(X1,X2)
r22: cons(active(X1),X2) -> cons(X1,X2)
r23: cons(X1,active(X2)) -> cons(X1,X2)
r24: s(mark(X)) -> s(X)
r25: s(active(X)) -> s(X)
r26: sieve(mark(X)) -> sieve(X)
r27: sieve(active(X)) -> sieve(X)
r28: nats(mark(X)) -> nats(X)
r29: nats(active(X)) -> nats(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(filter(cons(X,Y),|0|(),M)) -> mark#(cons(|0|(),filter(Y,M,M)))
p2: mark#(filter(X1,X2,X3)) -> active#(filter(mark(X1),mark(X2),mark(X3)))
p3: active#(filter(cons(X,Y),s(N),M)) -> mark#(cons(X,filter(Y,N,M)))
p4: mark#(filter(X1,X2,X3)) -> mark#(X1)
p5: mark#(filter(X1,X2,X3)) -> mark#(X2)
p6: mark#(filter(X1,X2,X3)) -> mark#(X3)
p7: mark#(cons(X1,X2)) -> mark#(X1)
p8: mark#(s(X)) -> mark#(X)
p9: mark#(sieve(X)) -> active#(sieve(mark(X)))
p10: active#(sieve(cons(|0|(),Y))) -> mark#(cons(|0|(),sieve(Y)))
p11: mark#(nats(X)) -> active#(nats(mark(X)))
p12: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p13: mark#(nats(X)) -> mark#(X)
p14: mark#(sieve(X)) -> mark#(X)
p15: mark#(zprimes()) -> active#(zprimes())
p16: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p17: active#(nats(N)) -> mark#(cons(N,nats(s(N))))

and R consists of:

r1: active(filter(cons(X,Y),|0|(),M)) -> mark(cons(|0|(),filter(Y,M,M)))
r2: active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
r3: active(sieve(cons(|0|(),Y))) -> mark(cons(|0|(),sieve(Y)))
r4: active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
r5: active(nats(N)) -> mark(cons(N,nats(s(N))))
r6: active(zprimes()) -> mark(sieve(nats(s(s(|0|())))))
r7: mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
r8: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r9: mark(|0|()) -> active(|0|())
r10: mark(s(X)) -> active(s(mark(X)))
r11: mark(sieve(X)) -> active(sieve(mark(X)))
r12: mark(nats(X)) -> active(nats(mark(X)))
r13: mark(zprimes()) -> active(zprimes())
r14: filter(mark(X1),X2,X3) -> filter(X1,X2,X3)
r15: filter(X1,mark(X2),X3) -> filter(X1,X2,X3)
r16: filter(X1,X2,mark(X3)) -> filter(X1,X2,X3)
r17: filter(active(X1),X2,X3) -> filter(X1,X2,X3)
r18: filter(X1,active(X2),X3) -> filter(X1,X2,X3)
r19: filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
r20: cons(mark(X1),X2) -> cons(X1,X2)
r21: cons(X1,mark(X2)) -> cons(X1,X2)
r22: cons(active(X1),X2) -> cons(X1,X2)
r23: cons(X1,active(X2)) -> cons(X1,X2)
r24: s(mark(X)) -> s(X)
r25: s(active(X)) -> s(X)
r26: sieve(mark(X)) -> sieve(X)
r27: sieve(active(X)) -> sieve(X)
r28: nats(mark(X)) -> nats(X)
r29: nats(active(X)) -> nats(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      active#_A(x1) = x1
      filter_A(x1,x2,x3) = x1 + ((1,0),(1,0)) x2 + x3 + (1,0)
      cons_A(x1,x2) = x1 + (1,1)
      |0|_A() = (4,1)
      mark#_A(x1) = x1 + (0,2)
      mark_A(x1) = x1 + (0,1)
      s_A(x1) = x1 + (0,1)
      sieve_A(x1) = x1 + (1,4)
      nats_A(x1) = x1 + (2,0)
      zprimes_A() = (8,0)
      active_A(x1) = x1

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: cons#(X1,mark(X2)) -> cons#(X1,X2)
p2: cons#(X1,active(X2)) -> cons#(X1,X2)
p3: cons#(active(X1),X2) -> cons#(X1,X2)
p4: cons#(mark(X1),X2) -> cons#(X1,X2)

and R consists of:

r1: active(filter(cons(X,Y),|0|(),M)) -> mark(cons(|0|(),filter(Y,M,M)))
r2: active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
r3: active(sieve(cons(|0|(),Y))) -> mark(cons(|0|(),sieve(Y)))
r4: active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
r5: active(nats(N)) -> mark(cons(N,nats(s(N))))
r6: active(zprimes()) -> mark(sieve(nats(s(s(|0|())))))
r7: mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
r8: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r9: mark(|0|()) -> active(|0|())
r10: mark(s(X)) -> active(s(mark(X)))
r11: mark(sieve(X)) -> active(sieve(mark(X)))
r12: mark(nats(X)) -> active(nats(mark(X)))
r13: mark(zprimes()) -> active(zprimes())
r14: filter(mark(X1),X2,X3) -> filter(X1,X2,X3)
r15: filter(X1,mark(X2),X3) -> filter(X1,X2,X3)
r16: filter(X1,X2,mark(X3)) -> filter(X1,X2,X3)
r17: filter(active(X1),X2,X3) -> filter(X1,X2,X3)
r18: filter(X1,active(X2),X3) -> filter(X1,X2,X3)
r19: filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
r20: cons(mark(X1),X2) -> cons(X1,X2)
r21: cons(X1,mark(X2)) -> cons(X1,X2)
r22: cons(active(X1),X2) -> cons(X1,X2)
r23: cons(X1,active(X2)) -> cons(X1,X2)
r24: s(mark(X)) -> s(X)
r25: s(active(X)) -> s(X)
r26: sieve(mark(X)) -> sieve(X)
r27: sieve(active(X)) -> sieve(X)
r28: nats(mark(X)) -> nats(X)
r29: nats(active(X)) -> nats(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      cons#_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
p2: filter#(X1,X2,active(X3)) -> filter#(X1,X2,X3)
p3: filter#(X1,active(X2),X3) -> filter#(X1,X2,X3)
p4: filter#(active(X1),X2,X3) -> filter#(X1,X2,X3)
p5: filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
p6: filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)

and R consists of:

r1: active(filter(cons(X,Y),|0|(),M)) -> mark(cons(|0|(),filter(Y,M,M)))
r2: active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
r3: active(sieve(cons(|0|(),Y))) -> mark(cons(|0|(),sieve(Y)))
r4: active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
r5: active(nats(N)) -> mark(cons(N,nats(s(N))))
r6: active(zprimes()) -> mark(sieve(nats(s(s(|0|())))))
r7: mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
r8: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r9: mark(|0|()) -> active(|0|())
r10: mark(s(X)) -> active(s(mark(X)))
r11: mark(sieve(X)) -> active(sieve(mark(X)))
r12: mark(nats(X)) -> active(nats(mark(X)))
r13: mark(zprimes()) -> active(zprimes())
r14: filter(mark(X1),X2,X3) -> filter(X1,X2,X3)
r15: filter(X1,mark(X2),X3) -> filter(X1,X2,X3)
r16: filter(X1,X2,mark(X3)) -> filter(X1,X2,X3)
r17: filter(active(X1),X2,X3) -> filter(X1,X2,X3)
r18: filter(X1,active(X2),X3) -> filter(X1,X2,X3)
r19: filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
r20: cons(mark(X1),X2) -> cons(X1,X2)
r21: cons(X1,mark(X2)) -> cons(X1,X2)
r22: cons(active(X1),X2) -> cons(X1,X2)
r23: cons(X1,active(X2)) -> cons(X1,X2)
r24: s(mark(X)) -> s(X)
r25: s(active(X)) -> s(X)
r26: sieve(mark(X)) -> sieve(X)
r27: sieve(active(X)) -> sieve(X)
r28: nats(mark(X)) -> nats(X)
r29: nats(active(X)) -> nats(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      filter#_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(1,0)) x2 + ((1,0),(1,1)) x3
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: sieve#(mark(X)) -> sieve#(X)
p2: sieve#(active(X)) -> sieve#(X)

and R consists of:

r1: active(filter(cons(X,Y),|0|(),M)) -> mark(cons(|0|(),filter(Y,M,M)))
r2: active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
r3: active(sieve(cons(|0|(),Y))) -> mark(cons(|0|(),sieve(Y)))
r4: active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
r5: active(nats(N)) -> mark(cons(N,nats(s(N))))
r6: active(zprimes()) -> mark(sieve(nats(s(s(|0|())))))
r7: mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
r8: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r9: mark(|0|()) -> active(|0|())
r10: mark(s(X)) -> active(s(mark(X)))
r11: mark(sieve(X)) -> active(sieve(mark(X)))
r12: mark(nats(X)) -> active(nats(mark(X)))
r13: mark(zprimes()) -> active(zprimes())
r14: filter(mark(X1),X2,X3) -> filter(X1,X2,X3)
r15: filter(X1,mark(X2),X3) -> filter(X1,X2,X3)
r16: filter(X1,X2,mark(X3)) -> filter(X1,X2,X3)
r17: filter(active(X1),X2,X3) -> filter(X1,X2,X3)
r18: filter(X1,active(X2),X3) -> filter(X1,X2,X3)
r19: filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
r20: cons(mark(X1),X2) -> cons(X1,X2)
r21: cons(X1,mark(X2)) -> cons(X1,X2)
r22: cons(active(X1),X2) -> cons(X1,X2)
r23: cons(X1,active(X2)) -> cons(X1,X2)
r24: s(mark(X)) -> s(X)
r25: s(active(X)) -> s(X)
r26: sieve(mark(X)) -> sieve(X)
r27: sieve(active(X)) -> sieve(X)
r28: nats(mark(X)) -> nats(X)
r29: nats(active(X)) -> nats(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      sieve#_A(x1) = ((1,0),(1,1)) x1
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: nats#(mark(X)) -> nats#(X)
p2: nats#(active(X)) -> nats#(X)

and R consists of:

r1: active(filter(cons(X,Y),|0|(),M)) -> mark(cons(|0|(),filter(Y,M,M)))
r2: active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
r3: active(sieve(cons(|0|(),Y))) -> mark(cons(|0|(),sieve(Y)))
r4: active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
r5: active(nats(N)) -> mark(cons(N,nats(s(N))))
r6: active(zprimes()) -> mark(sieve(nats(s(s(|0|())))))
r7: mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
r8: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r9: mark(|0|()) -> active(|0|())
r10: mark(s(X)) -> active(s(mark(X)))
r11: mark(sieve(X)) -> active(sieve(mark(X)))
r12: mark(nats(X)) -> active(nats(mark(X)))
r13: mark(zprimes()) -> active(zprimes())
r14: filter(mark(X1),X2,X3) -> filter(X1,X2,X3)
r15: filter(X1,mark(X2),X3) -> filter(X1,X2,X3)
r16: filter(X1,X2,mark(X3)) -> filter(X1,X2,X3)
r17: filter(active(X1),X2,X3) -> filter(X1,X2,X3)
r18: filter(X1,active(X2),X3) -> filter(X1,X2,X3)
r19: filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
r20: cons(mark(X1),X2) -> cons(X1,X2)
r21: cons(X1,mark(X2)) -> cons(X1,X2)
r22: cons(active(X1),X2) -> cons(X1,X2)
r23: cons(X1,active(X2)) -> cons(X1,X2)
r24: s(mark(X)) -> s(X)
r25: s(active(X)) -> s(X)
r26: sieve(mark(X)) -> sieve(X)
r27: sieve(active(X)) -> sieve(X)
r28: nats(mark(X)) -> nats(X)
r29: nats(active(X)) -> nats(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      nats#_A(x1) = ((1,0),(1,0)) x1
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: s#(mark(X)) -> s#(X)
p2: s#(active(X)) -> s#(X)

and R consists of:

r1: active(filter(cons(X,Y),|0|(),M)) -> mark(cons(|0|(),filter(Y,M,M)))
r2: active(filter(cons(X,Y),s(N),M)) -> mark(cons(X,filter(Y,N,M)))
r3: active(sieve(cons(|0|(),Y))) -> mark(cons(|0|(),sieve(Y)))
r4: active(sieve(cons(s(N),Y))) -> mark(cons(s(N),sieve(filter(Y,N,N))))
r5: active(nats(N)) -> mark(cons(N,nats(s(N))))
r6: active(zprimes()) -> mark(sieve(nats(s(s(|0|())))))
r7: mark(filter(X1,X2,X3)) -> active(filter(mark(X1),mark(X2),mark(X3)))
r8: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r9: mark(|0|()) -> active(|0|())
r10: mark(s(X)) -> active(s(mark(X)))
r11: mark(sieve(X)) -> active(sieve(mark(X)))
r12: mark(nats(X)) -> active(nats(mark(X)))
r13: mark(zprimes()) -> active(zprimes())
r14: filter(mark(X1),X2,X3) -> filter(X1,X2,X3)
r15: filter(X1,mark(X2),X3) -> filter(X1,X2,X3)
r16: filter(X1,X2,mark(X3)) -> filter(X1,X2,X3)
r17: filter(active(X1),X2,X3) -> filter(X1,X2,X3)
r18: filter(X1,active(X2),X3) -> filter(X1,X2,X3)
r19: filter(X1,X2,active(X3)) -> filter(X1,X2,X3)
r20: cons(mark(X1),X2) -> cons(X1,X2)
r21: cons(X1,mark(X2)) -> cons(X1,X2)
r22: cons(active(X1),X2) -> cons(X1,X2)
r23: cons(X1,active(X2)) -> cons(X1,X2)
r24: s(mark(X)) -> s(X)
r25: s(active(X)) -> s(X)
r26: sieve(mark(X)) -> sieve(X)
r27: sieve(active(X)) -> sieve(X)
r28: nats(mark(X)) -> nats(X)
r29: nats(active(X)) -> nats(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      s#_A(x1) = x1
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      active_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  Then no dependency pair remains.