YES
Time: 0.093623
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)}
  UR:
   {          minus(x, 0()) -> x,
      minus(minus(x, y), z) -> minus(x, plus(y, z)),
            minus(s x, s y) -> minus(x, 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 cons(x, nil()) -> cons(x, nil()),
    sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l),
                    a(w, v) -> w,
                    a(w, v) -> v}
   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))}
    STATUS:
     arrows: 0.826389
     SCCS (6):
      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:
       {sum# cons(x, cons(y, l)) -> sum# cons(plus(x, y), l)}
      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:
       {plus#(s x, y) -> plus#(x, y)}
      
      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:
         sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
         1 + 0x + 0y + 0l >= 1 + 0x + 0y + 0l
         sum cons(x, nil()) -> cons(x, nil())
         1 + 0x >= 1 + 0x
         sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
         1 + 0x + 0y + 0k + 0l >= 1 + 0x + 0y + 0k + 0l
         app(cons(x, l), k) -> cons(x, app(l, k))
         1 + 0x + 1k + 1l >= 1 + 0x + 1k + 1l
         app(nil(), k) -> k
         0 + 1k >= 1k
         app(l, nil()) -> l
         0 + 1l >= 1l
         plus(s x, y) -> s plus(x, y)
         0 + 0x + 0y >= 1 + 0x + 0y
         plus(0(), y) -> y
         0 + 0y >= 1y
         quot(s x, s y) -> s quot(minus(x, y), s y)
         3 + 0x + 0y >= 1 + 0x + 0y
         quot(0(), s y) -> 0()
         2 + 0y >= 0
         minus(s x, s y) -> minus(x, y)
         1 + 0x + 0y >= 1 + 0x + 0y
         minus(minus(x, y), z) -> minus(x, plus(y, z))
         1 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z
         minus(x, 0()) -> x
         1 + 0x >= 1x
       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)}
      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) = 0,
        
        [0] = 1,
        
        [nil] = 1,
        
        [app#](x0, x1) = x0
       Strict:
        app#(cons(x, l), k) -> app#(l, k)
        1 + 0x + 0k + 1l >= 0 + 0k + 1l
       Weak:
        sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
        0 + 0x + 0y + 0l >= 0 + 0x + 0y + 0l
        sum cons(x, nil()) -> cons(x, nil())
        0 + 0x >= 2 + 0x
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
        0 + 0x + 0y + 0k + 0l >= 0 + 0x + 0y + 0k + 0l
        app(cons(x, l), k) -> cons(x, app(l, k))
        2 + 0x + 1k + 1l >= 2 + 0x + 1k + 1l
        app(nil(), k) -> k
        2 + 1k >= 1k
        app(l, nil()) -> l
        2 + 1l >= 1l
        plus(s x, y) -> s plus(x, y)
        1 + 0x + 0y >= 0 + 0x + 0y
        plus(0(), y) -> y
        2 + 0y >= 1y
        quot(s x, s y) -> s quot(minus(x, y), s y)
        1 + 0x + 0y >= 0 + 0x + 0y
        quot(0(), s y) -> 0()
        2 + 0y >= 1
        minus(s x, s y) -> minus(x, y)
        1 + 0x + 0y >= 1 + 1x + 1y
        minus(minus(x, y), z) -> minus(x, plus(y, z))
        2 + 1x + 1y + 1z >= 2 + 1x + 1y + 0z
        minus(x, 0()) -> x
        2 + 1x >= 1x
      Qed
     
     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:
        sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
        2 + 0x + 0y + 1l >= 1 + 0x + 0y + 1l
        sum cons(x, nil()) -> cons(x, nil())
        2 + 0x >= 2 + 0x
        sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
        3 + 0x + 0y + 1k + 1l >= 3 + 0x + 0y + 1k + 1l
        app(cons(x, l), k) -> cons(x, app(l, k))
        2 + 0x + 1k + 1l >= 2 + 0x + 1k + 1l
        app(nil(), k) -> k
        2 + 1k >= 1k
        app(l, nil()) -> l
        2 + 1l >= 1l
        plus(s x, y) -> s plus(x, y)
        1 + 0x + 0y >= 0 + 0x + 0y
        plus(0(), y) -> y
        2 + 0y >= 1y
        quot(s x, s y) -> s quot(minus(x, y), s y)
        1 + 0x + 0y >= 0 + 0x + 0y
        quot(0(), s y) -> 0()
        2 + 0y >= 1
        minus(s x, s y) -> minus(x, y)
        1 + 0x + 0y >= 1 + 1x + 1y
        minus(minus(x, y), z) -> minus(x, plus(y, z))
        2 + 1x + 1y + 1z >= 2 + 1x + 1y + 0z
        minus(x, 0()) -> x
        2 + 1x >= 1x
      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:
       sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
       0 + 0x + 0y + 0l >= 0 + 0x + 0y + 0l
       sum cons(x, nil()) -> cons(x, nil())
       0 + 0x >= 2 + 0x
       sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
       0 + 0x + 0y + 0k + 0l >= 0 + 0x + 0y + 0k + 0l
       app(cons(x, l), k) -> cons(x, app(l, k))
       2 + 0x + 1k + 1l >= 2 + 0x + 1k + 1l
       app(nil(), k) -> k
       2 + 1k >= 1k
       app(l, nil()) -> l
       2 + 1l >= 1l
       plus(s x, y) -> s plus(x, y)
       2 + 1x + 0y >= 2 + 1x + 0y
       plus(0(), y) -> y
       2 + 0y >= 1y
       quot(s x, s y) -> s quot(minus(x, y), s y)
       2 + 0x + 1y >= 3 + 0x + 1y
       quot(0(), s y) -> 0()
       2 + 1y >= 1
       minus(s x, s y) -> minus(x, y)
       1 + 1x + 0y >= 0 + 1x + 0y
       minus(minus(x, y), z) -> minus(x, plus(y, z))
       0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
       minus(x, 0()) -> x
       0 + 1x >= 1x
     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)}
     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) = 0,
       
       [app](x0, x1) = x0 + x1 + 1,
       
       [cons](x0, x1) = 0,
       
       [s](x0) = x0 + 1,
       
       [sum](x0) = 0,
       
       [0] = 1,
       
       [nil] = 1,
       
       [minus#](x0, x1) = x0 + 1
      Strict:
       minus#(s x, s y) -> minus#(x, y)
       2 + 1x + 0y >= 1 + 1x + 0y
       minus#(minus(x, y), z) -> minus#(x, plus(y, z))
       2 + 1x + 1y + 0z >= 1 + 1x + 0y + 0z
      Weak:
       sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
       0 + 0x + 0y + 0l >= 0 + 0x + 0y + 0l
       sum cons(x, nil()) -> cons(x, nil())
       0 + 0x >= 0 + 0x
       sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
       0 + 0x + 0y + 0k + 0l >= 0 + 0x + 0y + 0k + 0l
       app(cons(x, l), k) -> cons(x, app(l, k))
       1 + 0x + 1k + 0l >= 0 + 0x + 0k + 0l
       app(nil(), k) -> k
       2 + 1k >= 1k
       app(l, nil()) -> l
       2 + 1l >= 1l
       plus(s x, y) -> s plus(x, y)
       0 + 0x + 0y >= 1 + 0x + 0y
       plus(0(), y) -> y
       0 + 0y >= 1y
       quot(s x, s y) -> s quot(minus(x, y), s y)
       2 + 0x + 1y >= 3 + 0x + 1y
       quot(0(), s y) -> 0()
       2 + 1y >= 1
       minus(s x, s y) -> minus(x, y)
       3 + 1x + 1y >= 1 + 1x + 1y
       minus(minus(x, y), z) -> minus(x, plus(y, z))
       2 + 1x + 1y + 1z >= 1 + 1x + 0y + 0z
       minus(x, 0()) -> x
       2 + 1x >= 1x
     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)}
    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) = 1,
      
      [app](x0, x1) = x0 + x1 + 1,
      
      [cons](x0, x1) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [sum](x0) = x0 + 1,
      
      [0] = 1,
      
      [nil] = 1,
      
      [plus#](x0, x1) = x0
     Strict:
      plus#(s x, y) -> plus#(x, y)
      1 + 1x + 0y >= 0 + 1x + 0y
     Weak:
      sum cons(x, cons(y, l)) -> sum cons(plus(x, y), l)
      3 + 0x + 0y + 1l >= 2 + 0x + 0y + 1l
      sum cons(x, nil()) -> cons(x, nil())
      3 + 0x >= 2 + 0x
      sum app(l, cons(x, cons(y, k))) -> sum app(l, sum cons(x, cons(y, k)))
      4 + 0x + 0y + 1k + 1l >= 5 + 0x + 0y + 1k + 1l
      app(cons(x, l), k) -> cons(x, app(l, k))
      2 + 0x + 1k + 1l >= 2 + 0x + 1k + 1l
      app(nil(), k) -> k
      2 + 1k >= 1k
      app(l, nil()) -> l
      2 + 1l >= 1l
      plus(s x, y) -> s plus(x, y)
      1 + 0x + 0y >= 2 + 0x + 0y
      plus(0(), y) -> y
      1 + 0y >= 1y
      quot(s x, s y) -> s quot(minus(x, y), s y)
      2 + 0x + 1y >= 3 + 0x + 1y
      quot(0(), s y) -> 0()
      2 + 1y >= 1
      minus(s x, s y) -> minus(x, y)
      3 + 1x + 1y >= 1 + 1x + 1y
      minus(minus(x, y), z) -> minus(x, plus(y, z))
      2 + 1x + 1y + 1z >= 2 + 1x + 0y + 0z
      minus(x, 0()) -> x
      2 + 1x >= 1x
    Qed