YES
Time: 0.043461
TRS:
 {                  minus(x, 0()) -> x,
            minus(minus(x, y), z) -> minus(x, plus(y, z)),
                  minus(s x, s y) -> minus(x, y),
                   quot(0(), s y) -> 0(),
                   quot(s x, s y) -> s quot(minus(x, y), s y),
                     plus(0(), y) -> y,
                     plus(s x, y) -> s plus(x, y),
                    app(l, nil()) -> l,
                    app(nil(), k) -> k,
               app(cons(x, l), k) -> cons(x, app(l, k)),
  sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
               sum cons(x, nil()) -> cons(x, nil()),
          sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)}
 DP:
  DP:
   {          minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
              minus#(minus(x, y), z) -> plus#(y, z),
                    minus#(s x, s y) -> minus#(x, y),
                     quot#(s x, s y) -> minus#(x, y),
                     quot#(s x, s y) -> quot#(minus(x, y), s y),
                       plus#(s x, y) -> plus#(x, y),
                 app#(cons(x, l), k) -> app#(l, k),
    sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))),
    sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))),
    sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)),
            sum# cons(x, cons(y, l)) -> plus#(x, y),
            sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
  TRS:
  {                  minus(x, 0()) -> x,
             minus(minus(x, y), z) -> minus(x, plus(y, z)),
                   minus(s x, s y) -> minus(x, y),
                    quot(0(), s y) -> 0(),
                    quot(s x, s y) -> s quot(minus(x, y), s y),
                      plus(0(), y) -> y,
                      plus(s x, y) -> s plus(x, y),
                     app(l, nil()) -> l,
                     app(nil(), k) -> k,
                app(cons(x, l), k) -> cons(x, app(l, k)),
   sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                sum cons(x, nil()) -> cons(x, nil()),
           sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)}
  EDG:
   {(sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
    (sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(s x, s y) -> minus#(x, y))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> plus#(y, z))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
    (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# app(l, cons(x, cons(y, k))) -> sum# cons(x, cons(y, k)))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))))
    (sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k))), sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))))
    (sum# cons(x, cons(y, l)) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
    (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, y) -> plus#(x, y))
    (sum# app(l, cons(x, cons(y, k))) -> app#(l, sum cons(x, cons(y, k))), app#(cons(x, l), k) -> app#(l, k))
    (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# cons(x, cons(y, l)) -> plus#(x, y))
    (sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l), sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l))
    (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
    (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))}
   SCCS (6):
    Scc:
     {sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
    Scc:
     {sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))}
    Scc:
     {app#(cons(x, l), k) -> app#(l, k)}
    Scc:
     {plus#(s x, y) -> plus#(x, y)}
    Scc:
     {quot#(s x, s y) -> quot#(minus(x, y), s y)}
    Scc:
     {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
            minus#(s x, s y) -> minus#(x, y)}
    SCC (1):
     Strict:
      {sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
     Weak:
     {                  minus(x, 0()) -> x,
                minus(minus(x, y), z) -> minus(x, plus(y, z)),
                      minus(s x, s y) -> minus(x, y),
                       quot(0(), s y) -> 0(),
                       quot(s x, s y) -> s quot(minus(x, y), s y),
                         plus(0(), y) -> y,
                         plus(s x, y) -> s plus(x, y),
                        app(l, nil()) -> l,
                        app(nil(), k) -> k,
                   app(cons(x, l), k) -> cons(x, app(l, k)),
      sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                   sum cons(x, nil()) -> cons(x, nil()),
              sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [minus](x0, x1) = x0 + x1 + 1,
       
       [quot](x0, x1) = x0 + 1,
       
       [plus](x0, x1) = x0 + 1,
       
       [app](x0, x1) = x0 + x1 + 1,
       
       [cons](x0, x1) = x0 + 1,
       
       [s](x0) = 0,
       
       [sum](x0) = x0,
       
       [0] = 1,
       
       [nil] = 1,
       
       [sum#](x0) = x0
      Strict:
       sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)
       2 + 0x + 0y + 1l >= 1 + 0x + 0y + 1l
      Weak:
       
     Qed
   SCC (1):
    Strict:
     {sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))}
    Weak:
    {                  minus(x, 0()) -> x,
               minus(minus(x, y), z) -> minus(x, plus(y, z)),
                     minus(s x, s y) -> minus(x, y),
                      quot(0(), s y) -> 0(),
                      quot(s x, s y) -> s quot(minus(x, y), s y),
                        plus(0(), y) -> y,
                        plus(s x, y) -> s plus(x, y),
                       app(l, nil()) -> l,
                       app(nil(), k) -> k,
                  app(cons(x, l), k) -> cons(x, app(l, k)),
     sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                  sum cons(x, nil()) -> cons(x, nil()),
             sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [minus](x0, x1) = 1,
      
      [quot](x0, x1) = x0 + x1 + 1,
      
      [plus](x0, x1) = 0,
      
      [app](x0, x1) = x0 + x1,
      
      [cons](x0, x1) = x0 + 1,
      
      [s](x0) = 1,
      
      [sum](x0) = 1,
      
      [0] = 0,
      
      [nil] = 0,
      
      [sum#](x0) = x0
     Strict:
      sum# app(l, cons(x, cons(y, k))) -> sum# app(l, sum cons(x, cons(y, k)))
      2 + 0x + 0y + 1k + 1l >= 1 + 0x + 0y + 0k + 1l
     Weak:
      
    Qed
   SCC (1):
    Strict:
     {app#(cons(x, l), k) -> app#(l, k)}
    Weak:
    {                  minus(x, 0()) -> x,
               minus(minus(x, y), z) -> minus(x, plus(y, z)),
                     minus(s x, s y) -> minus(x, y),
                      quot(0(), s y) -> 0(),
                      quot(s x, s y) -> s quot(minus(x, y), s y),
                        plus(0(), y) -> y,
                        plus(s x, y) -> s plus(x, y),
                       app(l, nil()) -> l,
                       app(nil(), k) -> k,
                  app(cons(x, l), k) -> cons(x, app(l, k)),
     sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                  sum cons(x, nil()) -> cons(x, nil()),
             sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)}
    SPSC:
     Simple Projection:
      pi(app#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {plus#(s x, y) -> plus#(x, y)}
    Weak:
    {                  minus(x, 0()) -> x,
               minus(minus(x, y), z) -> minus(x, plus(y, z)),
                     minus(s x, s y) -> minus(x, y),
                      quot(0(), s y) -> 0(),
                      quot(s x, s y) -> s quot(minus(x, y), s y),
                        plus(0(), y) -> y,
                        plus(s x, y) -> s plus(x, y),
                       app(l, nil()) -> l,
                       app(nil(), k) -> k,
                  app(cons(x, l), k) -> cons(x, app(l, k)),
     sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                  sum cons(x, nil()) -> cons(x, nil()),
             sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)}
    SPSC:
     Simple Projection:
      pi(plus#) = 0
     Strict:
      {}
     Qed
   SCC (1):
    Strict:
     {quot#(s x, s y) -> quot#(minus(x, y), s y)}
    Weak:
    {                  minus(x, 0()) -> x,
               minus(minus(x, y), z) -> minus(x, plus(y, z)),
                     minus(s x, s y) -> minus(x, y),
                      quot(0(), s y) -> 0(),
                      quot(s x, s y) -> s quot(minus(x, y), s y),
                        plus(0(), y) -> y,
                        plus(s x, y) -> s plus(x, y),
                       app(l, nil()) -> l,
                       app(nil(), k) -> k,
                  app(cons(x, l), k) -> cons(x, app(l, k)),
     sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                  sum cons(x, nil()) -> cons(x, nil()),
             sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [minus](x0, x1) = x0,
      
      [quot](x0, x1) = x0 + 1,
      
      [plus](x0, x1) = x0 + 1,
      
      [app](x0, x1) = x0 + x1 + 1,
      
      [cons](x0, x1) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [sum](x0) = 0,
      
      [0] = 1,
      
      [nil] = 1,
      
      [quot#](x0, x1) = x0 + 1
     Strict:
      quot#(s x, s y) -> quot#(minus(x, y), s y)
      2 + 1x + 0y >= 1 + 1x + 0y
     Weak:
      
    Qed
  SCC (2):
   Strict:
    {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
           minus#(s x, s y) -> minus#(x, y)}
   Weak:
   {                  minus(x, 0()) -> x,
              minus(minus(x, y), z) -> minus(x, plus(y, z)),
                    minus(s x, s y) -> minus(x, y),
                     quot(0(), s y) -> 0(),
                     quot(s x, s y) -> s quot(minus(x, y), s y),
                       plus(0(), y) -> y,
                       plus(s x, y) -> s plus(x, y),
                      app(l, nil()) -> l,
                      app(nil(), k) -> k,
                 app(cons(x, l), k) -> cons(x, app(l, k)),
    sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                 sum cons(x, nil()) -> cons(x, nil()),
            sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)}
   SPSC:
    Simple Projection:
     pi(minus#) = 0
    Strict:
     {minus#(s x, s y) -> minus#(x, y)}
    EDG:
     {(minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))}
     SCCS (1):
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      SCC (1):
       Strict:
        {minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {                  minus(x, 0()) -> x,
                  minus(minus(x, y), z) -> minus(x, plus(y, z)),
                        minus(s x, s y) -> minus(x, y),
                         quot(0(), s y) -> 0(),
                         quot(s x, s y) -> s quot(minus(x, y), s y),
                           plus(0(), y) -> y,
                           plus(s x, y) -> s plus(x, y),
                          app(l, nil()) -> l,
                          app(nil(), k) -> k,
                     app(cons(x, l), k) -> cons(x, app(l, k)),
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k))),
                     sum cons(x, nil()) -> cons(x, nil()),
                sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)}
       SPSC:
        Simple Projection:
         pi(minus#) = 1
        Strict:
         {}
        Qed