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())}
 MPO:
  Prec:
   prime > prime1, 
   prime > false, 
   prime1 > divp, 
   prime1 > not, 
   prime1 > and, 
   prime1 > true, 
   prime1 > false, 
   divp > rem, 
   divp > =, 
   divp > 0
   empty
  Strict:
   {}
   Weak:
    {}
  Qed