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