MAYBE
Trs:
 { bin(0(), s(y)) -> 0(),
  bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)),
      bin(x, 0()) -> s(0())}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open