TRS:
 {     rev(a()) -> a(),
       rev(b()) -> b(),
  rev(++(x, y)) -> ++(rev(y), rev(x)),
  rev(++(x, x)) -> rev(x)}
 LMPO:
  Quasi-Precedence:
  empty
  
Normal:
   pi(rev) = [1]
  
Safe:
   
  
Predicative System:
   {     rev(a();) -> a(),
         rev(b();) -> b(),
    rev(++(x,y;);) -> ++(rev(y;),rev(x;);),
    rev(++(x,x;);) -> rev(x;)}
  

   
  

  Qed