  We give a characterization, with respect to a large class of models of
untyped $\lambda$-calculus, of those models that are fully abstract for
head-normalization, i.e., whose equational theory is $\mathcal{H}^*$. An
extensional K-model $D$ is fully abstract if and only if it is hyperimmune,
i.e., non-well founded chains of elements of $D$ cannot be captured by any
recursive function.
  This article share its first title with its companion paper and a short
version. It is a standalone paper that present a purely syntactical proof of
the result as opposed to its companion paper that present an independent and
purely semantical proof of the exact same result.
