YES
TRS:
 {               app(app(app(compose(), f), g), x) -> app(g, app(f, x)),
  app(app(reverse2(), app(app(cons(), x), xs)), l) -> app(app(reverse2(), xs), app(app(cons(), x), l)),
                    app(app(reverse2(), nil()), l) -> l,
                                 app(reverse(), l) -> app(app(reverse2(), l), nil()),
                app(hd(), app(app(cons(), x), xs)) -> x,
                app(tl(), app(app(cons(), x), xs)) -> xs,
                                            last() -> app(app(compose(), hd()), reverse()),
                                            init() -> app(app(compose(), reverse()), app(app(compose(), tl()), reverse()))}
 RUF:
  Strict:
   {               app(app(app(compose(), f), g), x) -> app(g, app(f, x)),
    app(app(reverse2(), app(app(cons(), x), xs)), l) -> app(app(reverse2(), xs), app(app(cons(), x), l)),
                      app(app(reverse2(), nil()), l) -> l,
                                   app(reverse(), l) -> app(app(reverse2(), l), nil()),
                  app(hd(), app(app(cons(), x), xs)) -> x,
                  app(tl(), app(app(cons(), x), xs)) -> xs}
  Weak:
   {}
  RUF:
   Strict:
    {app(app(reverse2(), app(app(cons(), x), xs)), l) -> app(app(reverse2(), xs), app(app(cons(), x), l)),
                       app(app(reverse2(), nil()), l) -> l}
   Weak:
    {}
   RUF:
    Strict:
     {app(app(reverse2(), app(app(cons(), x), xs)), l) -> app(app(reverse2(), xs), app(app(cons(), x), l))}
    Weak:
     {}
    DP:
     Strict:
      {app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(app(reverse2(), xs), app(app(cons(), x), l)),
       app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(app(cons(), x), l),
       app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(reverse2(), xs)}
     Weak:
     {app(app(reverse2(), app(app(cons(), x), xs)), l) -> app(app(reverse2(), xs), app(app(cons(), x), l))}
     EDG:
      {(app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(app(reverse2(), xs), app(app(cons(), x), l)), app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(reverse2(), xs))
       (app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(app(reverse2(), xs), app(app(cons(), x), l)), app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(app(cons(), x), l))
       (app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(app(reverse2(), xs), app(app(cons(), x), l)), app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(app(reverse2(), xs), app(app(cons(), x), l)))}
      SCCS:
       Scc:
        {app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(app(reverse2(), xs), app(app(cons(), x), l))}
       SCC:
        Strict:
         {app#(app(reverse2(), app(app(cons(), x), xs)), l) -> app#(app(reverse2(), xs), app(app(cons(), x), l))}
        Weak:
        {app(app(reverse2(), app(app(cons(), x), xs)), l) -> app(app(reverse2(), xs), app(app(cons(), x), l))}
        POLY:
         Argument Filtering:
          pi(cons) = [], pi(reverse2) = [], pi(app#) = 0, pi(app) = [0,1]
         Usable Rules:
          {}
         Interpretation:
          [app](x0, x1) = x0 + x1 + 1,
          [cons] = 0,
          [reverse2] = 1
         Strict:
          {}
         Weak:
          {app(app(reverse2(), app(app(cons(), x), xs)), l) -> app(app(reverse2(), xs), app(app(cons(), x), l))}
         Qed