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)
  KBO Processor:
   argument filtering:
    pi(a) = []
    pi(rev) = [0]
    pi(b) = []
    pi(++) = [0,1]
    pi(rev#) = 0
   weight function:
    w0 = 1
    w(++) = w(b) = w(a) = 1
    w(rev#) = w(rev) = 0
   precedence:
    rev > rev# ~ ++ ~ b ~ a
   problem:
    DPs:
     
    TRS:
     rev(a()) -> a()
     rev(b()) -> b()
     rev(++(x,y)) -> ++(rev(y),rev(x))
     rev(++(x,x)) -> rev(x)
   Qed