YES
Time: 0.002374
TRS:
 {      rev nil() -> nil(),
        rev rev x -> x,
     rev ++(x, y) -> ++(rev y, rev x),
     ++(x, nil()) -> x,
  ++(x, ++(y, z)) -> ++(++(x, y), z),
     ++(nil(), y) -> y,
   ++(.(x, y), z) -> .(x, ++(y, z)),
           make x -> .(x, nil())}
 RUF:
  Strict:
   {      rev nil() -> nil(),
          rev rev x -> x,
       rev ++(x, y) -> ++(rev y, rev x),
       ++(x, nil()) -> x,
    ++(x, ++(y, z)) -> ++(++(x, y), z),
       ++(nil(), y) -> y,
     ++(.(x, y), z) -> .(x, ++(y, z))}
  Weak:
   {}
  DP:
   DP:
    {   rev# ++(x, y) -> rev# x,
        rev# ++(x, y) -> rev# y,
        rev# ++(x, y) -> ++#(rev y, rev x),
     ++#(x, ++(y, z)) -> ++#(x, y),
     ++#(x, ++(y, z)) -> ++#(++(x, y), z),
      ++#(.(x, y), z) -> ++#(y, z)}
   TRS:
   {      rev nil() -> nil(),
          rev rev x -> x,
       rev ++(x, y) -> ++(rev y, rev x),
       ++(x, nil()) -> x,
    ++(x, ++(y, z)) -> ++(++(x, y), z),
       ++(nil(), y) -> y,
     ++(.(x, y), z) -> .(x, ++(y, z))}
   EDG:
    {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))
     (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(++(x, y), z))
     (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(x, y))
     (rev# ++(x, y) -> ++#(rev y, rev x), ++#(.(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)) -> ++#(x, y))
     (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> ++#(rev y, rev x))
     (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# y)
     (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# x)
     (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(x, ++(y, z)) -> ++#(x, y))
     (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(x, ++(y, z)) -> ++#(++(x, y), z))
     (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(.(x, y), z) -> ++#(y, z))
     (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(x, y))
     (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z))
     (++#(x, ++(y, z)) -> ++#(x, y), ++#(.(x, y), z) -> ++#(y, z))
     (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# x)
     (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# y)
     (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> ++#(rev y, rev x))}
    SCCS (2):
     Scc:
      {++#(x, ++(y, z)) -> ++#(x, y),
       ++#(x, ++(y, z)) -> ++#(++(x, y), z),
        ++#(.(x, y), z) -> ++#(y, z)}
     Scc:
      {rev# ++(x, y) -> rev# x,
       rev# ++(x, y) -> rev# y}
     SCC (3):
      Strict:
       {++#(x, ++(y, z)) -> ++#(x, y),
        ++#(x, ++(y, z)) -> ++#(++(x, y), z),
         ++#(.(x, y), z) -> ++#(y, z)}
      Weak:
      {      rev nil() -> nil(),
             rev rev x -> x,
          rev ++(x, y) -> ++(rev y, rev x),
          ++(x, nil()) -> x,
       ++(x, ++(y, z)) -> ++(++(x, y), z),
          ++(nil(), y) -> y,
        ++(.(x, y), z) -> .(x, ++(y, z))}
      SPSC:
       Simple Projection:
        pi(++#) = 1
       Strict:
        {++#(x, ++(y, z)) -> ++#(x, y),
          ++#(.(x, y), z) -> ++#(y, z)}
       EDG:
        {(++#(x, ++(y, z)) -> ++#(x, y), ++#(.(x, y), z) -> ++#(y, z))
         (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(x, y))
         (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(x, y))
         (++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))}
        SCCS (1):
         Scc:
          {++#(x, ++(y, z)) -> ++#(x, y),
            ++#(.(x, y), z) -> ++#(y, z)}
         SCC (2):
          Strict:
           {++#(x, ++(y, z)) -> ++#(x, y),
             ++#(.(x, y), z) -> ++#(y, z)}
          Weak:
          {      rev nil() -> nil(),
                 rev rev x -> x,
              rev ++(x, y) -> ++(rev y, rev x),
              ++(x, nil()) -> x,
           ++(x, ++(y, z)) -> ++(++(x, y), z),
              ++(nil(), y) -> y,
            ++(.(x, y), z) -> .(x, ++(y, z))}
          SPSC:
           Simple Projection:
            pi(++#) = 1
           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:
              {      rev nil() -> nil(),
                     rev rev x -> x,
                  rev ++(x, y) -> ++(rev y, rev x),
                  ++(x, nil()) -> x,
               ++(x, ++(y, z)) -> ++(++(x, y), z),
                  ++(nil(), y) -> y,
                ++(.(x, y), z) -> .(x, ++(y, z))}
              SPSC:
               Simple Projection:
                pi(++#) = 0
               Strict:
                {}
               Qed
     SCC (2):
      Strict:
       {rev# ++(x, y) -> rev# x,
        rev# ++(x, y) -> rev# y}
      Weak:
      {      rev nil() -> nil(),
             rev rev x -> x,
          rev ++(x, y) -> ++(rev y, rev x),
          ++(x, nil()) -> x,
       ++(x, ++(y, z)) -> ++(++(x, y), z),
          ++(nil(), y) -> y,
        ++(.(x, y), z) -> .(x, ++(y, z))}
      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:
          {      rev nil() -> nil(),
                 rev rev x -> x,
              rev ++(x, y) -> ++(rev y, rev x),
              ++(x, nil()) -> x,
           ++(x, ++(y, z)) -> ++(++(x, y), z),
              ++(nil(), y) -> y,
            ++(.(x, y), z) -> .(x, ++(y, z))}
          SPSC:
           Simple Projection:
            pi(rev#) = 0
           Strict:
            {}
           Qed