TRS:
 {        prime(0()) -> false(),
       prime(s(0())) -> false(),
      prime(s(s(x))) -> prime1(s(s(x)), s(x)),
      prime1(x, 0()) -> false(),
   prime1(x, s(0())) -> true(),
  prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y))),
          divp(x, y) -> =(rem(x, y), 0())}
 POP* + Boolean Semantic Labelling:
  Normal positions:
  pi(divp_sl=1) = [1,2], pi(divp_sl=0) = [1,2], pi(prime1_sl=1) = [1,2], pi(prime1_sl=0) = [1,2], pi(prime_sl=1) = [1], pi(prime_sl=0) = [1]
  
Safe positions:
   pi(rem_sl=1) = [1,2], pi(rem_sl=0) = [1,2], pi(=_sl=1) = [1,2], pi(=_sl=0) = [1,2], pi(not_sl=1) = [1], pi(not_sl=0) = [1], pi(and_sl=1) = [1,2], pi(and_sl=0) = [1,2], pi(s_sl=1) = [1], pi(s_sl=0) = [1]
  
Precedence:
   prime_sl=0 > prime1_sl=0, 
   prime_sl=0 > false_sl=0, 
   prime1_sl=0 > divp_sl=0, 
   prime1_sl=0 > not_sl=0, 
   prime1_sl=0 > and_sl=0, 
   prime1_sl=0 > true_sl=0, 
   prime1_sl=0 > false_sl=0, 
   divp_sl=0 > rem_sl=0, 
   divp_sl=0 > =_sl=0, 
   divp_sl=0 > 0_sl=1
   empty
  
Interpretation:
   false^(0):
    | 0
   prime^(1):
   0 | 0
   1 | 0
   0^(0):
    | 0
   s^(1):
   0 | 0
   1 | 0
   prime1^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   true^(0):
    | 0
   and^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   not^(1):
   0 | 0
   1 | 0
   divp^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   =^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   rem^(2):
   00 | 0
   01 | 1
   10 | 1
   11 | 1
   
  
Labelling:
   false^(0):
    | 0
   prime^(1):
   0 | 0
   1 | 0
   0^(0):
    | 1
   s^(1):
   0 | 0
   1 | 0
   prime1^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   true^(0):
    | 0
   and^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   not^(1):
   0 | 0
   1 | 0
   divp^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   =^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   rem^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   
  
Labelled predicative System:
   {              prime_sl=0(0_sl=1();) -> false_sl=0(),
         prime_sl=0(s_sl=0(;0_sl=1());) -> false_sl=0(),
       prime_sl=0(s_sl=0(;s_sl=0(;x));) -> prime1_sl=0(s_sl=0(;s_sl=0(;x)),s_sl=0(;x);),
       prime_sl=0(s_sl=0(;s_sl=0(;x));) -> prime1_sl=0(s_sl=0(;s_sl=0(;x)),s_sl=0(;x);),
               prime1_sl=0(x,0_sl=1();) -> false_sl=0(),
               prime1_sl=0(x,0_sl=1();) -> false_sl=0(),
      prime1_sl=0(x,s_sl=0(;0_sl=1());) -> true_sl=0(),
      prime1_sl=0(x,s_sl=0(;0_sl=1());) -> true_sl=0(),
    prime1_sl=0(x,s_sl=0(;s_sl=0(;y));) -> and_sl=0(;not_sl=0(;divp_sl=0(s_sl=0(;s_sl=0(;y)),x;)),prime1_sl=0(x,s_sl=0(;y);)),
    prime1_sl=0(x,s_sl=0(;s_sl=0(;y));) -> and_sl=0(;not_sl=0(;divp_sl=0(s_sl=0(;s_sl=0(;y)),x;)),prime1_sl=0(x,s_sl=0(;y);)),
    prime1_sl=0(x,s_sl=0(;s_sl=0(;y));) -> and_sl=0(;not_sl=0(;divp_sl=0(s_sl=0(;s_sl=0(;y)),x;)),prime1_sl=0(x,s_sl=0(;y);)),
    prime1_sl=0(x,s_sl=0(;s_sl=0(;y));) -> and_sl=0(;not_sl=0(;divp_sl=0(s_sl=0(;s_sl=0(;y)),x;)),prime1_sl=0(x,s_sl=0(;y);)),
                        divp_sl=0(x,y;) -> =_sl=0(;rem_sl=0(;x,y),0_sl=1()),
                        divp_sl=0(x,y;) -> =_sl=0(;rem_sl=0(;x,y),0_sl=1()),
                        divp_sl=0(x,y;) -> =_sl=0(;rem_sl=0(;x,y),0_sl=1()),
                        divp_sl=0(x,y;) -> =_sl=0(;rem_sl=0(;x,y),0_sl=1())}
  

  Qed