YES
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:
   Strict:
    {  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)}
   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))}
   EDG:
    {(++#(x, ++(y, z)) -> ++#(x, y), ++#(.(x, y), z) -> ++#(y, z))
     (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z))
     (++#(x, ++(y, z)) -> ++#(x, y), ++#(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#(y), rev#(++(x, y)) -> ++#(rev(y), rev(x)))
     (rev#(++(x, y)) -> rev#(y), rev#(++(x, y)) -> rev#(y))
     (rev#(++(x, y)) -> rev#(y), 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))
     (rev#(++(x, y)) -> rev#(x), rev#(++(x, y)) -> rev#(x))
     (rev#(++(x, y)) -> rev#(x), rev#(++(x, y)) -> rev#(y))
     (rev#(++(x, y)) -> rev#(x), rev#(++(x, y)) -> ++#(rev(y), rev(x)))
     (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(x, y))
     (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(++(x, y), z))
     (++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))}
    SCCS:
     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:
      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:
         Scc:
          {++#(x, ++(y, z)) -> ++#(x, y),
            ++#(.(x, y), z) -> ++#(y, z)}
         SCC:
          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(++#) = 0
           Strict:
            {++#(x, ++(y, z)) -> ++#(x, y)}
           EDG:
            {(++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(x, y))}
            SCCS:
             Scc:
              {++#(x, ++(y, z)) -> ++#(x, y)}
             SCC:
              Strict:
               {++#(x, ++(y, z)) -> ++#(x, 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(++#) = 1
               Strict:
                {}
               Qed
     SCC:
      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:
         Scc:
          {rev#(++(x, y)) -> rev#(y)}
         SCC:
          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