YES
TRS:
 { app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)),
  app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys),
                                     app(app(filter(), f), nil()) -> nil(),
                   app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))}
 DP:
  Strict:
   { app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
     app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(filter(), f), ys)),
     app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f),
    app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
    app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f),
                     app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y),
                     app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)),
                     app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f),
                     app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y))}
  Weak:
  { app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)),
   app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys),
                                      app(app(filter(), f), nil()) -> nil(),
                    app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))}
  EDG:
   {(app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y)))
    (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f))
    (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)))
    (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y))
    (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys))
    (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(filter(), f), ys)))
    (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f))
    (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys))
    (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f))
    (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y))
    (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)))
    (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f))
    (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y)))
    (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y))
    (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)))
    (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f))
    (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y)))}
   SCCS:
    Scc:
     { app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
      app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
                       app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)}
    SCC:
     Strict:
      { app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
       app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
                        app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)}
     Weak:
     { app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)),
      app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys),
                                         app(app(filter(), f), nil()) -> nil(),
                       app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))}
     SPSC:
      Simple Projection:
       pi(app#) = 1
      Strict:
       {app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
                        app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)}
      EDG:
       {(app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y))
        (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys))
        (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y))}
       SCCS:
        Scc:
         {app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
                          app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)}
        SCC:
         Strict:
          {app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys),
                           app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)}
         Weak:
         { app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)),
          app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys),
                                             app(app(filter(), f), nil()) -> nil(),
                           app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))}
         SPSC:
          Simple Projection:
           pi(app#) = 1
          Strict:
           {app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)}
          EDG:
           {(app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y))}
           SCCS:
            Scc:
             {app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)}
            SCC:
             Strict:
              {app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)}
             Weak:
             { app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)),
              app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys),
                                                 app(app(filter(), f), nil()) -> nil(),
                               app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))}
             SPSC:
              Simple Projection:
               pi(app#) = 0
              Strict:
               {}
              Qed