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|())))))
  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))

-- SCC decomposition.

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

p1: active#(filter(cons(X,Y),|0|(),M)) -> cons#(|0|(),filter(Y,M,M))
p2: active#(filter(cons(X,Y),|0|(),M)) -> filter#(Y,M,M)
p3: active#(filter(cons(X,Y),s(N),M)) -> cons#(X,filter(Y,N,M))
p4: active#(filter(cons(X,Y),s(N),M)) -> filter#(Y,N,M)
p5: active#(sieve(cons(|0|(),Y))) -> cons#(|0|(),sieve(Y))
p6: active#(sieve(cons(|0|(),Y))) -> sieve#(Y)
p7: active#(sieve(cons(s(N),Y))) -> cons#(s(N),sieve(filter(Y,N,N)))
p8: active#(sieve(cons(s(N),Y))) -> sieve#(filter(Y,N,N))
p9: active#(sieve(cons(s(N),Y))) -> filter#(Y,N,N)
p10: active#(nats(N)) -> cons#(N,nats(s(N)))
p11: active#(nats(N)) -> nats#(s(N))
p12: active#(nats(N)) -> s#(N)
p13: active#(zprimes()) -> sieve#(nats(s(s(|0|()))))
p14: active#(zprimes()) -> nats#(s(s(|0|())))
p15: active#(zprimes()) -> s#(s(|0|()))
p16: active#(zprimes()) -> s#(|0|())
p17: active#(filter(X1,X2,X3)) -> filter#(active(X1),X2,X3)
p18: active#(filter(X1,X2,X3)) -> active#(X1)
p19: active#(filter(X1,X2,X3)) -> filter#(X1,active(X2),X3)
p20: active#(filter(X1,X2,X3)) -> active#(X2)
p21: active#(filter(X1,X2,X3)) -> filter#(X1,X2,active(X3))
p22: active#(filter(X1,X2,X3)) -> active#(X3)
p23: active#(cons(X1,X2)) -> cons#(active(X1),X2)
p24: active#(cons(X1,X2)) -> active#(X1)
p25: active#(s(X)) -> s#(active(X))
p26: active#(s(X)) -> active#(X)
p27: active#(sieve(X)) -> sieve#(active(X))
p28: active#(sieve(X)) -> active#(X)
p29: active#(nats(X)) -> nats#(active(X))
p30: active#(nats(X)) -> active#(X)
p31: filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
p32: filter#(X1,mark(X2),X3) -> filter#(X1,X2,X3)
p33: filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
p34: cons#(mark(X1),X2) -> cons#(X1,X2)
p35: s#(mark(X)) -> s#(X)
p36: sieve#(mark(X)) -> sieve#(X)
p37: nats#(mark(X)) -> nats#(X)
p38: proper#(filter(X1,X2,X3)) -> filter#(proper(X1),proper(X2),proper(X3))
p39: proper#(filter(X1,X2,X3)) -> proper#(X1)
p40: proper#(filter(X1,X2,X3)) -> proper#(X2)
p41: proper#(filter(X1,X2,X3)) -> proper#(X3)
p42: proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
p43: proper#(cons(X1,X2)) -> proper#(X1)
p44: proper#(cons(X1,X2)) -> proper#(X2)
p45: proper#(s(X)) -> s#(proper(X))
p46: proper#(s(X)) -> proper#(X)
p47: proper#(sieve(X)) -> sieve#(proper(X))
p48: proper#(sieve(X)) -> proper#(X)
p49: proper#(nats(X)) -> nats#(proper(X))
p50: proper#(nats(X)) -> proper#(X)
p51: filter#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
p52: cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
p53: s#(ok(X)) -> s#(X)
p54: sieve#(ok(X)) -> sieve#(X)
p55: nats#(ok(X)) -> nats#(X)
p56: top#(mark(X)) -> top#(proper(X))
p57: top#(mark(X)) -> proper#(X)
p58: top#(ok(X)) -> top#(active(X))
p59: top#(ok(X)) -> active#(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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p56, p58}
  {p18, p20, p22, p24, p26, p28, p30}
  {p39, p40, p41, p43, p44, p46, p48, p50}
  {p31, p32, p33, p51}
  {p34, p52}
  {p36, p54}
  {p37, p55}
  {p35, p53}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(X))
