YES

Problem:
 rev(a()) -> a()
 rev(b()) -> b()
 rev(++(x,y)) -> ++(rev(y),rev(x))
 rev(++(x,x)) -> rev(x)

Proof:
 DP Processor:
  DPs:
   rev#(++(x,y)) -> rev#(x)
   rev#(++(x,y)) -> rev#(y)
   rev#(++(x,x)) -> rev#(x)
  TRS:
   rev(a()) -> a()
   rev(b()) -> b()
   rev(++(x,y)) -> ++(rev(y),rev(x))
   rev(++(x,x)) -> rev(x)
  Subterm Criterion Processor:
   simple projection:
    pi(rev#) = 0
   problem:
    DPs:
     
    TRS:
     rev(a()) -> a()
     rev(b()) -> b()
     rev(++(x,y)) -> ++(rev(y),rev(x))
     rev(++(x,x)) -> rev(x)
   Qed