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