TRS:
 {    bin(x, 0()) -> s(0()),
   bin(0(), s(y)) -> 0(),
  bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y))}
 LMPO:
  Quasi-Precedence:
  empty
  
Normal:
   pi(bin) = [1,2]
  
Safe:
   
  
Predicative System:
   {      bin(x,0();) -> s(0();),
      bin(0(),s(y;);) -> 0(),
    bin(s(x;),s(y;);) -> +(bin(x,s(y;);),bin(x,y;);)}
  

   
  

  Qed