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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{1, x1 - 7}
        filter_A(x1,x2,x3) = max{x1, x2 + 56, x3 + 69}
        cons_A(x1,x2) = max{64, x1 + 52, x2 - 40}
        |0|_A = 11
        mark#_A(x1) = max{0, x1 - 7}
        zprimes_A = 209
        sieve_A(x1) = max{209, x1 + 114}
        nats_A(x1) = x1 + 66
        s_A(x1) = max{14, x1 + 9}
        mark_A(x1) = x1
        active_A(x1) = max{10, x1}
  
    precedence:
    
      active# = filter = cons = |0| = mark# = zprimes = sieve = nats = s = mark = active
    
    partial status:
  
      pi(active#) = []
      pi(filter) = []
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = []
      pi(zprimes) = []
      pi(sieve) = []
      pi(nats) = []
      pi(s) = []
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p7

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: mark#(sieve(X)) -> active#(sieve(mark(X)))
p8: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p9: mark#(s(X)) -> mark#(X)
p10: mark#(s(X)) -> active#(s(mark(X)))
p11: active#(sieve(cons(|0|(),Y))) -> mark#(cons(|0|(),sieve(Y)))
p12: mark#(cons(X1,X2)) -> mark#(X1)
p13: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p14: active#(filter(cons(X,Y),s(N),M)) -> mark#(cons(X,filter(Y,N,M)))
p15: mark#(filter(X1,X2,X3)) -> mark#(X3)
p16: mark#(filter(X1,X2,X3)) -> mark#(X2)
p17: mark#(filter(X1,X2,X3)) -> mark#(X1)
p18: 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, p18}


