YES
TRS:
 {           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(a(x, y, h()), l)),
           a(x, s(y), h()) -> a(x, y, s(h())),
          a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)),
            a(h(), h(), x) -> s(x),
           a(s(x), h(), z) -> a(x, z, z)}
 DP:
  Strict:
   {      app#(cons(x, l), k) -> app#(l, k),
    sum#(cons(x, cons(y, l))) -> sum#(cons(a(x, y, h()), l)),
    sum#(cons(x, cons(y, l))) -> a#(x, y, h()),
             a#(x, s(y), h()) -> a#(x, y, s(h())),
            a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)),
            a#(x, s(y), s(z)) -> a#(x, s(y), z),
             a#(s(x), h(), z) -> a#(x, z, z)}
  Weak:
  {           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(a(x, y, h()), l)),
            a(x, s(y), h()) -> a(x, y, s(h())),
           a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)),
             a(h(), h(), x) -> s(x),
            a(s(x), h(), z) -> a(x, z, z)}
  EDG:
   {(a#(x, s(y), h()) -> a#(x, y, s(h())), a#(s(x), h(), z) -> a#(x, z, z))
    (a#(x, s(y), h()) -> a#(x, y, s(h())), a#(x, s(y), s(z)) -> a#(x, s(y), z))
    (a#(x, s(y), h()) -> a#(x, y, s(h())), a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)))
    (a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)), a#(s(x), h(), z) -> a#(x, z, z))
    (a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)), a#(x, s(y), s(z)) -> a#(x, s(y), z))
    (a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)), a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)))
    (a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)), a#(x, s(y), h()) -> a#(x, y, s(h())))
    (a#(s(x), h(), z) -> a#(x, z, z), a#(s(x), h(), z) -> a#(x, z, z))
    (a#(s(x), h(), z) -> a#(x, z, z), a#(x, s(y), s(z)) -> a#(x, s(y), z))
    (a#(s(x), h(), z) -> a#(x, z, z), a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)))
    (a#(s(x), h(), z) -> a#(x, z, z), a#(x, s(y), h()) -> a#(x, y, s(h())))
    (sum#(cons(x, cons(y, l))) -> a#(x, y, h()), a#(x, s(y), h()) -> a#(x, y, s(h())))
    (sum#(cons(x, cons(y, l))) -> a#(x, y, h()), a#(s(x), h(), z) -> a#(x, z, z))
    (a#(x, s(y), s(z)) -> a#(x, s(y), z), a#(x, s(y), h()) -> a#(x, y, s(h())))
    (a#(x, s(y), s(z)) -> a#(x, s(y), z), a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)))
    (a#(x, s(y), s(z)) -> a#(x, s(y), z), a#(x, s(y), s(z)) -> a#(x, s(y), z))
    (sum#(cons(x, cons(y, l))) -> sum#(cons(a(x, y, h()), l)), sum#(cons(x, cons(y, l))) -> sum#(cons(a(x, y, h()), l)))
    (sum#(cons(x, cons(y, l))) -> sum#(cons(a(x, y, h()), l)), sum#(cons(x, cons(y, l))) -> a#(x, y, h()))
    (app#(cons(x, l), k) -> app#(l, k), app#(cons(x, l), k) -> app#(l, k))}
   SCCS:
    Scc:
     { a#(x, s(y), h()) -> a#(x, y, s(h())),
      a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)),
      a#(x, s(y), s(z)) -> a#(x, s(y), z),
       a#(s(x), h(), z) -> a#(x, z, z)}
    Scc:
     {sum#(cons(x, cons(y, l))) -> sum#(cons(a(x, y, h()), l))}
    Scc:
     {app#(cons(x, l), k) -> app#(l, k)}
    SCC:
     Strict:
      { a#(x, s(y), h()) -> a#(x, y, s(h())),
       a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)),
       a#(x, s(y), s(z)) -> a#(x, s(y), z),
        a#(s(x), h(), z) -> a#(x, z, z)}
     Weak:
     {           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(a(x, y, h()), l)),
               a(x, s(y), h()) -> a(x, y, s(h())),
              a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)),
                a(h(), h(), x) -> s(x),
               a(s(x), h(), z) -> a(x, z, z)}
     SPSC:
      Simple Projection:
       pi(a#) = 0
      Strict:
       { a#(x, s(y), h()) -> a#(x, y, s(h())),
        a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)),
        a#(x, s(y), s(z)) -> a#(x, s(y), z)}
      EDG:
       {(a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)), a#(x, s(y), s(z)) -> a#(x, s(y), z))
        (a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)), a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)))
        (a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)), a#(x, s(y), h()) -> a#(x, y, s(h())))
        (a#(x, s(y), s(z)) -> a#(x, s(y), z), a#(x, s(y), h()) -> a#(x, y, s(h())))
        (a#(x, s(y), s(z)) -> a#(x, s(y), z), a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)))
        (a#(x, s(y), s(z)) -> a#(x, s(y), z), a#(x, s(y), s(z)) -> a#(x, s(y), z))
        (a#(x, s(y), h()) -> a#(x, y, s(h())), a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)))
        (a#(x, s(y), h()) -> a#(x, y, s(h())), a#(x, s(y), s(z)) -> a#(x, s(y), z))}
       SCCS:
        Scc:
         { a#(x, s(y), h()) -> a#(x, y, s(h())),
          a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)),
          a#(x, s(y), s(z)) -> a#(x, s(y), z)}
        SCC:
         Strict:
          { a#(x, s(y), h()) -> a#(x, y, s(h())),
           a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)),
           a#(x, s(y), s(z)) -> a#(x, s(y), z)}
         Weak:
         {           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(a(x, y, h()), l)),
                   a(x, s(y), h()) -> a(x, y, s(h())),
                  a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)),
                    a(h(), h(), x) -> s(x),
                   a(s(x), h(), z) -> a(x, z, z)}
         SPSC:
          Simple Projection:
           pi(a#) = 1
          Strict:
           {a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)),
            a#(x, s(y), s(z)) -> a#(x, s(y), z)}
          EDG:
           {(a#(x, s(y), s(z)) -> a#(x, s(y), z), a#(x, s(y), s(z)) -> a#(x, s(y), z))
            (a#(x, s(y), s(z)) -> a#(x, s(y), z), a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)))
            (a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)), a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)))
            (a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)), a#(x, s(y), s(z)) -> a#(x, s(y), z))}
           SCCS:
            Scc:
             {a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)),
              a#(x, s(y), s(z)) -> a#(x, s(y), z)}
            SCC:
             Strict:
              {a#(x, s(y), s(z)) -> a#(x, y, a(x, s(y), z)),
               a#(x, s(y), s(z)) -> a#(x, s(y), z)}
             Weak:
             {           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(a(x, y, h()), l)),
                       a(x, s(y), h()) -> a(x, y, s(h())),
                      a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)),
                        a(h(), h(), x) -> s(x),
                       a(s(x), h(), z) -> a(x, z, z)}
             SPSC:
              Simple Projection:
               pi(a#) = 1
              Strict:
               {a#(x, s(y), s(z)) -> a#(x, s(y), z)}
              EDG:
               {(a#(x, s(y), s(z)) -> a#(x, s(y), z), a#(x, s(y), s(z)) -> a#(x, s(y), z))}
               SCCS:
                Scc:
                 {a#(x, s(y), s(z)) -> a#(x, s(y), z)}
                SCC:
                 Strict:
                  {a#(x, s(y), s(z)) -> a#(x, s(y), z)}
                 Weak:
                 {           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(a(x, y, h()), l)),
                           a(x, s(y), h()) -> a(x, y, s(h())),
                          a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)),
                            a(h(), h(), x) -> s(x),
                           a(s(x), h(), z) -> a(x, z, z)}
                 SPSC:
                  Simple Projection:
                   pi(a#) = 2
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {sum#(cons(x, cons(y, l))) -> sum#(cons(a(x, y, h()), l))}
     Weak:
     {           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(a(x, y, h()), l)),
               a(x, s(y), h()) -> a(x, y, s(h())),
              a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)),
                a(h(), h(), x) -> s(x),
               a(s(x), h(), z) -> a(x, z, z)}
     POLY:
      Argument Filtering:
       pi(s) = [], pi(h) = [], pi(a) = [], pi(sum#) = 0, pi(sum) = [], pi(cons) = [1], pi(nil) = [], pi(app) = []
      Usable Rules:
       {}
      Interpretation:
       [cons](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {           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(a(x, y, h()), l)),
                 a(x, s(y), h()) -> a(x, y, s(h())),
                a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)),
                  a(h(), h(), x) -> s(x),
                 a(s(x), h(), z) -> a(x, z, z)}
      Qed
    SCC:
     Strict:
      {app#(cons(x, l), k) -> app#(l, k)}
     Weak:
     {           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(a(x, y, h()), l)),
               a(x, s(y), h()) -> a(x, y, s(h())),
              a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)),
                a(h(), h(), x) -> s(x),
               a(s(x), h(), z) -> a(x, z, z)}
     SPSC:
      Simple Projection:
       pi(app#) = 0
      Strict:
       {}
      Qed