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*:
  Precedence:
  prime > prime1, 
  prime > false, 
  prime1 > divp, 
  prime1 > not, 
  prime1 > and, 
  prime1 > true, 
  prime1 > false, 
  divp > rem, 
  divp > =, 
  divp > 0
  empty
  
Normal:
   pi(divp) = [1,2], pi(prime1) = [1,2], pi(prime) = [1]
  
Safe:
   pi(rem) = [1,2], pi(=) = [1,2], pi(not) = [1], pi(and) = [1,2], pi(s) = [1]
  
Predicative System:
   {         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())}
  Qed