TRS:
 {     rev(a()) -> a(),
       rev(b()) -> b(),
  rev(++(x, y)) -> ++(rev(y), rev(x)),
  rev(++(x, x)) -> rev(x)}
 MPO:
  Prec:
   rev > ++
   empty
  Strict:
   {}
   Weak:
    {}
  Qed