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())}
 LMPO:
  Quasi-Precedence:
  prime > prime1, 
  prime1 > divp, 
  prime1 > not
  empty
  
Normal:
   pi(divp) = [1,2], pi(prime1) = [1,2], pi(prime) = [1]
  
Safe:
   
  
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