YES
TRS:
 {             p(0()) -> 0(),
              p(s(x)) -> x,
         plus(x, 0()) -> x,
        plus(x, s(y)) -> s(plus(x, p(s(y)))),
         plus(0(), y) -> y,
        plus(s(x), y) -> s(plus(x, y)),
        plus(s(x), y) -> s(plus(p(s(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#(x, s(y)) -> p#(s(y)),
          plus#(x, s(y)) -> plus#(x, p(s(y))),
          plus#(s(x), y) -> p#(s(x)),
          plus#(s(x), y) -> plus#(x, y),
          plus#(s(x), y) -> plus#(p(s(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:
  {             p(0()) -> 0(),
               p(s(x)) -> x,
          plus(x, 0()) -> x,
         plus(x, s(y)) -> s(plus(x, p(s(y)))),
          plus(0(), y) -> y,
         plus(s(x), y) -> s(plus(x, y)),
         plus(s(x), y) -> s(plus(p(s(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:
   {(prime#(s(s(x))) -> pr#(s(s(x)), s(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)), pr#(x, s(s(y))) -> divides#(s(s(y)), x))
    (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)))
    (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))
    (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))
    (plus#(x, s(y)) -> plus#(x, p(s(y))), plus#(s(x), y) -> plus#(p(s(x)), y))
    (plus#(x, s(y)) -> plus#(x, p(s(y))), plus#(s(x), y) -> plus#(x, y))
    (plus#(x, s(y)) -> plus#(x, p(s(y))), plus#(s(x), y) -> p#(s(x)))
    (plus#(x, s(y)) -> plus#(x, p(s(y))), plus#(x, s(y)) -> plus#(x, p(s(y))))
    (plus#(x, s(y)) -> plus#(x, p(s(y))), plus#(x, s(y)) -> p#(s(y)))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(p(s(x)), y))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> p#(s(x)))
    (plus#(s(x), y) -> plus#(x, y), plus#(x, s(y)) -> plus#(x, p(s(y))))
    (plus#(s(x), y) -> plus#(x, y), plus#(x, s(y)) -> p#(s(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)))
    (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))
    (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))
    (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#(x, s(y)) -> p#(s(y)))
    (times#(s(x), y) -> plus#(y, times(x, y)), plus#(x, s(y)) -> plus#(x, p(s(y))))
    (times#(s(x), y) -> plus#(y, times(x, y)), plus#(s(x), y) -> p#(s(x)))
    (times#(s(x), y) -> plus#(y, times(x, y)), plus#(s(x), y) -> plus#(x, y))
    (times#(s(x), y) -> plus#(y, times(x, y)), plus#(s(x), y) -> plus#(p(s(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))
    (plus#(s(x), y) -> plus#(p(s(x)), y), plus#(x, s(y)) -> p#(s(y)))
    (plus#(s(x), y) -> plus#(p(s(x)), y), plus#(x, s(y)) -> plus#(x, p(s(y))))
    (plus#(s(x), y) -> plus#(p(s(x)), y), plus#(s(x), y) -> p#(s(x)))
    (plus#(s(x), y) -> plus#(p(s(x)), y), plus#(s(x), y) -> plus#(x, y))
    (plus#(s(x), y) -> plus#(p(s(x)), y), plus#(s(x), y) -> plus#(p(s(x)), y))
    (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) -> times#(y, z))
    (quot#(x, 0(), s(z)) -> div#(x, s(z)), div#(div(x, y), z) -> div#(x, times(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#(x, s(y)) -> plus#(x, p(s(y))),
      plus#(s(x), y) -> plus#(x, y),
      plus#(s(x), y) -> plus#(p(s(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:
     {             p(0()) -> 0(),
                  p(s(x)) -> x,
             plus(x, 0()) -> x,
            plus(x, s(y)) -> s(plus(x, p(s(y)))),
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            plus(s(x), y) -> s(plus(p(s(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:
     {             p(0()) -> 0(),
                  p(s(x)) -> x,
             plus(x, 0()) -> x,
            plus(x, s(y)) -> s(plus(x, p(s(y)))),
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            plus(s(x), y) -> s(plus(p(s(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:
     {             p(0()) -> 0(),
                  p(s(x)) -> x,
             plus(x, 0()) -> x,
            plus(x, s(y)) -> s(plus(x, p(s(y)))),
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            plus(s(x), y) -> s(plus(p(s(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:
         {             p(0()) -> 0(),
                      p(s(x)) -> x,
                 plus(x, 0()) -> x,
                plus(x, s(y)) -> s(plus(x, p(s(y)))),
                 plus(0(), y) -> y,
                plus(s(x), y) -> s(plus(x, y)),
                plus(s(x), y) -> s(plus(p(s(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:
             {             p(0()) -> 0(),
                          p(s(x)) -> x,
                     plus(x, 0()) -> x,
                    plus(x, s(y)) -> s(plus(x, p(s(y)))),
                     plus(0(), y) -> y,
                    plus(s(x), y) -> s(plus(x, y)),
                    plus(s(x), y) -> s(plus(p(s(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(plus) = [], pi(s) = [], pi(p) = [], pi(0) = []
              Usable Rules:
               {}
              Interpretation:
               [quot#](x0) = x0 + 1,
               [div#](x0) = x0 + 1,
               [s] = 0,
               [0] = 1
              Strict:
               {div#(x, y) -> quot#(x, y, y)}
              Weak:
               {             p(0()) -> 0(),
                            p(s(x)) -> x,
                       plus(x, 0()) -> x,
                      plus(x, s(y)) -> s(plus(x, p(s(y)))),
                       plus(0(), y) -> y,
                      plus(s(x), y) -> s(plus(x, y)),
                      plus(s(x), y) -> s(plus(p(s(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:
     {             p(0()) -> 0(),
                  p(s(x)) -> x,
             plus(x, 0()) -> x,
            plus(x, s(y)) -> s(plus(x, p(s(y)))),
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            plus(s(x), y) -> s(plus(p(s(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#(x, s(y)) -> plus#(x, p(s(y))),
       plus#(s(x), y) -> plus#(x, y),
       plus#(s(x), y) -> plus#(p(s(x)), y)}
     Weak:
     {             p(0()) -> 0(),
                  p(s(x)) -> x,
             plus(x, 0()) -> x,
            plus(x, s(y)) -> s(plus(x, p(s(y)))),
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
            plus(s(x), y) -> s(plus(p(s(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) = [], pi(div) = [], pi(times) = [], pi(plus#) = 0, pi(plus) = [], pi(s) = [0], pi(p) = 0, pi(0) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {plus#(x, s(y)) -> plus#(x, p(s(y))),
        plus#(s(x), y) -> plus#(p(s(x)), y)}
      Weak:
       {             p(0()) -> 0(),
                    p(s(x)) -> x,
               plus(x, 0()) -> x,
              plus(x, s(y)) -> s(plus(x, p(s(y)))),
               plus(0(), y) -> y,
              plus(s(x), y) -> s(plus(x, y)),
              plus(s(x), y) -> s(plus(p(s(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:
       {(plus#(s(x), y) -> plus#(p(s(x)), y), plus#(s(x), y) -> plus#(p(s(x)), y))
        (plus#(s(x), y) -> plus#(p(s(x)), y), plus#(x, s(y)) -> plus#(x, p(s(y))))
        (plus#(x, s(y)) -> plus#(x, p(s(y))), plus#(x, s(y)) -> plus#(x, p(s(y))))
        (plus#(x, s(y)) -> plus#(x, p(s(y))), plus#(s(x), y) -> plus#(p(s(x)), y))}
       SCCS:
        Scc:
         {plus#(x, s(y)) -> plus#(x, p(s(y))),
          plus#(s(x), y) -> plus#(p(s(x)), y)}
        SCC:
         Strict:
          {plus#(x, s(y)) -> plus#(x, p(s(y))),
           plus#(s(x), y) -> plus#(p(s(x)), y)}
         Weak:
         {             p(0()) -> 0(),
                      p(s(x)) -> x,
                 plus(x, 0()) -> x,
                plus(x, s(y)) -> s(plus(x, p(s(y)))),
                 plus(0(), y) -> y,
                plus(s(x), y) -> s(plus(x, y)),
                plus(s(x), y) -> s(plus(p(s(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)}
         UR:
          {p(s(x)) -> x}
          BOUND:
           Bound: match(-raise)-bounded by 1
           Automaton:
            {plus#_1(3, 3) -> 1*
             plus#_1(3, 1) -> 1*
             plus#_1(1, 3) -> 1*
             plus#_0(1, 1) -> 1*
                    s_1(1) -> 2*
                    s_0(1) -> 1*
                    p_1(2) -> 3*
                    p_0(1) -> 1*
                         1 -> 3*}
           Strict:
            {}
           Qed