YES
TRS:
 {                      app(app(map(), f), nil()) -> nil(),
      app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
  app(app(treemap(), f), app(app(node(), x), xs)) -> app(app(node(), app(f, x)), app(app(map(), app(treemap(), f)), xs))}
 DP:
  Strict:
   {    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)),
    app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(f, x),
    app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs),
    app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(node(), app(f, x)), app(app(map(), app(treemap(), f)), xs)),
    app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(map(), app(treemap(), f)),
    app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(node(), app(f, x))}
  Weak:
  {                      app(app(map(), f), nil()) -> nil(),
       app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
   app(app(treemap(), f), app(app(node(), x), xs)) -> app(app(node(), app(f, x)), app(app(map(), app(treemap(), f)), xs))}
  EDG:
   {(app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
    (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
    (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
    (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(node(), app(f, x)))
    (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(map(), app(treemap(), f)))
    (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(node(), app(f, x)), app(app(map(), app(treemap(), f)), xs)))
    (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs))
    (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(f, x))
    (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
    (app#(app(treemap(), f), app(app(node(), 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(treemap(), f), app(app(node(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
    (app#(app(treemap(), f), app(app(node(), 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#(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)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(f, x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(node(), app(f, x)), app(app(map(), app(treemap(), f)), xs)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(map(), app(treemap(), f)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(node(), 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(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)))}
   SCCS:
    Scc:
     {    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(treemap(), f), app(app(node(), x), xs)) -> app#(f, x),
      app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs)}
    SCC:
     Strict:
      {    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(treemap(), f), app(app(node(), x), xs)) -> app#(f, x),
       app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs)}
     Weak:
     {                      app(app(map(), f), nil()) -> nil(),
          app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
      app(app(treemap(), f), app(app(node(), x), xs)) -> app(app(node(), app(f, x)), app(app(map(), app(treemap(), f)), xs))}
     SPSC:
      Simple Projection:
       pi(app#) = 1
      Strict:
       {    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(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs)}
      EDG:
       {(app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
        (app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs), 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#(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(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), 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#(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))}
       SCCS:
        Scc:
         {    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(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs)}
        SCC:
         Strict:
          {    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(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs)}
         Weak:
         {                      app(app(map(), f), nil()) -> nil(),
              app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
          app(app(treemap(), f), app(app(node(), x), xs)) -> app(app(node(), app(f, x)), app(app(map(), app(treemap(), f)), xs))}
         SPSC:
          Simple Projection:
           pi(app#) = 1
          Strict:
           {    app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
            app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs)}
          EDG:
           {(app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs), 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#(f, x), app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs))}
           SCCS:
            Scc:
             {    app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
              app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs)}
            SCC:
             Strict:
              {    app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
               app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs)}
             Weak:
             {                      app(app(map(), f), nil()) -> nil(),
                  app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
              app(app(treemap(), f), app(app(node(), x), xs)) -> app(app(node(), app(f, x)), app(app(map(), app(treemap(), f)), xs))}
             SPSC:
              Simple Projection:
               pi(app#) = 1
              Strict:
               {app#(app(treemap(), f), app(app(node(), x), xs)) -> app#(app(map(), app(treemap(), f)), xs)}
              EDG:
               {}
               SCCS:
                
                Qed