-- 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)) -> active#(cons(mark(X1),X2))
p8: active#(sieve(cons(|0|(),Y))) -> mark#(cons(|0|(),sieve(Y)))
p9: mark#(cons(X1,X2)) -> mark#(X1)
p10: mark#(s(X)) -> active#(s(mark(X)))
p11: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p12: mark#(s(X)) -> mark#(X)
p13: mark#(sieve(X)) -> active#(sieve(mark(X)))
p14: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p15: mark#(sieve(X)) -> mark#(X)
p16: mark#(nats(X)) -> active#(nats(mark(X)))
p17: mark#(nats(X)) -> mark#(X)
p18: mark#(zprimes()) -> active#(zprimes())

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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{21, x1}
        filter_A(x1,x2,x3) = max{x1 + 28, x2 + 39, x3 + 92}
        cons_A(x1,x2) = x1 + 30
        |0|_A = 58
        mark#_A(x1) = max{14, x1 + 3}
        mark_A(x1) = x1
        s_A(x1) = max{123, x1 + 65}
        sieve_A(x1) = x1 + 57
        zprimes_A = 279
        nats_A(x1) = x1 + 31
        active_A(x1) = max{29, x1}
  
    precedence:
    
      filter = s = sieve = zprimes > |0| = mark = nats = active > active# = cons > mark#
    
    partial status:
  
      pi(active#) = []
      pi(filter) = []
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = [1]
      pi(mark) = []
      pi(s) = []
      pi(sieve) = []
      pi(zprimes) = []
      pi(nats) = []
      pi(active) = []

The next rules are strictly ordered:

  p18

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

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{5, x1 - 4}
        filter_A(x1,x2,x3) = max{x1 + 62, x2 + 62, x3 + 12}
        cons_A(x1,x2) = max{27, x1 + 26}
        |0|_A = 7
        mark#_A(x1) = max{4, x1 - 4}
        nats_A(x1) = x1 + 48
        mark_A(x1) = x1
        zprimes_A = 112
        sieve_A(x1) = max{60, x1 + 38}
        s_A(x1) = x1 + 9
        active_A(x1) = max{1, x1}
  
    precedence:
    
      active# = filter = cons = |0| = mark# = nats = mark = zprimes = sieve = s = active
    
    partial status:
  
      pi(active#) = []
      pi(filter) = []
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = []
      pi(nats) = []
      pi(mark) = [1]
      pi(zprimes) = []
      pi(sieve) = []
      pi(s) = []
      pi(active) = [1]

The next rules are strictly ordered:

  p10

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


-- 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)) -> active#(cons(mark(X1),X2))
p8: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p9: mark#(cons(X1,X2)) -> mark#(X1)
p10: mark#(s(X)) -> active#(s(mark(X)))
p11: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p12: mark#(sieve(X)) -> active#(sieve(mark(X)))
p13: mark#(sieve(X)) -> mark#(X)
p14: mark#(s(X)) -> mark#(X)
p15: mark#(nats(X)) -> active#(nats(mark(X)))
p16: mark#(nats(X)) -> mark#(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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{82, x1 - 14}
        filter_A(x1,x2,x3) = 217
        cons_A(x1,x2) = 174
        |0|_A = 118
        mark#_A(x1) = 203
        mark_A(x1) = max{204, x1 - 407}
        s_A(x1) = 102
        sieve_A(x1) = 217
        zprimes_A = 217
        nats_A(x1) = 217
        active_A(x1) = max{101, x1 - 13}
  
    precedence:
    
      nats > filter = |0| = mark = sieve = active > active# = cons = mark# = s = zprimes
    
    partial status:
  
      pi(active#) = []
      pi(filter) = []
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = []
      pi(mark) = []
      pi(s) = []
      pi(sieve) = []
      pi(zprimes) = []
      pi(nats) = []
      pi(active) = []

The next rules are strictly ordered:

  p10

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#(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)) -> active#(cons(mark(X1),X2))
p8: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p9: mark#(cons(X1,X2)) -> mark#(X1)
p10: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p11: mark#(sieve(X)) -> active#(sieve(mark(X)))
p12: mark#(sieve(X)) -> mark#(X)
p13: mark#(s(X)) -> mark#(X)
p14: mark#(nats(X)) -> active#(nats(mark(X)))
p15: mark#(nats(X)) -> mark#(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, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15}


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

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{1, x1 - 3}
        filter_A(x1,x2,x3) = max{x1 + 71, x2 + 9, x3 + 12}
        cons_A(x1,x2) = max{115, x1 + 25}
        |0|_A = 8
        mark#_A(x1) = max{3, x1}
        nats_A(x1) = x1 + 158
        mark_A(x1) = x1 + 3
        zprimes_A = 246
        sieve_A(x1) = x1 + 8
        s_A(x1) = x1 + 34
        active_A(x1) = max{11, x1}
  
    precedence:
    
      mark > active > active# = filter = cons = |0| = mark# = nats = zprimes = sieve = s
    
    partial status:
  
      pi(active#) = []
      pi(filter) = [1]
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = [1]
      pi(nats) = [1]
      pi(mark) = []
      pi(zprimes) = []
      pi(sieve) = [1]
      pi(s) = []
      pi(active) = [1]

The next rules are strictly ordered:

  p11

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#(nats(X)) -> mark#(X)
p3: mark#(nats(X)) -> active#(nats(mark(X)))
p4: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p5: mark#(sieve(X)) -> mark#(X)
p6: mark#(s(X)) -> mark#(X)
p7: mark#(sieve(X)) -> active#(sieve(mark(X)))
p8: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p9: mark#(cons(X1,X2)) -> mark#(X1)
p10: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p11: mark#(filter(X1,X2,X3)) -> mark#(X3)
p12: mark#(filter(X1,X2,X3)) -> mark#(X2)
p13: mark#(filter(X1,X2,X3)) -> mark#(X1)
p14: 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}


-- 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#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
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)) -> active#(cons(mark(X1),X2))
p8: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p9: mark#(sieve(X)) -> active#(sieve(mark(X)))
p10: mark#(sieve(X)) -> mark#(X)
p11: mark#(cons(X1,X2)) -> mark#(X1)
p12: mark#(s(X)) -> mark#(X)
p13: mark#(nats(X)) -> active#(nats(mark(X)))
p14: mark#(nats(X)) -> mark#(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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{1, x1 - 5}
        filter_A(x1,x2,x3) = max{x1 + 19, x2, x3 + 19}
        cons_A(x1,x2) = max{12, x1}
        |0|_A = 13
        mark#_A(x1) = max{0, x1 - 5}
        mark_A(x1) = x1
        sieve_A(x1) = max{15, x1}
        s_A(x1) = x1 + 15
        zprimes_A = 43
        nats_A(x1) = max{12, x1}
        active_A(x1) = max{12, x1}
  
    precedence:
    
      active# = filter = cons = |0| = mark# = mark = sieve = s = zprimes = nats = active
    
    partial status:
  
      pi(active#) = []
      pi(filter) = []
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = []
      pi(mark) = []
      pi(sieve) = []
      pi(s) = []
      pi(zprimes) = []
      pi(nats) = []
      pi(active) = []

The next rules are strictly ordered:

  p6

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#(filter(X1,X2,X3)) -> active#(filter(mark(X1),mark(X2),mark(X3)))
p3: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p4: mark#(filter(X1,X2,X3)) -> mark#(X1)
p5: mark#(filter(X1,X2,X3)) -> mark#(X2)
p6: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p7: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p8: mark#(sieve(X)) -> active#(sieve(mark(X)))
p9: mark#(sieve(X)) -> mark#(X)
p10: mark#(cons(X1,X2)) -> mark#(X1)
p11: mark#(s(X)) -> mark#(X)
p12: mark#(nats(X)) -> active#(nats(mark(X)))
p13: mark#(nats(X)) -> mark#(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, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13}


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

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{225, x1 + 114}
        filter_A(x1,x2,x3) = 223
        cons_A(x1,x2) = 132
        |0|_A = 426
        mark#_A(x1) = 337
        nats_A(x1) = 223
        mark_A(x1) = x1 + 184
        zprimes_A = 442
        sieve_A(x1) = 223
        s_A(x1) = 236
        active_A(x1) = x1 + 93
  
    precedence:
    
      active# = filter = cons = |0| = mark# = nats = mark = zprimes = sieve = s = active
    
    partial status:
  
      pi(active#) = []
      pi(filter) = []
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = []
      pi(nats) = []
      pi(mark) = []
      pi(zprimes) = []
      pi(sieve) = []
      pi(s) = []
      pi(active) = [1]

The next rules are strictly ordered:

  p10

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


-- 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#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p4: mark#(filter(X1,X2,X3)) -> mark#(X1)
p5: mark#(filter(X1,X2,X3)) -> mark#(X2)
p6: mark#(sieve(X)) -> active#(sieve(mark(X)))
p7: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p8: mark#(sieve(X)) -> mark#(X)
p9: mark#(cons(X1,X2)) -> mark#(X1)
p10: mark#(s(X)) -> mark#(X)
p11: mark#(nats(X)) -> active#(nats(mark(X)))
p12: mark#(nats(X)) -> mark#(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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{179, x1 - 175}
        filter_A(x1,x2,x3) = max{x1 + 13, x2, x3 + 353}
        cons_A(x1,x2) = max{27, x1 + 3}
        |0|_A = 56
        mark#_A(x1) = max{179, x1 - 147}
        mark_A(x1) = x1 + 6
        sieve_A(x1) = x1 + 28
        s_A(x1) = x1 + 31
        zprimes_A = 352
        nats_A(x1) = x1 + 179
        active_A(x1) = max{32, x1}
  
    precedence:
    
      mark > sieve > active# = filter = mark# = s = nats > cons = |0| = zprimes = active
    
    partial status:
  
      pi(active#) = []
      pi(filter) = [3]
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = []
      pi(mark) = []
      pi(sieve) = []
      pi(s) = [1]
      pi(zprimes) = []
      pi(nats) = [1]
      pi(active) = [1]

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: active#(filter(cons(X,Y),|0|(),M)) -> mark#(cons(|0|(),filter(Y,M,M)))
p2: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p3: mark#(filter(X1,X2,X3)) -> mark#(X1)
p4: mark#(filter(X1,X2,X3)) -> mark#(X2)
p5: mark#(sieve(X)) -> active#(sieve(mark(X)))
p6: active#(zprimes()) -> mark#(sieve(nats(s(s(|0|())))))
p7: mark#(sieve(X)) -> mark#(X)
p8: mark#(cons(X1,X2)) -> mark#(X1)
p9: mark#(s(X)) -> mark#(X)
p10: mark#(nats(X)) -> active#(nats(mark(X)))
p11: mark#(nats(X)) -> mark#(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, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11}


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

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = x1 + 8
        filter_A(x1,x2,x3) = max{x1, x2, x3}
        cons_A(x1,x2) = max{x1, x2}
        |0|_A = 1
        mark#_A(x1) = x1 + 8
        nats_A(x1) = x1
        mark_A(x1) = x1
        zprimes_A = 5
        sieve_A(x1) = x1 + 3
        s_A(x1) = x1
        active_A(x1) = x1
  
    precedence:
    
      sieve > active# = filter = cons = |0| = mark# = zprimes > mark = s = active > nats
    
    partial status:
  
      pi(active#) = []
      pi(filter) = []
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = []
      pi(nats) = []
      pi(mark) = []
      pi(zprimes) = []
      pi(sieve) = []
      pi(s) = []
      pi(active) = []

The next rules are strictly ordered:

  p4

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#(nats(X)) -> mark#(X)
p3: mark#(nats(X)) -> active#(nats(mark(X)))
p4: mark#(sieve(X)) -> mark#(X)
p5: mark#(s(X)) -> mark#(X)
p6: mark#(cons(X1,X2)) -> mark#(X1)
p7: mark#(sieve(X)) -> active#(sieve(mark(X)))
p8: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p9: mark#(filter(X1,X2,X3)) -> mark#(X2)
p10: mark#(filter(X1,X2,X3)) -> mark#(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: 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}


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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{66, x1 - 9}
        filter_A(x1,x2,x3) = max{x1, x2 + 147, x3 + 147}
        cons_A(x1,x2) = max{x1 + 78, x2 - 53}
        |0|_A = 68
        mark#_A(x1) = max{1, x1 - 9}
        sieve_A(x1) = x1 + 75
        mark_A(x1) = x1
        s_A(x1) = max{85, x1 + 16}
        nats_A(x1) = max{119, x1 + 86}
        active_A(x1) = max{67, x1}
        zprimes_A = 262
  
    precedence:
    
      zprimes > filter = sieve > mark > |0| > cons > s = active > active# = mark# = nats
    
    partial status:
  
      pi(active#) = []
      pi(filter) = []
      pi(cons) = [1]
      pi(|0|) = []
      pi(mark#) = []
      pi(sieve) = []
      pi(mark) = [1]
      pi(s) = [1]
      pi(nats) = [1]
      pi(active) = [1]
      pi(zprimes) = []

The next rules are strictly ordered:

  p10

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


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

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{97, x1 + 13}
        filter_A(x1,x2,x3) = max{x1 + 99, x2 + 99, x3 + 99}
        cons_A(x1,x2) = x1 + 56
        |0|_A = 16
        mark#_A(x1) = x1 + 55
        nats_A(x1) = max{70, x1 + 56}
        mark_A(x1) = x1
        sieve_A(x1) = x1 + 53
        s_A(x1) = x1 + 118
        active_A(x1) = max{15, x1}
        zprimes_A = 362
  
    precedence:
    
      active# = filter = cons = |0| = mark# = nats = mark = sieve = s = active = zprimes
    
    partial status:
  
      pi(active#) = [1]
      pi(filter) = []
      pi(cons) = []
      pi(|0|) = []
      pi(mark#) = [1]
      pi(nats) = []
      pi(mark) = [1]
      pi(sieve) = []
      pi(s) = []
      pi(active) = [1]
      pi(zprimes) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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


-- Reduction pair.

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

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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        mark#_A(x1) = 380
        nats_A(x1) = 132
        active#_A(x1) = x1 + 223
        mark_A(x1) = max{156, x1 + 42}
        sieve_A(x1) = 157
        cons_A(x1,x2) = 79
        s_A(x1) = 180
        filter_A(x1,x2,x3) = 191
        active_A(x1) = max{101, x1 + 24}
        |0|_A = 262
        zprimes_A = 175
  
    precedence:
    
      mark# = nats = active# = mark = sieve = cons = s = filter = active = |0| = zprimes
    
    partial status:
  
      pi(mark#) = []
      pi(nats) = []
      pi(active#) = []
      pi(mark) = []
      pi(sieve) = []
      pi(cons) = []
      pi(s) = []
      pi(filter) = []
      pi(active) = [1]
      pi(|0|) = []
      pi(zprimes) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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


-- Reduction pair.

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

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

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{6, x1 - 9}
        sieve_A(x1) = max{34, x1 + 26}
        cons_A(x1,x2) = max{21, x1 + 5}
        s_A(x1) = x1 + 42
        mark#_A(x1) = x1
        filter_A(x1,x2,x3) = max{x1 + 18, x2 + 18}
        mark_A(x1) = x1
        active_A(x1) = max{6, x1}
        |0|_A = 22
        nats_A(x1) = x1 + 22
        zprimes_A = 154
  
    precedence:
    
      active# = sieve = cons = s = mark# = filter = mark = active = |0| = nats = zprimes
    
    partial status:
  
      pi(active#) = []
      pi(sieve) = []
      pi(cons) = []
      pi(s) = []
      pi(mark#) = [1]
      pi(filter) = []
      pi(mark) = [1]
      pi(active) = [1]
      pi(|0|) = []
      pi(nats) = []
      pi(zprimes) = []

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p2: mark#(sieve(X)) -> mark#(X)
p3: mark#(s(X)) -> mark#(X)
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(sieve(X)) -> active#(sieve(mark(X)))
p6: mark#(filter(X1,X2,X3)) -> mark#(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: 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}


-- Reduction pair.

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

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

  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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = x1 + 28
        sieve_A(x1) = max{125, x1 + 104}
        cons_A(x1,x2) = max{19, x1 + 1}
        s_A(x1) = x1 + 44
        mark#_A(x1) = x1 + 52
        filter_A(x1,x2,x3) = max{x1 + 52, x2 + 53, x3 + 74}
        mark_A(x1) = x1
        active_A(x1) = max{2, x1}
        |0|_A = 20
        nats_A(x1) = x1 + 42
        zprimes_A = 255
  
    precedence:
    
      sieve = cons = filter = |0| = nats > active# = s = mark# = mark = active = zprimes
    
    partial status:
  
      pi(active#) = []
      pi(sieve) = []
      pi(cons) = []
      pi(s) = []
      pi(mark#) = [1]
      pi(filter) = []
      pi(mark) = [1]
      pi(active) = [1]
      pi(|0|) = []
      pi(nats) = []
      pi(zprimes) = []

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p2: mark#(filter(X1,X2,X3)) -> mark#(X1)
p3: mark#(sieve(X)) -> active#(sieve(mark(X)))
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(sieve(X)) -> mark#(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, p2, p3, p4, p5}


-- Reduction pair.

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

p1: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p2: mark#(sieve(X)) -> mark#(X)
p3: mark#(cons(X1,X2)) -> mark#(X1)
p4: mark#(sieve(X)) -> active#(sieve(mark(X)))
p5: mark#(filter(X1,X2,X3)) -> mark#(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: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        active#_A(x1) = max{2, x1 - 30}
        sieve_A(x1) = x1 + 62
        cons_A(x1,x2) = max{14, x1}
        s_A(x1) = x1 + 14
        mark#_A(x1) = max{46, x1 + 29}
        filter_A(x1,x2,x3) = x1 + 46
        mark_A(x1) = x1 + 30
        active_A(x1) = max{42, x1}
        |0|_A = 15
        nats_A(x1) = max{87, x1 + 45}
        zprimes_A = 181
  
    precedence:
    
      mark > s = active = nats = zprimes > active# = sieve > filter > cons = mark# > |0|
    
    partial status:
  
      pi(active#) = []
      pi(sieve) = []
      pi(cons) = [1]
      pi(s) = []
      pi(mark#) = [1]
      pi(filter) = []
      pi(mark) = [1]
      pi(active) = [1]
      pi(|0|) = []
      pi(nats) = []
      pi(zprimes) = []

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(sieve(cons(s(N),Y))) -> mark#(cons(s(N),sieve(filter(Y,N,N))))
p2: mark#(sieve(X)) -> mark#(X)
p3: mark#(cons(X1,X2)) -> mark#(X1)
p4: mark#(filter(X1,X2,X3)) -> mark#(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: 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:

  {p2, p3, p4}


-- Reduction pair.

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

p1: mark#(sieve(X)) -> mark#(X)
p2: mark#(filter(X1,X2,X3)) -> mark#(X1)
p3: mark#(cons(X1,X2)) -> mark#(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: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        mark#_A(x1) = max{3, x1 + 2}
        sieve_A(x1) = x1 + 1
        filter_A(x1,x2,x3) = max{x1 + 3, x2 + 2, x3 + 3}
        cons_A(x1,x2) = max{x1, x2 + 1}
  
    precedence:
    
      mark# = sieve = filter = cons
    
    partial status:
  
      pi(mark#) = []
      pi(sieve) = [1]
      pi(filter) = [3]
      pi(cons) = [2]

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: mark#(sieve(X)) -> mark#(X)
p2: mark#(cons(X1,X2)) -> mark#(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: 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}


-- Reduction pair.

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

p1: mark#(sieve(X)) -> mark#(X)
p2: mark#(cons(X1,X2)) -> mark#(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: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        mark#_A(x1) = max{4, x1 + 3}
        sieve_A(x1) = x1 + 2
        cons_A(x1,x2) = max{x1 + 1, x2 + 1}
  
    precedence:
    
      mark# = sieve = cons
    
    partial status:
  
      pi(mark#) = []
      pi(sieve) = [1]
      pi(cons) = [2]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(cons(X1,X2)) -> mark#(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: 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}


-- Reduction pair.

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

p1: mark#(cons(X1,X2)) -> mark#(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: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        mark#_A(x1) = x1 + 2
        cons_A(x1,x2) = max{x1 + 1, x2 + 1}
  
    precedence:
    
      mark# = cons
    
    partial status:
  
      pi(mark#) = []
      pi(cons) = [2]

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: 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 reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        cons#_A(x1,x2) = max{0, x1 - 2}
        mark_A(x1) = x1
        active_A(x1) = max{3, x1 + 1}
  
    precedence:
    
      cons# = mark = active
    
    partial status:
  
      pi(cons#) = []
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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#(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 estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: cons#(X1,mark(X2)) -> cons#(X1,X2)
p2: cons#(mark(X1),X2) -> cons#(X1,X2)
p3: cons#(X1,active(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 reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        cons#_A(x1,x2) = max{0, x2 - 2}
        mark_A(x1) = max{3, x1 + 1}
        active_A(x1) = x1
  
    precedence:
    
      cons# = mark = active
    
    partial status:
  
      pi(cons#) = []
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(X1,active(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 estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(X1,active(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 reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        cons#_A(x1,x2) = x1 + 1
        mark_A(x1) = x1 + 1
        active_A(x1) = x1 + 1
  
    precedence:
    
      cons# = mark = active
    
    partial status:
  
      pi(cons#) = []
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: cons#(X1,active(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 estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: cons#(X1,active(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 reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        cons#_A(x1,x2) = max{0, x2 - 2}
        active_A(x1) = max{3, x1 + 1}
  
    precedence:
    
      cons# = active
    
    partial status:
  
      pi(cons#) = []
      pi(active) = [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: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        filter#_A(x1,x2,x3) = max{x1 - 1, x2 - 1, x3 + 1}
        mark_A(x1) = x1
        active_A(x1) = x1
  
    precedence:
    
      filter# = mark = active
    
    partial status:
  
      pi(filter#) = [3]
      pi(mark) = [1]
      pi(active) = [1]

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: filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
p2: filter#(X1,active(X2),X3) -> filter#(X1,X2,X3)
p3: filter#(active(X1),X2,X3) -> filter#(X1,X2,X3)
p4: filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
p5: 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 estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5}


-- 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,mark(X2),X3) -> filter#(X1,X2,X3)
p3: filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
p4: filter#(active(X1),X2,X3) -> filter#(X1,X2,X3)
p5: filter#(X1,active(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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        filter#_A(x1,x2,x3) = max{0, x2 - 2}
        mark_A(x1) = max{3, x1 + 1}
        active_A(x1) = x1
  
    precedence:
    
      filter# = mark = active
    
    partial status:
  
      pi(filter#) = []
      pi(mark) = [1]
      pi(active) = [1]

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: filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
p2: filter#(X1,X2,mark(X3)) -> filter#(X1,X2,X3)
p3: filter#(active(X1),X2,X3) -> filter#(X1,X2,X3)
p4: filter#(X1,active(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 estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4}


-- 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,active(X2),X3) -> filter#(X1,X2,X3)
p3: filter#(active(X1),X2,X3) -> filter#(X1,X2,X3)
p4: filter#(X1,X2,mark(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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        filter#_A(x1,x2,x3) = max{x1 - 1, x2 - 1, x3 + 1}
        mark_A(x1) = x1
        active_A(x1) = x1
  
    precedence:
    
      filter# = mark = active
    
    partial status:
  
      pi(filter#) = [3]
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
p2: filter#(X1,active(X2),X3) -> filter#(X1,X2,X3)
p3: filter#(active(X1),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 estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- 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#(active(X1),X2,X3) -> filter#(X1,X2,X3)
p3: filter#(X1,active(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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        filter#_A(x1,x2,x3) = max{x1 - 1, x2 + 1, x3 + 1}
        mark_A(x1) = x1
        active_A(x1) = x1
  
    precedence:
    
      filter# = mark = active
    
    partial status:
  
      pi(filter#) = [2]
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

p1: filter#(mark(X1),X2,X3) -> filter#(X1,X2,X3)
p2: filter#(active(X1),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 estimated dependency graph contains the following SCCs:

  {p1, p2}


-- 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#(active(X1),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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        filter#_A(x1,x2,x3) = max{x1, x3 + 1}
        mark_A(x1) = x1 + 2
        active_A(x1) = x1 + 1
  
    precedence:
    
      filter# = mark = active
    
    partial status:
  
      pi(filter#) = [1]
      pi(mark) = []
      pi(active) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: filter#(active(X1),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 estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: filter#(active(X1),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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        filter#_A(x1,x2,x3) = max{x1 + 1, x2 + 1, x3 + 1}
        active_A(x1) = x1
  
    precedence:
    
      filter# = active
    
    partial status:
  
      pi(filter#) = [1]
      pi(active) = [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: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        sieve#_A(x1) = max{3, x1 + 2}
        mark_A(x1) = x1
        active_A(x1) = x1 + 1
  
    precedence:
    
      sieve# = mark = active
    
    partial status:
  
      pi(sieve#) = [1]
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: 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 estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: 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:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        sieve#_A(x1) = x1 + 1
        active_A(x1) = x1
  
    precedence:
    
      sieve# = active
    
    partial status:
  
      pi(sieve#) = [1]
      pi(active) = [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: 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 monotone reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        nats#_A(x1) = max{3, x1 + 2}
        mark_A(x1) = x1
        active_A(x1) = x1 + 1
  
    precedence:
    
      nats# = mark = active
    
    partial status:
  
      pi(nats#) = [1]
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: 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}


-- Reduction pair.

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

p1: 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 monotone reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        nats#_A(x1) = x1 + 1
        active_A(x1) = x1
  
    precedence:
    
      nats# = active
    
    partial status:
  
      pi(nats#) = [1]
      pi(active) = [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: 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 monotone reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        s#_A(x1) = max{3, x1 + 2}
        mark_A(x1) = x1
        active_A(x1) = x1 + 1
  
    precedence:
    
      s# = mark = active
    
    partial status:
  
      pi(s#) = [1]
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: 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 estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: 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 monotone reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        s#_A(x1) = x1 + 1
        active_A(x1) = x1
  
    precedence:
    
      s# = active
    
    partial status:
  
      pi(s#) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1

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