Solution (source code)

= Solution

Suppose $G=\langle g_1,\ldots,g_n\mid R\rangle$ has a <finite group presentation>. Work in the <free product> $B=G*F(a,b)$ and put
$$
u_0=a,\quad u_i=b^{-i}ab^i,\qquad
v_0=b,\quad v_i=g_i a^{-i}ba^i\quad(1\le i\le n).
$$
The $u_i$ freely generate a subgroup of $F(a,b)$. Indeed, in a reduced word in these conjugates, combine adjacent powers with the same index. Expanding the remaining word leaves nonzero powers of $a$ separated by nonzero powers of $b$, so the <normal form theorem for a free product> makes it nonidentity. This proves the <free conjugate bases in a rank-two free group> fact we need.

The <group homomorphism> $B\to F(a,b)$ killing $G$ sends $v_i$ to $a^{-i}ba^i$, including $v_0=b$. These are a free conjugate basis by the same argument with $a,b$ interchanged. A nonempty reduced word in the $v_i$ therefore has nontrivial image and cannot be trivial in $B$. Thus $u_i\mapsto v_i$ extends to an <isomorphism> between the two rank-$(n+1)$ <free groups> embedded in $B$.

Adjoin one <stable letter> implementing this isomorphism:
$$
E=\langle g_1,\ldots,g_n,a,b,t\mid R,\ t^{-1}u_it=v_i\ (0\le i\le n)\rangle.
$$
We assume <Britton's lemma>, including its assertion that the base embeds in this <HNN extension>, and the factor-embedding assertion of the <normal form theorem for a free product>. Hence $G\hookrightarrow E$. The presentation is finite, and its relations express every generator in $a,t$:
$$
b=t^{-1}at,\qquad
g_i=t^{-1}b^{-i}ab^it\,(a^{-i}ba^i)^{-1}.
$$
Eliminating $b,g_i$ by <Tietze transformations> therefore gives \b[a two-generator finite presentation with $\boxed{G\hookrightarrow E=\langle a,t\rangle}$]. This explicitly constructs the <two-generator HNN embedding>; it does not rely on an arbitrary two-generator embedding preserving finite presentability.