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)
  CDG 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)
   graph:
    
   Qed