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