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