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