YES
TRS:
 {     rev(a()) -> a(),
       rev(b()) -> b(),
  rev(++(x, y)) -> ++(rev(y), rev(x)),
  rev(++(x, x)) -> rev(x)}
 DP:
  Strict:
   {rev#(++(x, y)) -> rev#(y),
    rev#(++(x, y)) -> rev#(x),
    rev#(++(x, x)) -> rev#(x)}
  Weak:
  {     rev(a()) -> a(),
        rev(b()) -> b(),
   rev(++(x, y)) -> ++(rev(y), rev(x)),
   rev(++(x, x)) -> rev(x)}
  EDG:
   {(rev#(++(x, x)) -> rev#(x), rev#(++(x, x)) -> rev#(x))
    (rev#(++(x, x)) -> rev#(x), rev#(++(x, y)) -> rev#(x))
    (rev#(++(x, x)) -> rev#(x), rev#(++(x, y)) -> rev#(y))
    (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, x)) -> rev#(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, x)) -> rev#(x))}
   SCCS:
    Scc:
     {rev#(++(x, y)) -> rev#(y),
      rev#(++(x, y)) -> rev#(x),
      rev#(++(x, x)) -> rev#(x)}
    SCC:
     Strict:
      {rev#(++(x, y)) -> rev#(y),
       rev#(++(x, y)) -> rev#(x),
       rev#(++(x, x)) -> rev#(x)}
     Weak:
     {     rev(a()) -> a(),
           rev(b()) -> b(),
      rev(++(x, y)) -> ++(rev(y), rev(x)),
      rev(++(x, x)) -> rev(x)}
     SPSC:
      Simple Projection:
       pi(rev#) = 0
      Strict:
       {rev#(++(x, y)) -> rev#(y),
        rev#(++(x, x)) -> rev#(x)}
      EDG:
       {(rev#(++(x, x)) -> rev#(x), rev#(++(x, x)) -> rev#(x))
        (rev#(++(x, x)) -> rev#(x), rev#(++(x, y)) -> rev#(y))
        (rev#(++(x, y)) -> rev#(y), rev#(++(x, y)) -> rev#(y))
        (rev#(++(x, y)) -> rev#(y), rev#(++(x, x)) -> rev#(x))}
       SCCS:
        Scc:
         {rev#(++(x, y)) -> rev#(y),
          rev#(++(x, x)) -> rev#(x)}
        SCC:
         Strict:
          {rev#(++(x, y)) -> rev#(y),
           rev#(++(x, x)) -> rev#(x)}
         Weak:
         {     rev(a()) -> a(),
               rev(b()) -> b(),
          rev(++(x, y)) -> ++(rev(y), rev(x)),
          rev(++(x, x)) -> rev(x)}
         SPSC:
          Simple Projection:
           pi(rev#) = 0
          Strict:
           {rev#(++(x, x)) -> rev#(x)}
          EDG:
           {(rev#(++(x, x)) -> rev#(x), rev#(++(x, x)) -> rev#(x))}
           SCCS:
            Scc:
             {rev#(++(x, x)) -> rev#(x)}
            SCC:
             Strict:
              {rev#(++(x, x)) -> rev#(x)}
             Weak:
             {     rev(a()) -> a(),
                   rev(b()) -> b(),
              rev(++(x, y)) -> ++(rev(y), rev(x)),
              rev(++(x, x)) -> rev(x)}
             SPSC:
              Simple Projection:
               pi(rev#) = 0
              Strict:
               {}
              Qed