YES
Time: 0.000944
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())}
 DP:
  DP:
   {     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())}
  EDG:
   {(prime# s s x -> prime1#(s s x, s x), prime1#(x, s s y) -> divp#(s s y, x))
    (prime# s s x -> prime1#(s s x, s x), prime1#(x, s s y) -> prime1#(x, s y))
    (prime1#(x, s s y) -> prime1#(x, s y), prime1#(x, s s y) -> prime1#(x, s y))
    (prime1#(x, s s y) -> prime1#(x, s y), prime1#(x, s s y) -> divp#(s s y, x))}
   SCCS (1):
    Scc:
     {prime1#(x, s s y) -> prime1#(x, s y)}
    SCC (1):
     Strict:
      {prime1#(x, s s y) -> prime1#(x, s y)}
     Weak:
     {       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())}
     SPSC:
      Simple Projection:
       pi(prime1#) = 1
      Strict:
       {}
      Qed