\documentclass[11pt]{article} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{lmodern} \usepackage[margin=1.05in]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{microtype,booktabs,array,enumitem} \usepackage{xcolor,aliascnt} \usepackage{tikz} \usetikzlibrary{arrows.meta} \usepackage[colorlinks=true,linkcolor=blue!45!black, citecolor=green!35!black,urlcolor=blue!45!black]{hyperref} \usepackage[nameinlink,noabbrev,capitalise]{cleveref} \newtheorem{theorem}{Theorem}[section] \newaliascnt{lemma}{theorem} \newtheorem{lemma}[lemma]{Lemma} \aliascntresetthe{lemma} \newaliascnt{proposition}{theorem} \newtheorem{proposition}[proposition]{Proposition} \aliascntresetthe{proposition} \newaliascnt{corollary}{theorem} \newtheorem{corollary}[corollary]{Corollary} \aliascntresetthe{corollary} \theoremstyle{definition} \newaliascnt{definition}{theorem} \newtheorem{definition}[definition]{Definition} \aliascntresetthe{definition} \theoremstyle{remark} \newaliascnt{remark}{theorem} \newtheorem{remark}[remark]{Remark} \aliascntresetthe{remark} \crefname{lemma}{Lemma}{Lemmas} \Crefname{lemma}{Lemma}{Lemmas} \crefname{proposition}{Proposition}{Propositions} \Crefname{proposition}{Proposition}{Propositions} \crefname{corollary}{Corollary}{Corollaries} \Crefname{corollary}{Corollary}{Corollaries} \crefname{definition}{Definition}{Definitions} \Crefname{definition}{Definition}{Definitions} \crefname{remark}{Remark}{Remarks} \Crefname{remark}{Remark}{Remarks} \newcommand{\Z}{\mathbb Z} \newcommand{\F}{\mathrm F} \newcommand{\gp}[1]{\langle #1\rangle} \newcommand{\ncl}[1]{\langle\!\langle #1\rangle\!\rangle} \newcommand{\pres}[2]{\left\langle #1\ \middle|\ #2\right\rangle} \newcommand{\code}{\mathcal B_0} \newcommand{\Sim}{\mathcal K} \newcommand{\Row}{\mathcal R} \newcommand{\Null}{\mathcal N} \newcommand{\calA}{\mathcal A} \newcommand{\calB}{\mathcal B} \newcommand{\calC}{\mathcal C} \newcommand{\calE}{\mathcal E} \newcommand{\id}{1} \DeclareMathOperator{\expn}{exp} \numberwithin{equation}{section} \setlist[enumerate]{itemsep=3pt,topsep=5pt} \setlist[itemize]{itemsep=3pt,topsep=5pt} \setlength{\emergencystretch}{2em} \title{A universal group with thirteen relators} \author{} \date{} \begin{document} \maketitle \begin{abstract} We construct a finitely presented group with 13 relators that contains an isomorphic copy of every finitely presented group. This improves Valiev's bound of 21 relators for universal groups. The proof combines Valiev's construction, subgroup calculations of Kegel--Li--Ren, and small-cancellation theory. \end{abstract} \section{Introduction} \label{sec:introduction} A finitely presented group is \emph{universal} if every finitely presented group embeds in it. Higman's embedding theorem implies the existence of such a group \cite{Higman1961}. Boone--Collins obtained a universal group with 26 defining relators \cite{BooneCollins1974}, and Valiev reduced the number to 21 \cite{Valiev1977}. \begin{theorem}\label{thm:main} There exists a universal group with a presentation on 2 generators and 13 relators. \end{theorem} An explicit presentation of this group is given in \cref{sec:final}. The improvement in \cref{thm:main} concerns the number of relators. By \cite[Theorem IV]{HNN1949}, any universal group embeds in a 2-generator universal group with the same number of defining relators; adjoining free generators gives the same bound for any prescribed number of generators at least 2. The construction of the universal group begins by embedding a fixed universal finitely presented group in a group with 32 relators. \Cref{sec:coding} supplies Valiev's coding and recognition results, which \cref{sec:attachment} uses to construct this embedding. We reduce the count by exploiting the commutation relations between the factors of an embedded direct product. The normal-form results recalled in \cref{sec:normalforms} allow us to verify that each enlargement preserves the original embedded copy and therefore remains universal. \subsection*{Reducing the number of relators} The cross-commutation relations form a rectangular array, indexed by generators of the two factors. In \cref{sec:symmetry}, using the subgroup calculations of Kegel--Li--Ren \cite{KegelLiRen2026}, we realize a symmetry and successive row and column shifts by HNN extensions. Conjugating retained relations recovers other commutation relations, while the new conjugation equations allow us to eliminate generators. This gives a presentation with 6 generators and 19 relators. In \cref{sec:swap}, the final HNN extension conjugates one copy of a direct product of free groups of ranks 2 and 3 onto another. The preceding symmetry supplies a commutation relation needed for the first copy. To obtain the second, we use the small-cancellation construction of \cref{sec:preparation}, which prepares the initial embedding so that a later extension contains the required free subgroup of rank 3. We prove both direct-product decompositions, so the correspondence between their factor bases defines an isomorphism and the HNN embedding theorem applies. Adjoining the conjugating generator adds 5 relations. We choose the isomorphism so that these relations both make 5 old relators consequences of the relations we retain and allow us to solve for 5 old generators. Deleting the old relators and eliminating those generators together with the 5 new relations leaves 2 generators and 14 relators. One further commutation relation follows from the others, giving 13 relators. \paragraph*{Provenance.} GPT-6 Astra found the proof presented here and drafted the manuscript under the direction of Qiuyu Ren, who guided subsequent revisions. A Lean formalization of \cref{thm:main}, with verification instructions, is available in \cite{UniversalGroupLean}. \paragraph*{Acknowledgments.} We thank Cameron Gordon for suggesting this problem and for helpful correspondence. \section{Normal forms} \label{sec:normalforms} Throughout, $w^g=g^{-1}wg$ and $[w,g]=w^{-1}g^{-1}wg$. We write $\F(z_1,\ldots,z_j)$ when the displayed elements freely generate. We recall the normal-form theorems for amalgamated products and HNN extensions \cite{HNN1949,LyndonSchupp}. If $A$ is a common subgroup of $B$ and $C$, then the factors embed in $B*_A C$, and every nonempty alternating product of elements of $B\setminus A$ and $C\setminus A$ is nontrivial. For an HNN extension with base $B$, stable letter $t$, and relations $t^{-1}at=\phi(a)$ for an isomorphism $\phi:A\to A'$ between subgroups of $B$, the base embeds. We call such an extension proper. A \emph{pinch} is a subword $t^{-1}at$ with $a\in A$ or $ta't^{-1}$ with $a'\in A'$. Britton's lemma states that a word written with base-group elements between successive stable letters is nontrivial if it contains a stable letter and no pinch. These theorems give two restriction principles. In the HNN extension above, if $S\leq B$ satisfies $\phi(A\cap S)=A'\cap S$, then $\gp{S,t}$ has the exact HNN presentation with base $S$ and associated subgroups $A\cap S,A'\cap S$, and meets $B$ in $S$. For amalgamated products, $S*_D T$ embeds in $B*_A C$ if $S\leq B$, $T\leq C$, and their intersections with $A$ both equal $D$ under the identification. Both restriction principles follow because reduced words in the smaller construction remain reduced in the larger one. \section{Preparing the input} \label{sec:preparation} A positive word contains no inverse letters; we allow the empty word. We prepare a 2-generator group, called the input, whose positive relations define it as a monoid as well as a group. We also require 3 specified elements to generate a free subgroup in the HNN extension below, after the relations of this group have been imposed. \begin{proposition}\label{prop:preparation} Every finitely presented group $K$ embeds in a group $G=\pres{u_1,u_2}{R_G}$ with the following properties. \begin{enumerate}[label=\textup{(\roman*)}] \item Both $u_1$ and $u_2$ have infinite order. \item The set $R_G$ is a finite list of positive words, and the monoid defined by $R_G=1$ is $G$. \item The elements $b,cbc^{-1},c^3$ freely generate in \begin{equation}\label{eq:rowgroup} \Row(G)=\pres{G,c,\ell,b}{u_1^b=\ell,\ \ell^b=c,\ c^b=u_2} \cong\pres{b,c}{R_G(b^2cb^{-2},b^{-1}cb)}. \end{equation} The first presentation in \eqref{eq:rowgroup} is a proper HNN extension of $G*\gp{c}*\gp{\ell}$. We call $\Row(G)$ the row group. \end{enumerate} \end{proposition} We recall the small-cancellation conventions used in the proof. In a free product, a syllable is a nonidentity element of a free factor in reduced normal form, and $|w|$ is the number of syllables of $w$. A reduced word is weakly cyclically reduced if it has at most one syllable or its end syllables are not mutual inverses. Symmetrization includes inverses and all weakly cyclically reduced conjugates. A product is weakly reduced if no syllables cancel at the join, although the boundary syllables may combine. A weak initial part of $Q$ is a word $p$ such that $Q=pv$ is weakly reduced. A piece is a common weak initial part of two distinct symmetrized relators. The condition $C'(1/6)$ requires every piece to have length less than one sixth of the length of each of these relators. A part of a word means a subword of a weakly cyclically reduced conjugate, as in \cite[Definition 2.9]{PoorRinot}. \begin{theorem}[Free-product small cancellation]\label{thm:smallcancellation} For a symmetrized $C'(1/6)$ family with relator lengths greater than $6$, the free factors embed in the quotient. Every nonidentity weakly cyclically reduced word in the normal closure has a common part with some symmetrized relator $Q$, and this common part has length greater than $|Q|/2$. \end{theorem} For factor embedding see \cite[\S2.1, Theorem 2.1]{MartinSteenbock}; for the common-part statement see \cite[Fact 2.10]{PoorRinot}. A weakly cyclically reduced conjugate of a cyclically reduced alternating word is a rotation with possibly one syllable split between its ends, so its length increases by at most $1$ \cite[Observation 2.6]{PoorRinot}. \begin{lemma}\label{lem:pieces} If the second-factor syllables in cyclically reduced alternating relators of length at least $12$ are globally distinct and none is the inverse of another, every piece has length at most $5$. \end{lemma} \begin{proof} A common weak initial part of length $6$ contains an unchanged second-factor syllable away from its endpoints. That syllable determines the relator, orientation, and position; its location fixes the starting position, and the first syllable fixes any split. The two symmetrized relators would therefore coincide. \end{proof} \begin{proof}[Proof of \cref{prop:preparation}] Write $K=\pres{k_1,\ldots,k_n}{R_1,\ldots,R_s}$ and set $k_0=1$. Choose \[ \alpha_{ij}=3(120i+j)+1\quad(1\leq j\leq120),\qquad W_i(u,v)=u^{\alpha_{i1}}v^{\alpha_{i2}}\cdots u^{\alpha_{i,119}}v^{\alpha_{i,120}} \quad(0\leq i\leq n). \] The exponents are positive, globally distinct, and congruent to $1$ modulo $3$. Define \begin{equation}\label{eq:preparedrelative} G=(K*\gp{u}*\gp{v})/\ncl{k_iW_i(u,v):0\leq i\leq n}. \end{equation} Here double angle brackets denote normal closure. Over $(K*\gp{u})*\gp{v}$, each relator has cyclically reduced length $120$, and the $v$-syllables are distinct across all relators. Its first syllable $k_i u^{\alpha_{i1}}$ is nontrivial even when $k_i=1$. The symmetrized lengths are $120$ or $121$, and the piece bound $5$ gives $C'(1/6)$. Thus $K*\gp{u}$ and $\gp{v}$ embed, preserving $K$ and the infinite orders of $u,v$. Using $k_i=W_i^{-1}$ to eliminate $k_1,\ldots,k_n$ gives the finite presentation on $u,v$ with relators \begin{equation}\label{eq:preparedfinite} W_0,\qquad R_j(W_1^{-1},\ldots,W_n^{-1})\quad(1\leq j\leq s). \end{equation} Write $W_0=uU$ and choose a cyclic rotation $vV$ of $W_0$. In $G$ we have $uU=Uu=vV=Vv=1$. Replace inverse letters in \eqref{eq:preparedfinite} by the positive words $U,V$ and include those 4 inverse relations. Every element of the resulting monoid is invertible, and its group presentation is equivalent to \eqref{eq:preparedfinite}. This gives the required positive presentation, with $u_1=u,u_2=v$. The triples $(u,\ell,c)$ and $(\ell,c,v)$ freely generate in $G*\gp{c}*\gp{\ell}$, so the row extension is proper. Its equations give $u=b^2cb^{-2}$, $v=b^{-1}cb$, and $\ell=bcb^{-1}$, hence \begin{equation}\label{eq:rowrelative} \Row(G)=(K*\gp{b}*\gp{c})/ \ncl{k_iW_i(b^2cb^{-2},b^{-1}cb):0\leq i\leq n}. \end{equation} Over $(K*\gp{b})*\gp{c}$, a cyclic conjugate of each relator is \begin{equation}\label{eq:rowrelator} c^{\alpha_{i1}}b^{-3}c^{\alpha_{i2}}b^3\cdots c^{\alpha_{i,119}}b^{-3}c^{\alpha_{i,120}}(bk_i b^2). \end{equation} The last syllable is nontrivial, and equals $b^3$ when $k_i=1$. The cyclically reduced length is $240$. The distinct $c$-powers again bound pieces by $5$, while symmetrized lengths are $240$ or $241$. The subgroup $L_0=\gp{b,cbc^{-1},c^3}\leq\F(b,c)$ is represented by a directed 3-edge $c$-cycle on vertices $0,1,2$, with $b$-loops only at $0,1$, based at $0$. The first two $c$-edges form a spanning tree and give the displayed free basis. Any 4 successive complete $c$-blocks of \eqref{eq:rowrelator}, with their 3 intervening $b$-blocks, cannot be read in this graph: each $c$-block advances one vertex modulo $3$, forcing a $b$-block at vertex $2$. For the inverse relator the same argument uses steps of $-1$. \begin{figure}[ht] \centering \begin{tikzpicture}[vertex/.style={circle,draw,minimum size=7mm,inner sep=0pt}] \node[vertex] (v0) at (0,0) {$0$}; \node[vertex] (v1) at (3,0) {$1$}; \node[vertex] (v2) at (1.5,-1.7) {$2$}; \draw[-{Stealth[length=2mm]},semithick] (v0) -- node[above] {$c$} (v1); \draw[-{Stealth[length=2mm]},semithick] (v1) -- node[right] {$c$} (v2); \draw[-{Stealth[length=2mm]},semithick] (v2) -- node[left] {$c$} (v0); \draw[-{Stealth[length=2mm]},semithick] (v0) edge[loop left,looseness=5] node[left] {$b$} (v0); \draw[-{Stealth[length=2mm]},semithick] (v1) edge[loop right,looseness=5] node[right] {$b$} (v1); \end{tikzpicture} \caption{The based labeled graph representing $L_0=\gp{b,cbc^{-1},c^3}$; the base vertex is $0$.} \label{fig:protectedsubgroup} \end{figure} If a nontrivial element of $L_0$ dies in the row quotient, cyclic reduction gives a nontrivial closed-path label, possibly at a different vertex. Combining end syllables in the same factor preserves this property. A one-syllable word cannot die because the factors embed. Otherwise \cref{thm:smallcancellation} gives a common part of at least $121$ syllables in weakly cyclically reduced conjugates of the closed-path label and of a row relator or its inverse. Only the end syllables can differ from the corresponding cyclic rotations \cite[Observation 2.6]{PoorRinot}. Removing 2 syllables at each end of the common part therefore leaves at least $117$ unchanged consecutive syllables of the row relator or its inverse, all readable in the graph. Every first-factor syllable of the path label is a $b$-power, so the exceptional syllable $bk_i b^2$ cannot occur in this interior if $k_i\ne1$. If $k_i=1$, it is a nonzero $b$-power. In either case the interior contains the forbidden 4 $c$-blocks. Thus $L_0$ embeds in $\Row(G)$. \end{proof} \section{The coding and simulator inputs} \label{sec:coding} Fix $G$ from \cref{prop:preparation}. Let $\Null$ be the positive words in $u_1,u_2$ representing $1$ in $G$, equivalently in its positive monoid presentation. \begin{theorem}[Classical 3-rule coding]\label{thm:coding} There are positive words $E_i,F_i$ $(1\leq i\leq3)$, $\bar g_1,\bar g_2,P$ on $s_1,s_2$ with the following properties. In the semigroup \[ S=\pres{s_1,s_2}{E_i=F_i\quad(1\leq i\leq3)}, \] we have $w\in\Null$ if and only if $w(\bar g_1,\bar g_2)P=_S P$, for every positive word $w$ in $u_1,u_2$. Here $=_S$ denotes equality in $S$, and the 3 equations $E_i=F_i$ are its rules. Every positive word $v$ in $s_1,s_2$ satisfying $vP=_S P$ is literally a concatenation of $\bar g_1,\bar g_2$. The datum can be chosen effectively, with every rule side containing both letters and, for suitable integers $N\geq3$, $\nu\geq0$, \begin{align} \bar g_1&=(s_1s_2)^2s_1^2s_2s_1^N,& \bar g_2&=(s_1s_2)^2s_1^3s_2s_1^{N-1},\label{eq:codes}\\ P&=(s_1s_2)^2s_1^4s_2s_1^{N-1}s_2^{2\nu}.\label{eq:marker} \end{align} \end{theorem} These are the recognition and literal-decoding properties stated in \cite[\S3, p.~208]{Valiev1977}, from the coding of \cite{BCM1971,BooneCollins1974}; see also \cite{Matiyasevich1995}. Every rule side contains both letters, as follows directly from the Boone--Collins formulas \cite[p.~2]{BooneCollins1974}: their two short rules are \begin{equation}\label{eq:shortrules} s_1s_2^2=s_2^2s_1s_2s_1,\qquad s_1s_2^2=s_2^2s_1^2, \end{equation} and both sides of the third rule contain $s_1s_2$. We use these coding words, chosen from $G$, throughout. In $\F(s_1,s_2)$ the codewords freely generate $\code=\gp{\bar g_1,\bar g_2}$: they are distinct positive words of equal length, so cannot be powers of a common root. Their common abelianization vector is $(N+4,3)$. Consequently \begin{equation}\label{eq:codecyclic} \code\cap z^{-1}\gp{s_j}z=1 \qquad(z\in\F(s_1,s_2),\ j=1,2), \end{equation} since no nonzero power of either letter has abelianization on that line. \subsection{The structural input} \label{sec:simulator} Define the first two stages of Valiev's auxiliary group, called the simulator, by \begin{equation}\label{eq:g0} G_0=\pres{d,e,s_1,s_2}{s_j^{-1}d^4s_j=d,\ s_j^{-1}es_j=e^4\quad(j=1,2)}, \end{equation} \begin{equation}\label{eq:gc} G_c=\pres{G_0,c}{[c,s_j]=1\ (j=1,2),\ c^{-1}A_i c=B_i\ (1\leq i\leq3)}, \end{equation} where $A_i=d^iF_i e^i$ and $B_i=d^iE_i e^i$. The last 3 equations also read \begin{equation}\label{eq:rulegroup} d^{-i}cd^iE_i=F_i e^i c e^{-i}\qquad(1\leq i\leq3). \end{equation} These are the presentations of $\Gamma_1,\Gamma_2$ in \cite{KegelLiRen2026}, with our input-dependent coding datum substituted. Their Propositions 3.3--3.4 are Borisov's normal-form statements for arbitrary nonempty positive rule words: his original formulation allows $M$ rules and any exponent $\alpha>M$ \cite[\S2, Assertions IV--V, pp.~769--770]{Borisov1969}. Here $M=3$ and $\alpha=4$. In the proof of their Lemma 3.5, the only additional property of the rule words is that every $E_i$ and $F_i$ contains both $s_1$ and $s_2$: this gives the intersections with $\gp{d,e,s_j}$ stated in the next lemma. This property holds by \cref{thm:coding}. No other property of the coding datum enters these subgroup proofs. Consequently their Propositions 3.3--3.4, Lemma 3.5, and Corollaries 3.6--3.7 apply to the datum chosen from each input $G$. \begin{lemma}[{\cite[Propositions 3.3--3.4, Lemma 3.5]{KegelLiRen2026}}]\label{lem:rankfive} The displayed lists freely generate \[ U_c=\gp{s_1,s_2,A_1,A_2,A_3},\qquad V_c=\gp{s_1,s_2,B_1,B_2,B_3}. \] For $J_j=\gp{d,e,s_j}\leq G_0$, their intersections with $J_j$ are $\gp{s_j}$, and their intersections with $\F(d,e)$ are trivial. \end{lemma} \begin{corollary}[{\cite[Corollaries 3.6--3.7]{KegelLiRen2026}}]\label{cor:singleletter} In $G_c$, the subgroup on $c,d,e$ is free and meets $G_0$ in $\F(d,e)$. For $j=1,2$, the subgroup $D_j=\gp{d,e,c,s_j}$ has the exact presentation \[ \pres{d,e,c,s_j}{s_j^{-1}d^4s_j=d,\ s_j^{-1}es_j=e^4,\ [c,s_j]=1}, \] and $D_j\cap G_0=J_j$. \end{corollary} The normal forms in $G_c$ also give $D_j\cap\F(s_1,s_2)=\gp{s_j}$. Adjoin stable letters $f,q,k$ that centralize the indicated subgroups: \begin{equation}\label{eq:L} L=\pres{G_c,f,q}{[f,c]=[f,d]=[q,c]=[q,e]=1}, \end{equation} \[ t=qf,\qquad T=PqP^{-1}f=Pt f^{-1}P^{-1}f,\qquad D=\gp{c,d,T}, \] \begin{equation}\label{eq:simK} \Sim=\pres{L,k}{[k,c]=[k,d]=[k,T]=1}. \end{equation} All these extensions are proper. The resulting Valiev simulator has 8 generators and 16 relators \cite[\S4, pp.~208--209]{Valiev1977}; its base is Borisov's construction \cite{Borisov1969}. \begin{lemma}\label{lem:F4} The subgroup $F_4=\gp{s_1,s_2,f,q}$ is free on these elements, and $F_4\cap G_c=\F(s_1,s_2)$. \end{lemma} \begin{proof} The subgroup $\F(s_1,s_2)$ meets $\gp{c,d}$ and $\gp{c,e}$ trivially. Restricting successively the $f$ and $q$ extensions therefore adjoins two free factors and preserves the stated base intersection. \end{proof} \subsection{Recognition} \label{sec:recognition} The recognition theorem detects the words representing $1$ in $G$ through intersections of subgroups of $\Sim$. In $\Sim$, set \[ x_0=k^{-1}fk,\quad x_1=f^{-1}s_1f,\quad x_2=f^{-1}s_2f,\quad x_3=Pt, \] \[ \calA=\gp{\bar g_1,\bar g_2,x_1,x_2,x_3},\quad \calB=\gp{\bar g_1,\bar g_2,f,T},\quad V=\gp{x_0,x_1,x_2,x_3}. \] For positive $w=w(u_1,u_2)$ write $\bar w=w(\bar g_1,\bar g_2)$ and \begin{equation}\label{eq:delta} \Delta(w)=\bar wT f^{-1}\bar w^{-1}f =\bar w x_3f^{-1}(\bar wP)^{-1}f. \end{equation} \begin{theorem}[Valiev's recognition theorem]\label{thm:recognition} The subgroup $V$ is free on $x_0,x_1,x_2,x_3$, and \begin{equation}\label{eq:intersection} D\cap\calA=D\cap\calB=\calE, \qquad\calE=\gp{\Delta(w):w\in\Null}. \end{equation} \end{theorem} Equation \eqref{eq:intersection} is \cite[Lemma 5.1, pp.~209--210]{Valiev1977}. The freeness of $V$ is stated in \cite[Lemma 8.1(a), pp.~211--212]{Valiev1977} for its image in a later extension of the same simulator, and therefore holds already in $\Sim$. In particular, \begin{equation}\label{eq:recognized} \Delta(w)^k=\Delta(w)\qquad(w\in\Null). \end{equation} \begin{lemma}\label{lem:recognizeramalgam} The displayed generators freely generate $\calA,\calB$. Moreover, \[ \calC:=\gp{\calA,k^{-1}\calB k} \cong\calA*_{\calE}k^{-1}\calB k, \qquad \calC\cap L=\calA. \] The element $c$ centralizes $V$. \end{lemma} \begin{proof} In $F_4$, the code subgroup and $f^{-1}\F(s_1,s_2)f$ form a free product. Replacing $q$ by $x_3=Pqf$ gives the asserted basis of $\calA$; replacing it by $T=PqP^{-1}f$ gives that of $\calB$. A $k$-pinch between the two factors occurs precisely in their intersections with $D$, both equal to $\calE$. Britton's lemma gives the amalgam and base intersection. The last assertion follows from the commutations of $c$ with $s_1,s_2,f,q,k$. \end{proof} \section{Attaching the input} \label{sec:attachment} Attach $G$ to $\Sim$ by making it commute with the free subgroup $V$: \begin{equation}\label{eq:smalleramalgam} M=\Sim*_V(V\times G). \end{equation} Both $G$ and $\Sim$ embed in $M$, whose presentation adds just the 8 commutations \begin{equation}\label{eq:inputgrid} [u_i,x_j]=1\qquad(i=1,2;\ 0\leq j\leq3). \end{equation} Let $\rho:M\to\Sim$ be the retraction killing $G$. Define $\psi$ on the two factors of $\calC$ by \[ \psi(\bar g_i)=\bar g_i f u_i f^{-1},\qquad \psi(x_j)=x_j\ (j=1,2,3),\qquad \psi|_{k^{-1}\calB k}=\mathrm{id}. \] The freeness of $\calA$ ensures that the assignment on its generators defines a homomorphism. Since $fu_if^{-1}$ commutes with $s_1,s_2$ by \eqref{eq:inputgrid}, this homomorphism sends $\bar w$ to $\bar w f w(u_1,u_2)f^{-1}$. For $w\in\Null$ this is $\bar w$, and the expression for $\Delta(w)$ in the $\calA$-basis is fixed. The factor maps thus agree on $\calE$. They define $\psi:\calC\to M$, which is injective because $\rho\psi$ is the original inclusion. Put $\calC'=\psi(\calC)$. Adjoin $\ell$ implementing this isomorphism, with 2 equations \begin{equation}\label{eq:attachment} \bar g_i\ell=\ell\bar g_i f u_i f^{-1}\quad(i=1,2) \end{equation} and the 7 commutations of $\ell$ with \begin{equation}\label{eq:ellnine} x_0,x_1,x_2,x_3,\quad k^{-1}\bar g_1k,\ k^{-1}\bar g_2k,\ k^{-1}Tk. \end{equation} The extension is proper. The recognition theorem lets us derive the input relators from these relations, removing the dependence of the relator count on $G$. \begin{lemma}\label{lem:deleteinput} Every defining relator of $G$ follows from the simulator relations, the cross-commutations \eqref{eq:inputgrid}, and the attaching relations. The commutation of $\ell$ with the last word in \eqref{eq:ellnine} is also redundant. \end{lemma} \begin{proof} Omit all input relators and let $w$ be one of them. The fixed simulator still satisfies \eqref{eq:recognized}, since its coding words and rules were chosen from the input presentation. The expression $k^{-1}\Delta(w)k$ is fixed by $\ell$. On the other hand, conjugating the $\calA$ expression in \eqref{eq:delta} by $\ell$ gives \[ \bar w f w(u_1,u_2)f^{-1}x_3f^{-1}(\bar wP)^{-1}f. \] The suffix $x_3f^{-1}(\bar wP)^{-1}f$ is fixed, being a word in $x_1,x_2,x_3$. Comparing with $\Delta(w)=k^{-1}\Delta(w)k$ and cancelling gives $w(u_1,u_2)=1$ without using any input relator. Finally, $k^{-1}Tk=T=x_3P(x_1,x_2)^{-1}$ is already fixed by $\ell$. \end{proof} After these deletions the group, denoted $N$, still contains $G$ and has 11 generators and $16+8+9-1=32$ relators. \begin{lemma}\label{lem:initialgrid} In $N$, the subgroup $U=\gp{c,u_1,u_2,\ell}$ is $\gp{c}*G*\gp{\ell}$, and $\gp{U,V}=U\times V$. \end{lemma} \begin{proof} The $c$-exponent map $\Sim\to\Z$ vanishes on $\calC$ and $V$, so each meets $\gp{c}$ trivially. Amalgam normal forms give $\gp{c,G}=\gp{c}*G$ and $\gp{c,G}\cap\Sim=\gp{c}$. Hence $\gp{c,G}\cap\calC=1$. Its intersection with $\calC'$ is also trivial: $\rho$ maps it into $\gp{c}\cap\calC$, and $\rho$ is injective on $\calC'$. Restriction of the $\ell$ extension therefore adds the free factor $\gp{\ell}$. An element of $U\cap V$ must then lie in $\gp{c,G}\cap\Sim=\gp{c}$, hence is trivial. The defining relations give $[U,V]=1$, so $\gp{U,V}\cong U\times V$. \end{proof} We view the commutations between the generators of $U$ and $V$ as a grid, with rows $c,u_1,u_2,\ell$ and columns $x_0,x_1,x_2,x_3$. Each entry is the commutation of its row and column generators. The next extensions use conjugation to recover several entries from a single row or column. \section{The positive symmetry and the 19-relator host} \label{sec:symmetry} We extend a symmetry of the subgroups associated with $s_1$ and $s_2$ across the attachment. The new letter $h$ will satisfy $[d,h^2]=1$, a relation needed for the final HNN extension in \cref{sec:swap}. Put $E_0=f^{-1}ef$, $Q_0=f^{-1}qf$, and \[ H_-=\gp{d,E_0,c,f,x_1},\qquad H_+=\gp{d,E_0,c,Q_0,x_2}. \] The symmetry will exchange $d$ and $E_0$ without inversion; this is the meaning of ``positive.'' \begin{lemma}\label{lem:singleletterH} These groups have the exact presentations \begin{align*} H_-&\cong\pres{d,E_0,c,f,x_1}{x_1^{-1}d^4x_1=d,\ x_1^{-1}E_0x_1=E_0^4,\ [c,x_1]=[c,f]=[d,f]=1},\\ H_+&\cong\pres{d,E_0,c,Q_0,x_2}{x_2^{-1}d^4x_2=d,\ x_2^{-1}E_0x_2=E_0^4,\ [c,x_2]=[c,Q_0]=[E_0,Q_0]=1}, \end{align*} and \begin{equation}\label{eq:Hintersections} \calC\cap H_-=V\cap H_-=\gp{x_1},\qquad \calC\cap H_+=V\cap H_+=\gp{x_2}. \end{equation} \end{lemma} \begin{proof} Restrict the $f$ extension to $D_1$ and conjugate by $f$ to obtain $H_-$. For $H_+$, restrict the independent $q$ extension to $D_2$ and conjugate by $f$. The letters $f$ and $q$ centralize $c,d$ and $c,e$, respectively; thus \cref{cor:singleletter} and the HNN restriction principle in \cref{sec:normalforms} give the presentations. The same restrictions and $D_j\cap\F(s_1,s_2)=\gp{s_j}$ give \[ H_-\cap F_4=\gp{s_1,f},\qquad H_+\cap F_4=f^{-1}\gp{s_2,q}f. \] Since $\calC\cap L=\calA\subset F_4$, the remaining intersections are free-group calculations. By \eqref{eq:codecyclic}, $\calA\cap\gp{s_1,f}=\gp{x_1}$. For the second, replace $f$ in a free basis of $F_4$ by $a_0=fPq$; then \[ f\calA f^{-1}=\gp{s_1,s_2,a_0,\ q^{-1}(P^{-1}\code P)q}. \] The intersection $P^{-1}\code P\cap\gp{s_2}=1$ implies that this group meets $\gp{s_2,q}$ in $\gp{s_2}$. This gives the $\calC$ intersections. The $V$ intersections follow from $V\subset\calC$ and $x_1,x_2\in V$. \end{proof} The positive assignment \begin{equation}\label{eq:positivemap} d\mapsto E_0,\quad E_0\mapsto d,\quad c\mapsto c,\quad f\mapsto Q_0,\quad x_1\mapsto x_2^{-1} \end{equation} is an isomorphism $H_-\to H_+$. It sends the two power relations to $x_2E_0^4x_2^{-1}=E_0$ and $x_2dx_2^{-1}=d^4$, equivalent to the target relations, and transports the commutations. The reverse assignment is its inverse. \begin{lemma}\label{lem:extendH} The map \eqref{eq:positivemap} extends, fixing $G,\ell$, to an isomorphism $\gp{H_-,G,\ell}\to\gp{H_+,G,\ell}$. These subgroups meet $U\times V$ in $U\times\gp{x_1}$ and $U\times\gp{x_2}$, respectively. \end{lemma} \begin{proof} By \eqref{eq:Hintersections}, adjoining $G$ in the amalgam adds exactly the commutations $[u_i,x_1]$ or $[u_i,x_2]$. The resulting subgroups meet $\Sim$ in $H_\pm$, hence meet $\calC$ in the indicated cyclic subgroups. Their intersections with $\calC'$ are the same: apply $\rho$, which is injective on $\calC'$, and use that $\psi$ fixes $x_1,x_2$. Restriction of the $\ell$ extension therefore adds exactly $[\ell,x_1]$ or $[\ell,x_2]$, so the map extends. The retraction $\rho:M\to\Sim$ extends to $\widehat\rho:N\to\Sim$ by $\ell\mapsto1$, since $\rho\psi$ is the inclusion of $\calC$. Put $S_\pm=\gp{H_\pm,G,\ell}$. Then $\widehat\rho(S_\pm)=H_\pm$ and $\widehat\rho$ fixes $V$. If $uv\in S_\pm\cap(U\times V)$, with $u\in U$ and $v\in V$, then $U\leq S_\pm$ gives $v\in S_\pm$. Thus $v=\widehat\rho(v)\in H_\pm\cap V$, which is $\gp{x_1}$ or $\gp{x_2}$ by \eqref{eq:Hintersections}. The reverse inclusions follow from the generators. \end{proof} Adjoin $h$ implementing this isomorphism, with 8 equations \begin{equation}\label{eq:hrelations} \begin{gathered} d^h=E_0,\quad E_0^h=d,\quad c^h=c,\quad f^h=Q_0,\quad x_1^h=x_2^{-1},\\ u_1^h=u_1,\quad u_2^h=u_2,\quad \ell^h=\ell. \end{gathered} \end{equation} Conjugating the retained source relations recovers 8 old ones: the two $s_2$ power relations, $[c,s_2]$, $[c,q]$, $[e,q]$, the two $[u_i,x_2]$, and $[\ell,x_2]$. Delete these and eliminate $e,s_2,q$ using \begin{equation}\label{eq:hdefinitions} \begin{aligned} e&=fh^{-1}dhf^{-1},&s_2&=fh^{-1}x_1^{-1}hf^{-1},\\ q&=fh^{-1}fhf^{-1},&t&=fh^{-1}fh. \end{aligned} \end{equation} The remaining equation $E_0^h=d$ is \begin{equation}\label{eq:hsquare} [d,h^2]=1. \end{equation} This leaves 9 generators and $32+8-8-3=29$ relators. By the intersection statement in \cref{lem:extendH}, restriction to the grid gives \begin{equation}\label{eq:hgrid} \gp{U,V,h}\cong U\times \pres{x_0,x_1,x_2,x_3,h}{x_1^h=x_2^{-1}} \cong U\times\F(x_0,x_1,h,x_3), \end{equation} and its intersection with $N$ is $U\times V$. \subsection{Column and row shifts} \label{sec:columnrow} Restore $[c,x_3]=1$, which follows from the commutations of $c$ with $s_1,f,h$ and \eqref{eq:hdefinitions}. Of the resulting 30 relators, 18 can equivalently be written \begin{equation}\label{eq:18block} \begin{gathered} [z,v]=1\quad(z\in\{c,u_1,u_2,\ell\},\ v\in\{x_0,x_1,h,x_3\}),\\ [c,k]=[d,f]=1. \end{gathered} \end{equation} For example, $[c,x_0]$ and $[c,k]$ recover $[c,f]$, after which $[c,x_1]$ recovers $[c,s_1]$. Adjoin $a$ fixing $U$ and satisfying \begin{equation}\label{eq:ashift} x_0^a=x_1,\qquad x_1^a=h,\qquad h^a=x_3. \end{equation} The source and target are $U\times\F(x_0,x_1,h)$ and $U\times\F(x_1,h,x_3)$ inside \eqref{eq:hgrid}, so this extension is proper. Retaining the $x_0$ column and the 4 new commutations with $a$ recovers the other 12 grid entries. The first two shifts eliminate the actual generators $s_1,h$; the third remains as $Pt=x_0^{a^3}$. The count is $30+7-12-2=23$, on 8 generators. Restriction to the grid gives \begin{equation}\label{eq:agrid} \gp{U,a,x_0}\cong U\times\F(a,x_0), \end{equation} since the 3 column symbols $x_1,h,x_3$ can be eliminated from this subgroup presentation. Only $s_1$ and $h$ were eliminated from the presentation of the whole group; $x_1,x_3$ were word abbreviations there. Next adjoin $b$ fixing $a,x_0$ and satisfying \begin{equation}\label{eq:bshift} u_1^b=\ell,\qquad \ell^b=c,\qquad c^b=u_2. \end{equation} The row triples are free in $U=\gp{c}*G*\gp{\ell}$, and their products with $\F(a,x_0)$ are the exact associated subgroups. This is again proper. Eliminate $\ell,u_1,u_2$ by \begin{equation}\label{eq:bdefinitions} \ell=bcb^{-1},\qquad u_1=b^2cb^{-2},\qquad u_2=b^{-1}cb. \end{equation} Since $a,x_0$ commute with $b,c$, they also commute with the displayed words for $\ell,u_1,u_2$. Deleting these 6 commutations leaves $23+5-6-3=19$ relators on $c,d,f,k,a,b$. Call this host $B_{19}^{+}$, and put $x=x_0$. Both associated subgroups lie in \eqref{eq:agrid}, with $b$ acting identically on the column factor. Restriction therefore gives the embedded product \begin{equation}\label{eq:bgrid} \gp{U,b,a,x}\cong\Row(G)\times\F(a,x). \end{equation} The row relations are exactly those of \eqref{eq:rowgroup}. \subsection{The 19-relator presentation} For reference, the word abbreviations in $B_{19}^{+}$ are \begin{equation}\label{eq:19words} \begin{aligned} x&=k^{-1}fk,&x_1&=a^{-1}xa,&h&=a^{-2}xa^2,\\ s_1&=fx_1f^{-1},&s_2&=fh^{-1}x_1^{-1}hf^{-1},&e&=fh^{-1}dhf^{-1},\\ t&=fh^{-1}fh,&\ell&=bcb^{-1},&u_1&=b^2cb^{-2},\quad u_2=b^{-1}cb. \end{aligned} \end{equation} The coding words are evaluated at $s_1,s_2$, and $T=Pt f^{-1}P^{-1}f$. The 12 core equations are \begin{equation}\label{eq:19core} \begin{aligned} d^4s_1&=s_1d,&es_1&=s_1e^4,\\ d^{-i}cd^iE_i&=F_i e^i c e^{-i}&&(i=1,2,3),\\ [T,k]&=1,\\ \bar g_i\ell&=\ell\bar g_i f u_i f^{-1}&&(i=1,2),\\ [\ell,k^{-1}\bar g_i k]&=1&&(i=1,2),\\ [d,h^2]&=1,&Pt&=a^{-3}xa^3. \end{aligned} \end{equation} The other 7 are \begin{equation}\label{eq:19comm} [c,f]=[d,f]=[c,k]=[d,k]=[c,a]=[a,b]=[b,x]=1. \end{equation} Here we have replaced the retained $[c,x]$ by $[c,f]$, using $[c,k]$ and $x=k^{-1}fk$. \section{Compression to 13 relators} \label{sec:swap} Write $\F_j$ for a free group of rank $j$. We exhibit two copies of $\F_2\times\F_3$ to serve as the source and target of an HNN extension. The source uses the relation $[d,h^2]=1$; the target uses the free triple $b,cbc^{-1},c^3$ in $\Row(G)$ supplied by \cref{prop:preparation}. \begin{lemma}\label{lem:source} The host $B_{19}^{+}$ contains the exact product \[ \gp{c,d,f,k,h^2}=\F(c,d)\times\F(f,k,h^2). \] \end{lemma} \begin{proof} The pair $c,d$ is free by \cref{cor:singleletter}, and commutes with $f,k,h^2$ by \eqref{eq:19comm}, \eqref{eq:hsquare}, and $c^h=c$. We next show that $f,k,h^2$ freely generate. In the group obtained after adjoining $h$, before the $a,b$ extensions, take the quotient killing $c,d,s_1,u_1,u_2,\ell$. The definitions then kill $e,s_2$ and the coding words, leaving exactly \[ Q=\pres{f,h,k}{[k,ff^h]=1}. \] First consider the intersection needed to restrict this centralizer extension. In $\F(f,h)$, the subgroup of words with even exponent sum in $h$ has free basis $(f,f^h,h^2)$. The exponent-sum map in the basis element $f^h$ vanishes on $\gp{f,h^2}$ but is nonzero on every nontrivial power of $ff^h$. Hence \[ \gp{f,h^2}\cap\gp{ff^h}=1. \] Now apply the HNN restriction principle to the extension defining $Q$: because the associated subgroup has trivial intersection with $\gp{f,h^2}$, the subgroup $\gp{f,h^2,k}$ is the free product $\gp{f,h^2}*\gp{k}$ and is therefore free on $f,h^2,k$. Finally, the quotient map above kills $\gp{c,d}$ and is injective on $\gp{f,k,h^2}$. The two factors therefore have trivial intersection; since they commute, they generate the displayed direct product. The subsequent proper extensions preserve it. \end{proof} Set \begin{equation}\label{eq:targetwords} B=cbc^{-1},\qquad A=Bc^3B^{-1},\qquad C=b. \end{equation} The triple $(b,B,c^3)$ is free in $\Row(G)$ by preparation. Permuting its basis and conjugating $c^3$ by $B$ gives the basis $(A,B,C)$. Thus \eqref{eq:bgrid} contains \begin{equation}\label{eq:targetproduct} \gp{a,x,A,B,C}=\F(a,x)\times\F(A,B,C). \end{equation} Adjoin $r$ with \begin{equation}\label{eq:rrelations} c^r=a,\qquad d^r=x,\qquad f^r=A,\qquad k^r=B,\qquad(h^2)^r=b. \end{equation} The source and target bases define an isomorphism, so this HNN extension is proper and contains $B_{19}^{+}$. \begin{lemma}\label{lem:fivedeletions} Retaining $[c,a],[a,b],[b,x]$, the 5 old relators $[c,f],[c,k],[d,f],[d,k],[d,h^2]$ are redundant. \end{lemma} \begin{proof} We recover the 5 relations in three successive stages. First, $a$ centralizes $b,c$, and therefore centralizes the words $A,B$. Pulling back $[a,A]=[a,B]=1$ through \eqref{eq:rrelations} gives $[c,f]=[c,k]=1$. These two recovered relations and $x=k^{-1}fk$ give $[c,x]=1$. Together with the retained relation $[b,x]=1$, this shows that $x$ centralizes both $A$ and $B$. Pulling back $[x,A]=[x,B]=1$ now gives $[d,f]=[d,k]=1$. Finally, pulling back $[x,b]=1$ gives $[d,h^2]=1$. Thus each relation is recovered before it is used in the next stage. \end{proof} \begin{lemma}\label{lem:fiveeliminations} The 5 equations \eqref{eq:rrelations} eliminate the generators $a,b,k,f,d$. \end{lemma} \begin{proof} The identity $x=k^{-1}fk$ gives $x^r=A^B=c^3$. Since $a=c^r$ and $h=x^{a^2}$, the last equation becomes \begin{equation}\label{eq:belimination} b=(h^2)^r=((x^r)^2)^{(a^r)^2} =(c^6)^{(c^2)^{r^2}}. \end{equation} This is a word in $c,r$ alone. We may therefore eliminate in the order \[ a=c^r,\quad b=(c^6)^{(c^2)^{r^2}},\quad k=rBr^{-1},\quad f=rBc^3B^{-1}r^{-1},\quad d=r^2c^3r^{-2}. \] Conversely these definitions give $k^{-1}fk=rc^3r^{-1}=x$, and recover $c^r=a$, $d^r=x$, $f^r=A$, $k^r=B$. Equation \eqref{eq:belimination} recovers $(h^2)^r=b$. Thus the 5 equations allow 5 Tietze eliminations, without using any commutation relations. The resulting presentation has 2 generators and $19+5-5-5=14$ relators. \end{proof} \begin{lemma}\label{lem:lastdeletion} After these eliminations, $[a,b]=1$ follows from $[c,a]=1$. \end{lemma} \begin{proof} Write $c_i=c^{r^i}$. The retained relation and its $r$-conjugate give $[c_0,c_1]=[c_1,c_2]=1$. Hence $a=c_1$ commutes with $b=c_2^{-2}c_0^6c_2^2$. \end{proof} The use of $[a,b]$ in \cref{lem:fivedeletions} is noncircular: it was retained then, and its independent derivation uses definitions obtained without it. Deleting it now preserves the group and leaves 13 relators. \subsection{The final presentation} \label{sec:final} The only presentation generators are $c,r$. Define the following words in order: \begin{equation}\label{eq:finaldefinitions1} \begin{aligned} a&=r^{-1}cr,&J&=r^{-2}c^2r^2,&b&=J^{-1}c^6J,\\ B&=cbc^{-1},&k&=rBr^{-1},&f&=rBc^3B^{-1}r^{-1},\\ x&=rc^3r^{-1},&d&=r^2c^3r^{-2}. \end{aligned} \end{equation} Then set \begin{equation}\label{eq:finaldefinitions2} \begin{aligned} x_1&=a^{-1}xa,&h&=a^{-2}xa^2,&s_1&=fx_1f^{-1},\\ s_2&=fh^{-1}x_1^{-1}hf^{-1},&e&=fh^{-1}dhf^{-1},&t&=fh^{-1}fh,\\ \ell&=bcb^{-1},&u_1&=b^2cb^{-2},&u_2&=b^{-1}cb. \end{aligned} \end{equation} Evaluate the coding words of \cref{thm:coding} at $s_1,s_2$ and put $T=Pt f^{-1}P^{-1}f$. The 13 equations are \begin{center} \renewcommand{\arraystretch}{1.25} \begin{tabular}{cl} \toprule Number & Defining equation\\ \midrule 1 & $d^4s_1=s_1d$\\ 2 & $es_1=s_1e^4$\\ 3--5 & $d^{-i}cd^iE_i=F_i e^i c e^{-i}\quad(i=1,2,3)$\\ 6 & $[T,k]=1$\\ 7--8 & $\bar g_i\ell=\ell\bar g_i f u_i f^{-1}\quad(i=1,2)$\\ 9--10 & $[\ell,k^{-1}\bar g_i k]=1\quad(i=1,2)$\\ 11 & $Pt=a^{-3}xa^3$\\ 12 & $[c,a]=1$\\ 13 & $[b,x]=1$\\ \bottomrule \end{tabular} \end{center} The complete count is recorded below; word abbreviations are never counted as generators. \begin{center} \begin{tabular}{lrr} \toprule Stage & Generators & Relators\\ \midrule Simulator & 8 & 16\\ Input attached; input relators removed & 11 & 32\\ Positive symmetry and eliminations & 9 & 29\\ Restore the redundant grid entry & 9 & 30\\ Column compression & 8 & 23\\ Row compression & 6 & 19\\ Add the final HNN extension & 7 & 24\\ Recover and delete 5 old relations & 7 & 19\\ Eliminate 5 generator/definition pairs & 2 & 14\\ Delete $[a,b]$ & 2 & 13\\ \bottomrule \end{tabular} \end{center} \begin{proof}[Proof of \cref{thm:main}] Choose a universal finitely presented group $K_*$ using Higman's embedding theorem \cite{Higman1961}. Applying the construction with $K=K_*$ gives a group $U_{K_*}$ and embeddings \[ K_*\hookrightarrow G\hookrightarrow M\hookrightarrow N \hookrightarrow B_{19}^{+}\hookrightarrow U_{K_*}. \] The Tietze transformations above give the displayed 2-generator, 13-relator presentation of $U_{K_*}$. Explicitly, the generator $k_i$ of $K_*$ is sent to $W_i(u_1,u_2)^{-1}$, followed by the ordered substitutions \eqref{eq:finaldefinitions1}--\eqref{eq:finaldefinitions2}. Since $U_{K_*}$ contains the universal group $K_*$, it is universal. \end{proof} The input relations enter the coding words, but are recovered and deleted in \cref{lem:deleteinput}. They affect the lengths of the final words, without adding any equations to the 13-relator table. \begin{thebibliography}{99} \bibitem{BCM1971} W.~W. Boone, D.~J. Collins, and Yu.~V. Matijasevi\v{c}, \emph{Embeddings into semigroups with only a few defining relations}, in J.~E. Fenstad (ed.), Proceedings of the Second Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics \textbf{63}, North-Holland, 1971, pp.~27--40. \href{https://doi.org/10.1016/S0049-237X(08)70841-3}{doi:10.1016/S0049-237X(08)70841-3}. \bibitem{BooneCollins1974} W.~W. Boone and D.~J. Collins, \emph{Embeddings into groups with only a few defining relations}, J. Austral. Math. Soc. \textbf{18} (1974), 1--7. \href{https://doi.org/10.1017/S1446788700019066}{doi:10.1017/S1446788700019066}. \bibitem{Borisov1969} V.~V. Borisov, \emph{Simple examples of groups with unsolvable word problem}, Mat. Zametki \textbf{6} (1969), 521--532; English translation, Math. Notes \textbf{6} (1969), 768--775. \href{https://doi.org/10.1007/BF01101402}{doi:10.1007/BF01101402}. \bibitem{HNN1949} G. Higman, B.~H. Neumann, and H. Neumann, \emph{Embedding theorems for groups}, J. London Math. Soc. \textbf{24} (1949), 247--254. \href{https://doi.org/10.1112/jlms/s1-24.4.247}{doi:10.1112/jlms/s1-24.4.247}. \bibitem{Higman1961} G. Higman, \emph{Subgroups of finitely presented groups}, Proc. Roy. Soc. London Ser. A \textbf{262} (1961), 455--475. \href{https://doi.org/10.1098/rspa.1961.0132}{doi:10.1098/rspa.1961.0132}. \bibitem{KegelLiRen2026} M. Kegel, S.~Y. Li, and Q. Ren, \emph{Small undecidable groups and unrecognizable $4$-manifolds}, arXiv:2609.10461v1 [math.GR], 2026. \href{https://arxiv.org/abs/2609.10461v1}{arXiv:2609.10461v1}. \bibitem{LyndonSchupp} R.~C. Lyndon and P.~E. Schupp, \emph{Combinatorial Group Theory}, Ergebnisse der Mathematik und ihrer Grenzgebiete \textbf{89}, Springer-Verlag, Berlin--New York, 1977. \bibitem{MartinSteenbock} A. Martin and M. Steenbock, \emph{A combination theorem for cubulation in small cancellation theory over free products}, Ann. Inst. Fourier (Grenoble) \textbf{67} (2017), 1613--1670. \href{https://doi.org/10.5802/aif.3118}{doi:10.5802/aif.3118}. \bibitem{Matiyasevich1995} Yu. Matiyasevich, \emph{Word problem for Thue systems with a few relations}, in H. Comon and J.-P. Jouannaud (eds.), Term Rewriting, Lecture Notes in Computer Science \textbf{909}, Springer, 1995, pp.~39--53. \href{https://doi.org/10.1007/3-540-59340-3_4}{doi:10.1007/3-540-59340-3\_4}. \bibitem{PoorRinot} M. Po\'or and A. Rinot, \emph{A Shelah group in ZFC}, Forum Math. Pi \textbf{13} (2025), e13. \href{https://doi.org/10.1017/fmp.2025.5}{doi:10.1017/fmp.2025.5}. \bibitem{UniversalGroupLean} Q. Ren, \emph{Universal-Group}, Lean 4 formalization, \href{https://github.com/32805433/Universal-Group}{GitHub repository}, 2026, commit \href{https://github.com/32805433/Universal-Group/tree/a6913011408330cc2039d3a9b95daf14f676f405}{\texttt{a691301}}. \bibitem{Valiev1977} M.~K. Valiev, \emph{Universal group with twenty-one defining relations}, Discrete Math. \textbf{17} (1977), 207--213. \href{https://doi.org/10.1016/0012-365X(77)90153-4}{doi:10.1016/0012-365X(77)90153-4}. \end{thebibliography} \end{document}