YES
TRS:
 {            app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
  app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                    app(app(map(), f), nil()) -> nil(),
                                 app(id(), x) -> x,
                              app(add(), 0()) -> id()}
 DP:
  Strict:
   {            app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y),
                app#(app(add(), app(s(), x)), y) -> app#(add(), x),
                app#(app(add(), app(s(), x)), y) -> app#(s(), app(app(add(), x), y)),
    app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
    app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs),
    app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)),
    app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))}
  Weak:
  {            app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
   app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                     app(app(map(), f), nil()) -> nil(),
                                  app(id(), x) -> x,
                               app(add(), 0()) -> id()}
  EDG:
   {(app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
    (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
    (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
    (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(add(), app(s(), x)), y) -> app#(s(), app(app(add(), x), y)))
    (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(add(), app(s(), x)), y) -> app#(add(), x))
    (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(add(), app(s(), x)), y) -> app#(add(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(add(), app(s(), x)), y) -> app#(s(), app(app(add(), x), y)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))}
   SCCS:
    Scc:
     {            app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y),
      app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
      app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)}
    SCC:
     Strict:
      {            app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y),
       app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
       app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)}
     Weak:
     {            app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
      app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                        app(app(map(), f), nil()) -> nil(),
                                     app(id(), x) -> x,
                                  app(add(), 0()) -> id()}
     SPSC:
      Simple Projection:
       pi(app#) = 1
      Strict:
       {            app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y),
        app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)}
      EDG:
       {(app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
        (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y))
        (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))}
       SCCS:
        Scc:
         {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)}
        Scc:
         {app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y)}
        SCC:
         Strict:
          {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)}
         Weak:
         {            app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
          app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                            app(app(map(), f), nil()) -> nil(),
                                         app(id(), x) -> x,
                                      app(add(), 0()) -> id()}
         SPSC:
          Simple Projection:
           pi(app#) = 1
          Strict:
           {}
          Qed
        SCC:
         Strict:
          {app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y)}
         Weak:
         {            app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
          app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                            app(app(map(), f), nil()) -> nil(),
                                         app(id(), x) -> x,
                                      app(add(), 0()) -> id()}
         UR:
          {app(add(), 0()) -> id()}
          BOUND:
           Bound: match(-raise)-bounded by 1
           Automaton:
            {       s_0() -> 3*
                    0_0() -> 2*
                  add_1() -> 4*
                  add_0() -> 1*
                   id_1() -> 5 | 1
                   id_0() -> 1*
             app#_1(5, 3) -> 1*
             app#_1(5, 2) -> 1*
             app#_1(5, 1) -> 1*
             app#_0(3, 3) -> 1*
             app#_0(3, 2) -> 1*
             app#_0(3, 1) -> 1*
             app#_0(2, 3) -> 1*
             app#_0(2, 2) -> 1*
             app#_0(2, 1) -> 1*
             app#_0(1, 3) -> 1*
             app#_0(1, 2) -> 1*
             app#_0(1, 1) -> 1*
              app_1(4, 3) -> 5*
              app_1(4, 2) -> 5*
              app_1(4, 1) -> 5*
              app_0(3, 3) -> 1*
              app_0(3, 2) -> 1*
              app_0(3, 1) -> 1*
              app_0(2, 3) -> 1*
              app_0(2, 2) -> 1*
              app_0(2, 1) -> 1*
              app_0(1, 3) -> 1*
              app_0(1, 2) -> 1*
              app_0(1, 1) -> 1*}
           Strict:
            {}
           Qed