MAYBE MAYBE TRS: { 0() -> n__0(), f(X) -> n__f(X), f(0()) -> cons(0(), n__f(n__s(n__0()))), f(s(0())) -> f(p(s(0()))), p(s(X)) -> X, s(X) -> n__s(X), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__0()) -> 0() } DUP: We consider a non-duplicating system. Trs: { 0() -> n__0(), f(X) -> n__f(X), f(0()) -> cons(0(), n__f(n__s(n__0()))), f(s(0())) -> f(p(s(0()))), p(s(X)) -> X, s(X) -> n__s(X), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__0()) -> 0() } Fail