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)
  Usable Rule Processor:
   DPs:
    rev#(++(x,y)) -> rev#(x)
    rev#(++(x,y)) -> rev#(y)
    rev#(++(x,x)) -> rev#(x)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [rev#](x0) = x0,
     
     [++](x0, x1) = 3x0 + 1x1 + -2
    orientation:
     rev#(++(x,y)) = 3x + 1y + -2 >= x = rev#(x)
     
     rev#(++(x,y)) = 3x + 1y + -2 >= y = rev#(y)
     
     rev#(++(x,x)) = 3x + -2 >= x = rev#(x)
    problem:
     DPs:
      
     TRS:
      
    Qed