p2: top#(mark(X)) -> top#(proper(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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(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, r30, r31, r32

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      top#_A(x1) = ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1
      ok_A(x1) = x1 + (0,0,5,0)
      active_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,1,0,0)) x1 + (0,9,0,1)
      mark_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (10,1,8,7)
      proper_A(x1) = ((1,0,0,0),(0,1,0,0),(1,0,1,0),(0,1,1,0)) x1 + (0,2,0,1)
      filter_A(x1,x2,x3) = x1 + ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x2 + ((1,0,0,0),(1,1,0,0),(1,0,1,0),(0,0,1,0)) x3 + (11,2,20,0)
      cons_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x1 + ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x2 + (1,1,0,3)
      s_A(x1) = ((1,0,0,0),(1,0,0,0),(1,1,0,0),(1,0,1,0)) x1 + (3,7,0,0)
      sieve_A(x1) = x1 + (11,8,11,8)
      nats_A(x1) = ((1,0,0,0),(0,0,0,0),(1,1,0,0),(0,1,1,0)) x1 + (12,7,10,0)
      |0|_A() = (5,1,0,1)
      zprimes_A() = (45,1,1,0)

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: top#(ok(X)) -> top#(active(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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(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, r28, r29, r30, r31, r32

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      top#_A(x1) = ((0,0,0,0),(1,0,0,0),(1,0,0,0),(0,1,0,0)) x1
      ok_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + (9,6,8,23)
      active_A(x1) = ((1,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,0,0)) x1 + (1,5,13,25)
      filter_A(x1,x2,x3) = ((1,0,0,0),(1,0,0,0),(0,1,0,0),(0,1,1,0)) x1 + ((1,0,0,0),(1,0,0,0),(1,1,0,0),(0,0,1,0)) x2 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x3 + (13,0,18,13)
      mark_A(x1) = ((0,0,0,0),(1,0,0,0),(1,1,0,0),(1,1,0,0)) x1 + (4,6,10,1)
      cons_A(x1,x2) = x1 + ((1,0,0,0),(0,0,0,0),(0,1,0,0),(0,0,0,0)) x2 + (16,7,1,26)
      s_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (2,0,9,4)
      sieve_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (1,4,16,1)
      nats_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (4,2,1,1)
      |0|_A() = (1,1,1,1)
      zprimes_A() = (4,21,1,1)

The next rules are strictly ordered:

  p1

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: active#(nats(X)) -> active#(X)
p2: active#(sieve(X)) -> active#(X)
p3: active#(s(X)) -> active#(X)
p4: active#(cons(X1,X2)) -> active#(X1)
p5: active#(filter(X1,X2,X3)) -> active#(X3)
p6: active#(filter(X1,X2,X3)) -> active#(X2)
p7: active#(filter(X1,X2,X3)) -> active#(X1)

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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      active#_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,0,0),(1,1,1,0)) x1
      nats_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      sieve_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      s_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      cons_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      filter_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,0,0),(1,1,1,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3 + (1,1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7

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: proper#(nats(X)) -> proper#(X)
p2: proper#(sieve(X)) -> proper#(X)
p3: proper#(s(X)) -> proper#(X)
p4: proper#(cons(X1,X2)) -> proper#(X2)
p5: proper#(cons(X1,X2)) -> proper#(X1)
p6: proper#(filter(X1,X2,X3)) -> proper#(X3)
p7: proper#(filter(X1,X2,X3)) -> proper#(X2)
p8: proper#(filter(X1,X2,X3)) -> proper#(X1)

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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      proper#_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1
      nats_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      sieve_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      s_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      cons_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,1,1)
      filter_A(x1,x2,x3) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x3 + (1,1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8
  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, r30, r31, r32, r33, r34

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#(ok(X1),ok(X2),ok(X3)) -> filter#(X1,X2,X3)
p3: filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
p4: 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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2, p3, p4

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#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(ok(X1),ok(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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      cons#_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,0,0),(1,1,1,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,0,0),(1,1,1,0)) x1 + (1,1,1,1)
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,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: sieve#(mark(X)) -> sieve#(X)
p2: sieve#(ok(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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      sieve#_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,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, r30, r31, r32, r33, r34

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#(ok(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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      nats#_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,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, r30, r31, r32, r33, r34

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#(ok(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: active(filter(X1,X2,X3)) -> filter(active(X1),X2,X3)
r8: active(filter(X1,X2,X3)) -> filter(X1,active(X2),X3)
r9: active(filter(X1,X2,X3)) -> filter(X1,X2,active(X3))
r10: active(cons(X1,X2)) -> cons(active(X1),X2)
r11: active(s(X)) -> s(active(X))
r12: active(sieve(X)) -> sieve(active(X))
r13: active(nats(X)) -> nats(active(X))
r14: filter(mark(X1),X2,X3) -> mark(filter(X1,X2,X3))
r15: filter(X1,mark(X2),X3) -> mark(filter(X1,X2,X3))
r16: filter(X1,X2,mark(X3)) -> mark(filter(X1,X2,X3))
r17: cons(mark(X1),X2) -> mark(cons(X1,X2))
r18: s(mark(X)) -> mark(s(X))
r19: sieve(mark(X)) -> mark(sieve(X))
r20: nats(mark(X)) -> mark(nats(X))
r21: proper(filter(X1,X2,X3)) -> filter(proper(X1),proper(X2),proper(X3))
r22: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r23: proper(|0|()) -> ok(|0|())
r24: proper(s(X)) -> s(proper(X))
r25: proper(sieve(X)) -> sieve(proper(X))
r26: proper(nats(X)) -> nats(proper(X))
r27: proper(zprimes()) -> ok(zprimes())
r28: filter(ok(X1),ok(X2),ok(X3)) -> ok(filter(X1,X2,X3))
r29: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r30: s(ok(X)) -> ok(s(X))
r31: sieve(ok(X)) -> ok(sieve(X))
r32: nats(ok(X)) -> ok(nats(X))
r33: top(mark(X)) -> top(proper(X))
r34: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      s#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x1
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,1,1)
      ok_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (1,1,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, r30, r31, r32, r33, r34

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