YES

Problem:
 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())

Proof:
 DP Processor:
  DPs:
   prime#(s(s(x))) -> prime1#(s(s(x)),s(x))
   prime1#(x,s(s(y))) -> prime1#(x,s(y))
   prime1#(x,s(s(y))) -> divp#(s(s(y)),x)
  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())
  Usable Rule Processor:
   DPs:
    prime#(s(s(x))) -> prime1#(s(s(x)),s(x))
    prime1#(x,s(s(y))) -> prime1#(x,s(y))
    prime1#(x,s(s(y))) -> divp#(s(s(y)),x)
   TRS:
    
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     
    interpretation:
     [divp#](x0, x1) = 1,
     
     [prime1#](x0, x1) = 2x0 + x1 + 7,
     
     [prime#](x0) = 3x0 + 4,
     
     [s](x0) = 2x0 + 3
    orientation:
     prime#(s(s(x))) = 12x + 31 >= 10x + 28 = prime1#(s(s(x)),s(x))
     
     prime1#(x,s(s(y))) = 2x + 4y + 16 >= 2x + 2y + 10 = prime1#(x,s(y))
     
     prime1#(x,s(s(y))) = 2x + 4y + 16 >= 1 = divp#(s(s(y)),x)
    problem:
     DPs:
      
     TRS:
      
    Qed