TRS:
 {    bin(x, 0()) -> s(0()),
   bin(0(), s(y)) -> 0(),
  bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y))}
 RPO Product:
  Quasi-Precedence:
  empty
  
  Qed


TRS:
 {    bin(x, 0()) -> s(0()),
   bin(0(), s(y)) -> 0(),
  bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y))}
 Fail