TRS:
 { filter(cons(X), 0(), M) -> cons(0()),
  filter(cons(X), s(N), M) -> cons(X),
          sieve(cons(0())) -> cons(0()),
         sieve(cons(s(N))) -> cons(s(N)),
                   nats(N) -> cons(N),
                 zprimes() -> sieve(nats(s(s(0()))))}
 POP* + Boolean Semantic Labelling:
  Normal positions:
  pi(nats_sl=1) = [1], pi(nats_sl=0) = [1], pi(sieve_sl=1) = [1], pi(sieve_sl=0) = [1], pi(filter_sl=1) = [1,2,3], pi(filter_sl=0) = [1,2,3]
  
Safe positions:
   pi(s_sl=1) = [1], pi(s_sl=0) = [1], pi(cons_sl=1) = [1], pi(cons_sl=0) = [1]
  
Precedence:
   nats_sl=0 > cons_sl=0, 
   filter_sl=0 > cons_sl=0, 
   zprimes_sl=0 > nats_sl=0, 
   zprimes_sl=0 > sieve_sl=0, 
   zprimes_sl=0 > s_sl=0, 
   zprimes_sl=0 > 0_sl=0
   empty
  
Interpretation:
   cons^(1):
   0 | 0
   1 | 0
   0^(0):
    | 0
   filter^(3):
   000 | 0
   001 | 0
   010 | 0
   011 | 0
   100 | 0
   101 | 0
   110 | 0
   111 | 0
   s^(1):
   0 | 0
   1 | 0
   sieve^(1):
   0 | 0
   1 | 0
   nats^(1):
   0 | 0
   1 | 0
   zprimes^(0):
    | 0
   
  
Labelling:
   cons^(1):
   0 | 0
   1 | 0
   0^(0):
    | 0
   filter^(3):
   000 | 0
   001 | 0
   010 | 0
   011 | 0
   100 | 0
   101 | 0
   110 | 0
   111 | 0
   s^(1):
   0 | 0
   1 | 0
   sieve^(1):
   0 | 0
   1 | 0
   nats^(1):
   0 | 0
   1 | 0
   zprimes^(0):
    | 0
   
  
Labelled predicative System:
   {  filter_sl=0(cons_sl=0(;X),0_sl=0(),M;) -> cons_sl=0(;0_sl=0()),
      filter_sl=0(cons_sl=0(;X),0_sl=0(),M;) -> cons_sl=0(;0_sl=0()),
      filter_sl=0(cons_sl=0(;X),0_sl=0(),M;) -> cons_sl=0(;0_sl=0()),
      filter_sl=0(cons_sl=0(;X),0_sl=0(),M;) -> cons_sl=0(;0_sl=0()),
    filter_sl=0(cons_sl=0(;X),s_sl=0(;N),M;) -> cons_sl=0(;X),
    filter_sl=0(cons_sl=0(;X),s_sl=0(;N),M;) -> cons_sl=0(;X),
    filter_sl=0(cons_sl=0(;X),s_sl=0(;N),M;) -> cons_sl=0(;X),
    filter_sl=0(cons_sl=0(;X),s_sl=0(;N),M;) -> cons_sl=0(;X),
    filter_sl=0(cons_sl=0(;X),s_sl=0(;N),M;) -> cons_sl=0(;X),
    filter_sl=0(cons_sl=0(;X),s_sl=0(;N),M;) -> cons_sl=0(;X),
    filter_sl=0(cons_sl=0(;X),s_sl=0(;N),M;) -> cons_sl=0(;X),
    filter_sl=0(cons_sl=0(;X),s_sl=0(;N),M;) -> cons_sl=0(;X),
           sieve_sl=0(cons_sl=0(;0_sl=0());) -> cons_sl=0(;0_sl=0()),
         sieve_sl=0(cons_sl=0(;s_sl=0(;N));) -> cons_sl=0(;s_sl=0(;N)),
         sieve_sl=0(cons_sl=0(;s_sl=0(;N));) -> cons_sl=0(;s_sl=0(;N)),
                               nats_sl=0(N;) -> cons_sl=0(;N),
                               nats_sl=0(N;) -> cons_sl=0(;N),
                              zprimes_sl=0() -> sieve_sl=0(nats_sl=0(s_sl=0(;s_sl=0(;0_sl=0())););)}
  

  Qed