MAYBE MAYBE TRS: { sum(0()) -> 0(), sum(s(x)) -> +(sum(x), s(x)), +(x, 0()) -> x, +(x, s(y)) -> s(+(x, y)) } DUP: We consider a duplicating system. Trs: { sum(0()) -> 0(), sum(s(x)) -> +(sum(x), s(x)), +(x, 0()) -> x, +(x, s(y)) -> s(+(x, y)) } Fail