MAYBE
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(append(), nil()), xs) -> xs,
  app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                             app(concat(), nil()) -> nil(),
           app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
          app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), 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(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys)),
    app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys),
    app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs),
             app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)),
             app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs),
             app#(concat(), app(app(cons(), x), xs)) -> app#(append(), x),
            app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs),
            app#(flatten(), app(app(node(), x), xs)) -> app#(app(cons(), x), app(concat(), app(app(map(), flatten()), xs))),
            app#(flatten(), app(app(node(), x), xs)) -> app#(map(), flatten()),
            app#(flatten(), app(app(node(), x), xs)) -> app#(cons(), x),
            app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), 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(append(), nil()), xs) -> xs,
   app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                              app(concat(), nil()) -> nil(),
            app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
           app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), 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#(cons(), 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#(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#(f, x))
    (app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs))
    (app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys))
    (app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys)))
    (app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs), app#(concat(), app(app(cons(), x), xs)) -> app#(append(), x))
    (app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs), app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs))
    (app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs), app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), 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#(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(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(concat(), app(app(cons(), x), xs)) -> app#(append(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(app(cons(), x), app(concat(), app(app(map(), flatten()), xs))))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(map(), flatten()))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(cons(), x))
    (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), xs)))
    (app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), xs)), app#(concat(), app(app(cons(), x), xs)) -> app#(app(append(), x), app(concat(), xs)))
    (app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), xs)), app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs))
    (app#(flatten(), app(app(node(), x), xs)) -> app#(concat(), app(app(map(), flatten()), xs)), app#(concat(), app(app(cons(), x), xs)) -> app#(append(), x))
    (app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))
    (app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs))
    (app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)))
    (app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))
    (app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys)))
    (app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys))
    (app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs))}
   SCCS:
    Scc:
     {app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), xs)}
    Scc:
     {app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys)}
    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#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs)}
    SCC:
     Strict:
      {app#(concat(), app(app(cons(), x), xs)) -> app#(concat(), 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(append(), nil()), xs) -> xs,
      app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                                 app(concat(), nil()) -> nil(),
               app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
              app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), xs)))}
     SPSC:
      Simple Projection:
       pi(app#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys)}
     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(append(), nil()), xs) -> xs,
      app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                                 app(concat(), nil()) -> nil(),
               app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
              app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), xs)))}
     Fail
    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#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), 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(append(), nil()), xs) -> xs,
      app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                                 app(concat(), nil()) -> nil(),
               app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
              app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), xs)))}
     SPSC:
      Simple Projection:
       pi(app#) = 1
      Strict:
       {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
            app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs)}
      EDG:
       {(app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), 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#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs))}
       SCCS:
        Scc:
         {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
              app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs)}
        SCC:
         Strict:
          {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x),
               app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), 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(append(), nil()), xs) -> xs,
          app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)),
                                     app(concat(), nil()) -> nil(),
                   app(concat(), app(app(cons(), x), xs)) -> app(app(append(), x), app(concat(), xs)),
                  app(flatten(), app(app(node(), x), xs)) -> app(app(cons(), x), app(concat(), app(app(map(), flatten()), xs)))}
         SPSC:
          Simple Projection:
           pi(app#) = 1
          Strict:
           {app#(flatten(), app(app(node(), x), xs)) -> app#(app(map(), flatten()), xs)}
          EDG:
           {}
           SCCS:
            
            Qed