TRS: { from(X) -> cons(X, from(s(X))), after(0(), XS) -> XS, after(s(N), cons(X, XS)) -> after(N, XS)} Fail