YES
Time: 0.005683
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:
  DP:
   {       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}
  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}
  EDG:
   {(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)))
    (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))
    (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z))
    (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
    (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# 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))
    (++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
    (++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(y, z))
    (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))
    (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))}
   SCCS (3):
    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 (2):
     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 (1):
        Scc:
         {rev# ++(x, y) -> rev# y}
        SCC (1):
         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 (2):
     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 (1):
        Scc:
         {++#(++(x, y), z) -> ++#(y, z)}
        SCC (1):
         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 (5):
     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# ++(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# 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 -> 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)
        (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)}
       SCCS (1):
        Scc:
         {       flatten# unit x -> flatten# x,
               flatten# ++(x, y) -> flatten# x,
               flatten# ++(x, y) -> flatten# y,
          flatten# ++(unit x, y) -> flatten# y}
        SCC (4):
         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 (1):
            Scc:
             {       flatten# unit x -> flatten# x,
                   flatten# ++(x, y) -> flatten# x,
              flatten# ++(unit x, y) -> flatten# y}
            SCC (3):
             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 -> flatten# x, flatten# ++(unit x, y) -> flatten# y)
                (flatten# unit x -> flatten# x, flatten# unit x -> flatten# x)
                (flatten# ++(unit x, y) -> flatten# y, flatten# unit x -> flatten# x)
                (flatten# ++(unit x, y) -> flatten# y, flatten# ++(unit x, y) -> flatten# y)}
               SCCS (1):
                Scc:
                 {       flatten# unit x -> flatten# x,
                  flatten# ++(unit x, y) -> flatten# y}
                SCC (2):
                 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 (1):
                    Scc:
                     {flatten# ++(unit x, y) -> flatten# y}
                    SCC (1):
                     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