YES
TRS:
 {       plus(x, 0()) -> x,
         plus(0(), y) -> y,
        plus(s(x), y) -> s(plus(x, y)),
        times(0(), y) -> 0(),
       times(s(x), y) -> plus(y, times(x, y)),
     times(s(0()), y) -> y,
            div(x, y) -> quot(x, y, y),
          div(0(), y) -> 0(),
    div(div(x, y), z) -> div(x, times(y, z)),
   quot(x, 0(), s(z)) -> s(div(x, s(z))),
   quot(0(), s(y), z) -> 0(),
  quot(s(x), s(y), z) -> quot(x, y, z),
         eq(0(), 0()) -> true(),
        eq(0(), s(y)) -> false(),
        eq(s(x), 0()) -> false(),
       eq(s(x), s(y)) -> eq(x, y),
        divides(y, x) -> eq(x, times(div(x, y), y)),
        pr(x, s(0())) -> true(),
       pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
       prime(s(s(x))) -> pr(s(s(x)), s(x)),
     if(true(), x, y) -> false(),
    if(false(), x, y) -> pr(x, y)}
 DP:
  Strict:
   {      plus#(s(x), y) -> plus#(x, y),
         times#(s(x), y) -> plus#(y, times(x, y)),
         times#(s(x), y) -> times#(x, y),
              div#(x, y) -> quot#(x, y, y),
      div#(div(x, y), z) -> times#(y, z),
      div#(div(x, y), z) -> div#(x, times(y, z)),
     quot#(x, 0(), s(z)) -> div#(x, s(z)),
    quot#(s(x), s(y), z) -> quot#(x, y, z),
         eq#(s(x), s(y)) -> eq#(x, y),
          divides#(y, x) -> times#(div(x, y), y),
          divides#(y, x) -> div#(x, y),
          divides#(y, x) -> eq#(x, times(div(x, y), y)),
         pr#(x, s(s(y))) -> divides#(s(s(y)), x),
         pr#(x, s(s(y))) -> if#(divides(s(s(y)), x), x, s(y)),
         prime#(s(s(x))) -> pr#(s(s(x)), s(x)),
      if#(false(), x, y) -> pr#(x, y)}
  Weak:
  {       plus(x, 0()) -> x,
          plus(0(), y) -> y,
         plus(s(x), y) -> s(plus(x, y)),
         times(0(), y) -> 0(),
        times(s(x), y) -> plus(y, times(x, y)),
      times(s(0()), y) -> y,
             div(x, y) -> quot(x, y, y),
           div(0(), y) -> 0(),
     div(div(x, y), z) -> div(x, times(y, z)),
    quot(x, 0(), s(z)) -> s(div(x, s(z))),
    quot(0(), s(y), z) -> 0(),
   quot(s(x), s(y), z) -> quot(x, y, z),
          eq(0(), 0()) -> true(),
         eq(0(), s(y)) -> false(),
         eq(s(x), 0()) -> false(),
        eq(s(x), s(y)) -> eq(x, y),
         divides(y, x) -> eq(x, times(div(x, y), y)),
         pr(x, s(0())) -> true(),
        pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
        prime(s(s(x))) -> pr(s(s(x)), s(x)),
      if(true(), x, y) -> false(),
     if(false(), x, y) -> pr(x, y)}
  EDG:
   {(pr#(x, s(s(y))) -> divides#(s(s(y)), x), divides#(y, x) -> eq#(x, times(div(x, y), y)))
    (pr#(x, s(s(y))) -> divides#(s(s(y)), x), divides#(y, x) -> div#(x, y))
    (pr#(x, s(s(y))) -> divides#(s(s(y)), x), divides#(y, x) -> times#(div(x, y), y))
    (quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(div(x, y), z) -> div#(x, times(y, z)))
    (quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(div(x, y), z) -> times#(y, z))
    (quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(x, y) -> quot#(x, y, y))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (eq#(s(x), s(y)) -> eq#(x, y), eq#(s(x), s(y)) -> eq#(x, y))
    (pr#(x, s(s(y))) -> if#(divides(s(s(y)), x), x, s(y)), if#(false(), x, y) -> pr#(x, y))
    (quot#(s(x), s(y), z) -> quot#(x, y, z), quot#(s(x), s(y), z) -> quot#(x, y, z))
    (quot#(s(x), s(y), z) -> quot#(x, y, z), quot#(x, 0(), s(z)) -> div#(x, s(z)))
    (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> div#(x, times(y, z)))
    (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> times#(y, z))
    (div#(div(x, y), z) -> div#(x, times(y, z)), div#(x, y) -> quot#(x, y, y))
    (divides#(y, x) -> times#(div(x, y), y), times#(s(x), y) -> times#(x, y))
    (divides#(y, x) -> times#(div(x, y), y), times#(s(x), y) -> plus#(y, times(x, y)))
    (divides#(y, x) -> eq#(x, times(div(x, y), y)), eq#(s(x), s(y)) -> eq#(x, y))
    (times#(s(x), y) -> plus#(y, times(x, y)), plus#(s(x), y) -> plus#(x, y))
    (if#(false(), x, y) -> pr#(x, y), pr#(x, s(s(y))) -> divides#(s(s(y)), x))
    (if#(false(), x, y) -> pr#(x, y), pr#(x, s(s(y))) -> if#(divides(s(s(y)), x), x, s(y)))
    (divides#(y, x) -> div#(x, y), div#(x, y) -> quot#(x, y, y))
    (divides#(y, x) -> div#(x, y), div#(div(x, y), z) -> times#(y, z))
    (divides#(y, x) -> div#(x, y), div#(div(x, y), z) -> div#(x, times(y, z)))
    (times#(s(x), y) -> times#(x, y), times#(s(x), y) -> plus#(y, times(x, y)))
    (times#(s(x), y) -> times#(x, y), times#(s(x), y) -> times#(x, y))
    (prime#(s(s(x))) -> pr#(s(s(x)), s(x)), pr#(x, s(s(y))) -> divides#(s(s(y)), x))
    (prime#(s(s(x))) -> pr#(s(s(x)), s(x)), pr#(x, s(s(y))) -> if#(divides(s(s(y)), x), x, s(y)))
    (div#(div(x, y), z) -> times#(y, z), times#(s(x), y) -> plus#(y, times(x, y)))
    (div#(div(x, y), z) -> times#(y, z), times#(s(x), y) -> times#(x, y))
    (div#(x, y) -> quot#(x, y, y), quot#(x, 0(), s(z)) -> div#(x, s(z)))
    (div#(x, y) -> quot#(x, y, y), quot#(s(x), s(y), z) -> quot#(x, y, z))}
   SCCS:
    Scc:
     {   pr#(x, s(s(y))) -> if#(divides(s(s(y)), x), x, s(y)),
      if#(false(), x, y) -> pr#(x, y)}
    Scc:
     {eq#(s(x), s(y)) -> eq#(x, y)}
    Scc:
     {          div#(x, y) -> quot#(x, y, y),
        div#(div(x, y), z) -> div#(x, times(y, z)),
       quot#(x, 0(), s(z)) -> div#(x, s(z)),
      quot#(s(x), s(y), z) -> quot#(x, y, z)}
    Scc:
     {times#(s(x), y) -> times#(x, y)}
    Scc:
     {plus#(s(x), y) -> plus#(x, y)}
    SCC:
     Strict:
      {   pr#(x, s(s(y))) -> if#(divides(s(s(y)), x), x, s(y)),
       if#(false(), x, y) -> pr#(x, y)}
     Weak:
     {       plus(x, 0()) -> x,
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            times(0(), y) -> 0(),
           times(s(x), y) -> plus(y, times(x, y)),
         times(s(0()), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
       quot(x, 0(), s(z)) -> s(div(x, s(z))),
       quot(0(), s(y), z) -> 0(),
      quot(s(x), s(y), z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
            eq(0(), s(y)) -> false(),
            eq(s(x), 0()) -> false(),
           eq(s(x), s(y)) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
            pr(x, s(0())) -> true(),
           pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
           prime(s(s(x))) -> pr(s(s(x)), s(x)),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
     SPSC:
      Simple Projection:
       pi(if#) = 2, pi(pr#) = 1
      Strict:
       {if#(false(), x, y) -> pr#(x, y)}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {eq#(s(x), s(y)) -> eq#(x, y)}
     Weak:
     {       plus(x, 0()) -> x,
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            times(0(), y) -> 0(),
           times(s(x), y) -> plus(y, times(x, y)),
         times(s(0()), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
       quot(x, 0(), s(z)) -> s(div(x, s(z))),
       quot(0(), s(y), z) -> 0(),
      quot(s(x), s(y), z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
            eq(0(), s(y)) -> false(),
            eq(s(x), 0()) -> false(),
           eq(s(x), s(y)) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
            pr(x, s(0())) -> true(),
           pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
           prime(s(s(x))) -> pr(s(s(x)), s(x)),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
     SPSC:
      Simple Projection:
       pi(eq#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {          div#(x, y) -> quot#(x, y, y),
         div#(div(x, y), z) -> div#(x, times(y, z)),
        quot#(x, 0(), s(z)) -> div#(x, s(z)),
       quot#(s(x), s(y), z) -> quot#(x, y, z)}
     Weak:
     {       plus(x, 0()) -> x,
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            times(0(), y) -> 0(),
           times(s(x), y) -> plus(y, times(x, y)),
         times(s(0()), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
       quot(x, 0(), s(z)) -> s(div(x, s(z))),
       quot(0(), s(y), z) -> 0(),
      quot(s(x), s(y), z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
            eq(0(), s(y)) -> false(),
            eq(s(x), 0()) -> false(),
           eq(s(x), s(y)) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
            pr(x, s(0())) -> true(),
           pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
           prime(s(s(x))) -> pr(s(s(x)), s(x)),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
     SPSC:
      Simple Projection:
       pi(quot#) = 0, pi(div#) = 0
      Strict:
       {         div#(x, y) -> quot#(x, y, y),
         div#(div(x, y), z) -> div#(x, times(y, z)),
        quot#(x, 0(), s(z)) -> div#(x, s(z))}
      EDG:
       {(div#(x, y) -> quot#(x, y, y), quot#(x, 0(), s(z)) -> div#(x, s(z)))
        (quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(x, y) -> quot#(x, y, y))
        (quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(div(x, y), z) -> div#(x, times(y, z)))
        (div#(div(x, y), z) -> div#(x, times(y, z)), div#(x, y) -> quot#(x, y, y))
        (div#(div(x, y), z) -> div#(x, times(y, z)), div#(div(x, y), z) -> div#(x, times(y, z)))}
       SCCS:
        Scc:
         {         div#(x, y) -> quot#(x, y, y),
           div#(div(x, y), z) -> div#(x, times(y, z)),
          quot#(x, 0(), s(z)) -> div#(x, s(z))}
        SCC:
         Strict:
          {         div#(x, y) -> quot#(x, y, y),
            div#(div(x, y), z) -> div#(x, times(y, z)),
           quot#(x, 0(), s(z)) -> div#(x, s(z))}
         Weak:
         {       plus(x, 0()) -> x,
                 plus(0(), y) -> y,
                plus(s(x), y) -> s(plus(x, y)),
                times(0(), y) -> 0(),
               times(s(x), y) -> plus(y, times(x, y)),
             times(s(0()), y) -> y,
                    div(x, y) -> quot(x, y, y),
                  div(0(), y) -> 0(),
            div(div(x, y), z) -> div(x, times(y, z)),
           quot(x, 0(), s(z)) -> s(div(x, s(z))),
           quot(0(), s(y), z) -> 0(),
          quot(s(x), s(y), z) -> quot(x, y, z),
                 eq(0(), 0()) -> true(),
                eq(0(), s(y)) -> false(),
                eq(s(x), 0()) -> false(),
               eq(s(x), s(y)) -> eq(x, y),
                divides(y, x) -> eq(x, times(div(x, y), y)),
                pr(x, s(0())) -> true(),
               pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
               prime(s(s(x))) -> pr(s(s(x)), s(x)),
             if(true(), x, y) -> false(),
            if(false(), x, y) -> pr(x, y)}
         SPSC:
          Simple Projection:
           pi(quot#) = 0, pi(div#) = 0
          Strict:
           {         div#(x, y) -> quot#(x, y, y),
            quot#(x, 0(), s(z)) -> div#(x, s(z))}
          EDG:
           {(quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(x, y) -> quot#(x, y, y))
            (div#(x, y) -> quot#(x, y, y), quot#(x, 0(), s(z)) -> div#(x, s(z)))}
           SCCS:
            Scc:
             {         div#(x, y) -> quot#(x, y, y),
              quot#(x, 0(), s(z)) -> div#(x, s(z))}
            SCC:
             Strict:
              {         div#(x, y) -> quot#(x, y, y),
               quot#(x, 0(), s(z)) -> div#(x, s(z))}
             Weak:
             {       plus(x, 0()) -> x,
                     plus(0(), y) -> y,
                    plus(s(x), y) -> s(plus(x, y)),
                    times(0(), y) -> 0(),
                   times(s(x), y) -> plus(y, times(x, y)),
                 times(s(0()), y) -> y,
                        div(x, y) -> quot(x, y, y),
                      div(0(), y) -> 0(),
                div(div(x, y), z) -> div(x, times(y, z)),
               quot(x, 0(), s(z)) -> s(div(x, s(z))),
               quot(0(), s(y), z) -> 0(),
              quot(s(x), s(y), z) -> quot(x, y, z),
                     eq(0(), 0()) -> true(),
                    eq(0(), s(y)) -> false(),
                    eq(s(x), 0()) -> false(),
                   eq(s(x), s(y)) -> eq(x, y),
                    divides(y, x) -> eq(x, times(div(x, y), y)),
                    pr(x, s(0())) -> true(),
                   pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
                   prime(s(s(x))) -> pr(s(s(x)), s(x)),
                 if(true(), x, y) -> false(),
                if(false(), x, y) -> pr(x, y)}
             POLY:
              Argument Filtering:
               pi(if) = [], pi(prime) = [], pi(pr) = [], pi(divides) = [], pi(false) = [], pi(eq) = [], pi(true) = [], pi(quot#) = 1, pi(quot) = [], pi(div#) = 1, pi(div) = [], pi(times) = [], pi(s) = [], pi(0) = [], pi(plus) = []
              Usable Rules:
               {}
              Interpretation:
               [s] = 0,
               [0] = 1
              Strict:
               {div#(x, y) -> quot#(x, y, y)}
              Weak:
               {       plus(x, 0()) -> x,
                       plus(0(), y) -> y,
                      plus(s(x), y) -> s(plus(x, y)),
                      times(0(), y) -> 0(),
                     times(s(x), y) -> plus(y, times(x, y)),
                   times(s(0()), y) -> y,
                          div(x, y) -> quot(x, y, y),
                        div(0(), y) -> 0(),
                  div(div(x, y), z) -> div(x, times(y, z)),
                 quot(x, 0(), s(z)) -> s(div(x, s(z))),
                 quot(0(), s(y), z) -> 0(),
                quot(s(x), s(y), z) -> quot(x, y, z),
                       eq(0(), 0()) -> true(),
                      eq(0(), s(y)) -> false(),
                      eq(s(x), 0()) -> false(),
                     eq(s(x), s(y)) -> eq(x, y),
                      divides(y, x) -> eq(x, times(div(x, y), y)),
                      pr(x, s(0())) -> true(),
                     pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
                     prime(s(s(x))) -> pr(s(s(x)), s(x)),
                   if(true(), x, y) -> false(),
                  if(false(), x, y) -> pr(x, y)}
              EDG:
               {}
               SCCS:
                
                Qed
    SCC:
     Strict:
      {times#(s(x), y) -> times#(x, y)}
     Weak:
     {       plus(x, 0()) -> x,
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            times(0(), y) -> 0(),
           times(s(x), y) -> plus(y, times(x, y)),
         times(s(0()), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
       quot(x, 0(), s(z)) -> s(div(x, s(z))),
       quot(0(), s(y), z) -> 0(),
      quot(s(x), s(y), z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
            eq(0(), s(y)) -> false(),
            eq(s(x), 0()) -> false(),
           eq(s(x), s(y)) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
            pr(x, s(0())) -> true(),
           pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
           prime(s(s(x))) -> pr(s(s(x)), s(x)),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
     SPSC:
      Simple Projection:
       pi(times#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {plus#(s(x), y) -> plus#(x, y)}
     Weak:
     {       plus(x, 0()) -> x,
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            times(0(), y) -> 0(),
           times(s(x), y) -> plus(y, times(x, y)),
         times(s(0()), y) -> y,
                div(x, y) -> quot(x, y, y),
              div(0(), y) -> 0(),
        div(div(x, y), z) -> div(x, times(y, z)),
       quot(x, 0(), s(z)) -> s(div(x, s(z))),
       quot(0(), s(y), z) -> 0(),
      quot(s(x), s(y), z) -> quot(x, y, z),
             eq(0(), 0()) -> true(),
            eq(0(), s(y)) -> false(),
            eq(s(x), 0()) -> false(),
           eq(s(x), s(y)) -> eq(x, y),
            divides(y, x) -> eq(x, times(div(x, y), y)),
            pr(x, s(0())) -> true(),
           pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y)),
           prime(s(s(x))) -> pr(s(s(x)), s(x)),
         if(true(), x, y) -> false(),
        if(false(), x, y) -> pr(x, y)}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {}
      Qed