YES

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

Proof:
 Bounds Processor:
  bound: 0
  enrichment: roof
  automaton:
   final states: {14,13,12,11,5,3,2,1}
   transitions:
    f40() -> 4*
    a0() -> 11*,6,5,1
    b0() -> 12*,6,5,2
    ++0(12,14) -> 13*
    ++0(13,5) -> 13*
    ++0(13,11) -> 13*
    ++0(13,13) -> 13*
    ++0(14,12) -> 13*
    ++0(14,14) -> 13*
    ++0(11,12) -> 13*
    ++0(6,12) -> 13*
    ++0(11,14) -> 13*
    ++0(6,14) -> 13*
    ++0(12,5) -> 13*
    ++0(12,11) -> 13*
    ++0(12,13) -> 13*
    ++0(13,12) -> 13*
    ++0(13,14) -> 13*
    ++0(14,5) -> 13*
    ++0(14,11) -> 13*
    ++0(14,13) -> 13*
    ++0(11,5) -> 13*
    ++0(6,5) -> 13*,6,5,3
    ++0(11,11) -> 13*
    ++0(6,11) -> 13*
    ++0(11,13) -> 13*
    ++0(6,13) -> 13*
    ++0(12,12) -> 13*
    rev0(4) -> 14*,6,5
    1 -> 5,6
    2 -> 5,6
    3 -> 5,6
  problem:
   
  Qed