(VAR N X XS ) (RULES after(s(N),cons(X)) -> after(N,XS) from(X) -> cons(X) after(0,XS) -> XS )