YES
TRS:
 {         flatten(nil()) -> nil(),
      flatten(flatten(x)) -> flatten(x),
         flatten(unit(x)) -> flatten(x),
        flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
  flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
             ++(x, nil()) -> x,
             ++(nil(), y) -> y,
          ++(++(x, y), z) -> ++(x, ++(y, z)),
               rev(nil()) -> nil(),
             rev(unit(x)) -> unit(x),
            rev(++(x, y)) -> ++(rev(y), rev(x)),
              rev(rev(x)) -> x}
 DP:
  Strict:
   {       flatten#(unit(x)) -> flatten#(x),
          flatten#(++(x, y)) -> flatten#(x),
          flatten#(++(x, y)) -> flatten#(y),
          flatten#(++(x, y)) -> ++#(flatten(x), flatten(y)),
    flatten#(++(unit(x), y)) -> flatten#(x),
    flatten#(++(unit(x), y)) -> flatten#(y),
    flatten#(++(unit(x), y)) -> ++#(flatten(x), flatten(y)),
            ++#(++(x, y), z) -> ++#(x, ++(y, z)),
            ++#(++(x, y), z) -> ++#(y, z),
              rev#(++(x, y)) -> ++#(rev(y), rev(x)),
              rev#(++(x, y)) -> rev#(x),
              rev#(++(x, y)) -> rev#(y)}
  Weak:
  {         flatten(nil()) -> nil(),
       flatten(flatten(x)) -> flatten(x),
          flatten(unit(x)) -> flatten(x),
         flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
   flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
              ++(x, nil()) -> x,
              ++(nil(), y) -> y,
           ++(++(x, y), z) -> ++(x, ++(y, z)),
                rev(nil()) -> nil(),
              rev(unit(x)) -> unit(x),
             rev(++(x, y)) -> ++(rev(y), rev(x)),
               rev(rev(x)) -> x}
  EDG:
   {(flatten#(++(x, y)) -> flatten#(x), flatten#(++(unit(x), y)) -> ++#(flatten(x), flatten(y)))
    (flatten#(++(x, y)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(y))
    (flatten#(++(x, y)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(x))
    (flatten#(++(x, y)) -> flatten#(x), flatten#(++(x, y)) -> ++#(flatten(x), flatten(y)))
    (flatten#(++(x, y)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(y))
    (flatten#(++(x, y)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(x))
    (flatten#(++(x, y)) -> flatten#(x), flatten#(unit(x)) -> flatten#(x))
    (rev#(++(x, y)) -> rev#(x), rev#(++(x, y)) -> rev#(y))
    (rev#(++(x, y)) -> rev#(x), rev#(++(x, y)) -> rev#(x))
    (rev#(++(x, y)) -> rev#(x), rev#(++(x, y)) -> ++#(rev(y), rev(x)))
    (flatten#(++(unit(x), y)) -> ++#(flatten(x), flatten(y)), ++#(++(x, y), z) -> ++#(y, z))
    (flatten#(++(unit(x), y)) -> ++#(flatten(x), flatten(y)), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
    (++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(y, z))
    (++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
    (flatten#(++(x, y)) -> flatten#(y), flatten#(++(unit(x), y)) -> ++#(flatten(x), flatten(y)))
    (flatten#(++(x, y)) -> flatten#(y), flatten#(++(unit(x), y)) -> flatten#(y))
    (flatten#(++(x, y)) -> flatten#(y), flatten#(++(unit(x), y)) -> flatten#(x))
    (flatten#(++(x, y)) -> flatten#(y), flatten#(++(x, y)) -> ++#(flatten(x), flatten(y)))
    (flatten#(++(x, y)) -> flatten#(y), flatten#(++(x, y)) -> flatten#(y))
    (flatten#(++(x, y)) -> flatten#(y), flatten#(++(x, y)) -> flatten#(x))
    (flatten#(++(x, y)) -> flatten#(y), flatten#(unit(x)) -> flatten#(x))
    (rev#(++(x, y)) -> rev#(y), rev#(++(x, y)) -> rev#(y))
    (rev#(++(x, y)) -> rev#(y), rev#(++(x, y)) -> rev#(x))
    (rev#(++(x, y)) -> rev#(y), rev#(++(x, y)) -> ++#(rev(y), rev(x)))
    (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(unit(x)) -> flatten#(x))
    (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(x, y)) -> flatten#(x))
    (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(x, y)) -> flatten#(y))
    (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(x, y)) -> ++#(flatten(x), flatten(y)))
    (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(unit(x), y)) -> flatten#(x))
    (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(unit(x), y)) -> flatten#(y))
    (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(unit(x), y)) -> ++#(flatten(x), flatten(y)))
    (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
    (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z))
    (rev#(++(x, y)) -> ++#(rev(y), rev(x)), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
    (rev#(++(x, y)) -> ++#(rev(y), rev(x)), ++#(++(x, y), z) -> ++#(y, z))
    (flatten#(++(x, y)) -> ++#(flatten(x), flatten(y)), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
    (flatten#(++(x, y)) -> ++#(flatten(x), flatten(y)), ++#(++(x, y), z) -> ++#(y, z))
    (flatten#(++(unit(x), y)) -> flatten#(x), flatten#(unit(x)) -> flatten#(x))
    (flatten#(++(unit(x), y)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(x))
    (flatten#(++(unit(x), y)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(y))
    (flatten#(++(unit(x), y)) -> flatten#(x), flatten#(++(x, y)) -> ++#(flatten(x), flatten(y)))
    (flatten#(++(unit(x), y)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(x))
    (flatten#(++(unit(x), y)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(y))
    (flatten#(++(unit(x), y)) -> flatten#(x), flatten#(++(unit(x), y)) -> ++#(flatten(x), flatten(y)))
    (flatten#(unit(x)) -> flatten#(x), flatten#(unit(x)) -> flatten#(x))
    (flatten#(unit(x)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(x))
    (flatten#(unit(x)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(y))
    (flatten#(unit(x)) -> flatten#(x), flatten#(++(x, y)) -> ++#(flatten(x), flatten(y)))
    (flatten#(unit(x)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(x))
    (flatten#(unit(x)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(y))
    (flatten#(unit(x)) -> flatten#(x), flatten#(++(unit(x), y)) -> ++#(flatten(x), flatten(y)))}
   SCCS:
    Scc:
     {rev#(++(x, y)) -> rev#(x),
      rev#(++(x, y)) -> rev#(y)}
    Scc:
     {++#(++(x, y), z) -> ++#(x, ++(y, z)),
      ++#(++(x, y), z) -> ++#(y, z)}
    Scc:
     {       flatten#(unit(x)) -> flatten#(x),
            flatten#(++(x, y)) -> flatten#(x),
            flatten#(++(x, y)) -> flatten#(y),
      flatten#(++(unit(x), y)) -> flatten#(x),
      flatten#(++(unit(x), y)) -> flatten#(y)}
    SCC:
     Strict:
      {rev#(++(x, y)) -> rev#(x),
       rev#(++(x, y)) -> rev#(y)}
     Weak:
     {         flatten(nil()) -> nil(),
          flatten(flatten(x)) -> flatten(x),
             flatten(unit(x)) -> flatten(x),
            flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
      flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
                 ++(x, nil()) -> x,
                 ++(nil(), y) -> y,
              ++(++(x, y), z) -> ++(x, ++(y, z)),
                   rev(nil()) -> nil(),
                 rev(unit(x)) -> unit(x),
                rev(++(x, y)) -> ++(rev(y), rev(x)),
                  rev(rev(x)) -> x}
     SPSC:
      Simple Projection:
       pi(rev#) = 0
      Strict:
       {rev#(++(x, y)) -> rev#(y)}
      EDG:
       {(rev#(++(x, y)) -> rev#(y), rev#(++(x, y)) -> rev#(y))}
       SCCS:
        Scc:
         {rev#(++(x, y)) -> rev#(y)}
        SCC:
         Strict:
          {rev#(++(x, y)) -> rev#(y)}
         Weak:
         {         flatten(nil()) -> nil(),
              flatten(flatten(x)) -> flatten(x),
                 flatten(unit(x)) -> flatten(x),
                flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
          flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
                     ++(x, nil()) -> x,
                     ++(nil(), y) -> y,
                  ++(++(x, y), z) -> ++(x, ++(y, z)),
                       rev(nil()) -> nil(),
                     rev(unit(x)) -> unit(x),
                    rev(++(x, y)) -> ++(rev(y), rev(x)),
                      rev(rev(x)) -> x}
         SPSC:
          Simple Projection:
           pi(rev#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {++#(++(x, y), z) -> ++#(x, ++(y, z)),
       ++#(++(x, y), z) -> ++#(y, z)}
     Weak:
     {         flatten(nil()) -> nil(),
          flatten(flatten(x)) -> flatten(x),
             flatten(unit(x)) -> flatten(x),
            flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
      flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
                 ++(x, nil()) -> x,
                 ++(nil(), y) -> y,
              ++(++(x, y), z) -> ++(x, ++(y, z)),
                   rev(nil()) -> nil(),
                 rev(unit(x)) -> unit(x),
                rev(++(x, y)) -> ++(rev(y), rev(x)),
                  rev(rev(x)) -> x}
     SPSC:
      Simple Projection:
       pi(++#) = 0
      Strict:
       {++#(++(x, y), z) -> ++#(y, z)}
      EDG:
       {(++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z))}
       SCCS:
        Scc:
         {++#(++(x, y), z) -> ++#(y, z)}
        SCC:
         Strict:
          {++#(++(x, y), z) -> ++#(y, z)}
         Weak:
         {         flatten(nil()) -> nil(),
              flatten(flatten(x)) -> flatten(x),
                 flatten(unit(x)) -> flatten(x),
                flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
          flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
                     ++(x, nil()) -> x,
                     ++(nil(), y) -> y,
                  ++(++(x, y), z) -> ++(x, ++(y, z)),
                       rev(nil()) -> nil(),
                     rev(unit(x)) -> unit(x),
                    rev(++(x, y)) -> ++(rev(y), rev(x)),
                      rev(rev(x)) -> x}
         SPSC:
          Simple Projection:
           pi(++#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {       flatten#(unit(x)) -> flatten#(x),
             flatten#(++(x, y)) -> flatten#(x),
             flatten#(++(x, y)) -> flatten#(y),
       flatten#(++(unit(x), y)) -> flatten#(x),
       flatten#(++(unit(x), y)) -> flatten#(y)}
     Weak:
     {         flatten(nil()) -> nil(),
          flatten(flatten(x)) -> flatten(x),
             flatten(unit(x)) -> flatten(x),
            flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
      flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
                 ++(x, nil()) -> x,
                 ++(nil(), y) -> y,
              ++(++(x, y), z) -> ++(x, ++(y, z)),
                   rev(nil()) -> nil(),
                 rev(unit(x)) -> unit(x),
                rev(++(x, y)) -> ++(rev(y), rev(x)),
                  rev(rev(x)) -> x}
     SPSC:
      Simple Projection:
       pi(flatten#) = 0
      Strict:
       {       flatten#(unit(x)) -> flatten#(x),
              flatten#(++(x, y)) -> flatten#(x),
              flatten#(++(x, y)) -> flatten#(y),
        flatten#(++(unit(x), y)) -> flatten#(y)}
      EDG:
       {(flatten#(++(x, y)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(y))
        (flatten#(++(x, y)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(y))
        (flatten#(++(x, y)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(x))
        (flatten#(++(x, y)) -> flatten#(x), flatten#(unit(x)) -> flatten#(x))
        (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(unit(x), y)) -> flatten#(y))
        (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(x, y)) -> flatten#(y))
        (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(x, y)) -> flatten#(x))
        (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(unit(x)) -> flatten#(x))
        (flatten#(++(x, y)) -> flatten#(y), flatten#(unit(x)) -> flatten#(x))
        (flatten#(++(x, y)) -> flatten#(y), flatten#(++(x, y)) -> flatten#(x))
        (flatten#(++(x, y)) -> flatten#(y), flatten#(++(x, y)) -> flatten#(y))
        (flatten#(++(x, y)) -> flatten#(y), flatten#(++(unit(x), y)) -> flatten#(y))
        (flatten#(unit(x)) -> flatten#(x), flatten#(unit(x)) -> flatten#(x))
        (flatten#(unit(x)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(x))
        (flatten#(unit(x)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(y))
        (flatten#(unit(x)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(y))}
       SCCS:
        Scc:
         {       flatten#(unit(x)) -> flatten#(x),
                flatten#(++(x, y)) -> flatten#(x),
                flatten#(++(x, y)) -> flatten#(y),
          flatten#(++(unit(x), y)) -> flatten#(y)}
        SCC:
         Strict:
          {       flatten#(unit(x)) -> flatten#(x),
                 flatten#(++(x, y)) -> flatten#(x),
                 flatten#(++(x, y)) -> flatten#(y),
           flatten#(++(unit(x), y)) -> flatten#(y)}
         Weak:
         {         flatten(nil()) -> nil(),
              flatten(flatten(x)) -> flatten(x),
                 flatten(unit(x)) -> flatten(x),
                flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
          flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
                     ++(x, nil()) -> x,
                     ++(nil(), y) -> y,
                  ++(++(x, y), z) -> ++(x, ++(y, z)),
                       rev(nil()) -> nil(),
                     rev(unit(x)) -> unit(x),
                    rev(++(x, y)) -> ++(rev(y), rev(x)),
                      rev(rev(x)) -> x}
         SPSC:
          Simple Projection:
           pi(flatten#) = 0
          Strict:
           {       flatten#(unit(x)) -> flatten#(x),
                  flatten#(++(x, y)) -> flatten#(x),
            flatten#(++(unit(x), y)) -> flatten#(y)}
          EDG:
           {(flatten#(unit(x)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(y))
            (flatten#(unit(x)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(x))
            (flatten#(unit(x)) -> flatten#(x), flatten#(unit(x)) -> flatten#(x))
            (flatten#(++(x, y)) -> flatten#(x), flatten#(unit(x)) -> flatten#(x))
            (flatten#(++(x, y)) -> flatten#(x), flatten#(++(x, y)) -> flatten#(x))
            (flatten#(++(x, y)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(y))
            (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(unit(x)) -> flatten#(x))
            (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(x, y)) -> flatten#(x))
            (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(unit(x), y)) -> flatten#(y))}
           SCCS:
            Scc:
             {       flatten#(unit(x)) -> flatten#(x),
                    flatten#(++(x, y)) -> flatten#(x),
              flatten#(++(unit(x), y)) -> flatten#(y)}
            SCC:
             Strict:
              {       flatten#(unit(x)) -> flatten#(x),
                     flatten#(++(x, y)) -> flatten#(x),
               flatten#(++(unit(x), y)) -> flatten#(y)}
             Weak:
             {         flatten(nil()) -> nil(),
                  flatten(flatten(x)) -> flatten(x),
                     flatten(unit(x)) -> flatten(x),
                    flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
              flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
                         ++(x, nil()) -> x,
                         ++(nil(), y) -> y,
                      ++(++(x, y), z) -> ++(x, ++(y, z)),
                           rev(nil()) -> nil(),
                         rev(unit(x)) -> unit(x),
                        rev(++(x, y)) -> ++(rev(y), rev(x)),
                          rev(rev(x)) -> x}
             SPSC:
              Simple Projection:
               pi(flatten#) = 0
              Strict:
               {       flatten#(unit(x)) -> flatten#(x),
                flatten#(++(unit(x), y)) -> flatten#(y)}
              EDG:
               {(flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(unit(x), y)) -> flatten#(y))
                (flatten#(++(unit(x), y)) -> flatten#(y), flatten#(unit(x)) -> flatten#(x))
                (flatten#(unit(x)) -> flatten#(x), flatten#(unit(x)) -> flatten#(x))
                (flatten#(unit(x)) -> flatten#(x), flatten#(++(unit(x), y)) -> flatten#(y))}
               SCCS:
                Scc:
                 {       flatten#(unit(x)) -> flatten#(x),
                  flatten#(++(unit(x), y)) -> flatten#(y)}
                SCC:
                 Strict:
                  {       flatten#(unit(x)) -> flatten#(x),
                   flatten#(++(unit(x), y)) -> flatten#(y)}
                 Weak:
                 {         flatten(nil()) -> nil(),
                      flatten(flatten(x)) -> flatten(x),
                         flatten(unit(x)) -> flatten(x),
                        flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
                  flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
                             ++(x, nil()) -> x,
                             ++(nil(), y) -> y,
                          ++(++(x, y), z) -> ++(x, ++(y, z)),
                               rev(nil()) -> nil(),
                             rev(unit(x)) -> unit(x),
                            rev(++(x, y)) -> ++(rev(y), rev(x)),
                              rev(rev(x)) -> x}
                 SPSC:
                  Simple Projection:
                   pi(flatten#) = 0
                  Strict:
                   {flatten#(++(unit(x), y)) -> flatten#(y)}
                  EDG:
                   {(flatten#(++(unit(x), y)) -> flatten#(y), flatten#(++(unit(x), y)) -> flatten#(y))}
                   SCCS:
                    Scc:
                     {flatten#(++(unit(x), y)) -> flatten#(y)}
                    SCC:
                     Strict:
                      {flatten#(++(unit(x), y)) -> flatten#(y)}
                     Weak:
                     {         flatten(nil()) -> nil(),
                          flatten(flatten(x)) -> flatten(x),
                             flatten(unit(x)) -> flatten(x),
                            flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
                      flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
                                 ++(x, nil()) -> x,
                                 ++(nil(), y) -> y,
                              ++(++(x, y), z) -> ++(x, ++(y, z)),
                                   rev(nil()) -> nil(),
                                 rev(unit(x)) -> unit(x),
                                rev(++(x, y)) -> ++(rev(y), rev(x)),
                                  rev(rev(x)) -> x}
                     SPSC:
                      Simple Projection:
                       pi(flatten#) = 0
                      Strict:
                       {}
                      Qed