= Solution
Fix a closed $T$ and an arbitrary closed target $M$. If $S$ is an <easy lambda term>, the extension by $S=\lambda x.M$, with fresh $x$, is consistent. In that extension
$$
ST=(\lambda x.M)T=M.
$$
The theory obtained by adding only $ST=M$ is a subtheory of this consistent extension, so it is consistent too. Thus \b[$ST$ is easy for every closed $T$]. The printed unrestricted wording requires this qualification because easiness was defined only for closed terms: if $T$ is open, $ST$ need not be closed. With easiness extended to equations between open terms, the same argument works for arbitrary $T$.
If an easy closed $S$ were a <solvable lambda term>, some finite sequence of closed arguments would give $SP_1\cdots P_k\equiv_\beta I$. Repeated application of the result above would make this term easy. Easiness is invariant under <beta equivalence>, so $I$ would be easy, contrary to the preceding calculation. Hence \b[every easy term is unsolvable].
Back to article page
