\documentclass[12pt,oneside,leqno]{amsart}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage[hidelinks]{hyperref}
\usepackage{tikz}
\usetikzlibrary{cd}
\usepackage{mathrsfs}

\newenvironment{nouppercase}{%
  \let\uppercase\relax%
  \renewcommand{\uppercasenonmath}[1]{}}{}

\usepackage{comment}

\makeatletter
\renewcommand{\eqref}[1]{\textup{(\ignorespaces\ref{#1}\unskip\@@italiccorr)}}
\def\maketag@@@#1{\hbox{\m@th\normalfont\bfseries#1}}
\makeatother

% THEOREMS -------------------------------------------------------

\numberwithin{equation}{section}
\numberwithin{figure}{section}

\theoremstyle{plain}
\newtheorem{thm}[equation]{Theorem}
\newtheorem{lemma}[equation]{Lemma}
\newtheorem{cor}[equation]{Corollary}
\newtheorem{prop}[equation]{Proposition}
\newtheorem{example}[equation]{Example}

\theoremstyle{definition}
\newtheorem{definition}[equation]{Definition}
\newtheorem{question}[equation]{Question}
\newtheorem{remark}[equation]{Remark}



% MATH -----------------------------------------------------------
\newcommand{\Q}{\ensuremath \mathbb{Q}}
\newcommand{\R}{\ensuremath \mathbb{R}}
\newcommand{\C}{\ensuremath \mathbb{C}}
\newcommand{\Z}{\ensuremath \mathbb{Z}}
\newcommand{\N}{\ensuremath \mathbb{N}}
\newcommand{\M}{\ensuremath \mathbb{M}}
\newcommand{\F}{\ensuremath \mathbb{F}}

\newcommand\subsetsim{\mathrel{\substack{
  \textstyle\subset\\[-0.2ex]\textstyle\sim}}}

\begin{document}

\section{Equation 1518}

Our carrier set will be the (nonabelian) free group $G$ on countably many letters $x_1,x_2,\ldots$. The functional equation for 1518 is
\[
f(f(f(h)h^{-1})hf(1)^{-1})=hf(1)^{-1}.
\]
Think of this as saying that once $(1,x_1),(a,b),(ba^{-1},c)\in f$, then $(cax_1^{-1},ax_1^{-1})\in f$.  A special family built from this rule is
\[
E_0  =  \{(1,x_1),(x_1,x_2),(x_2x_1^{-1},x_1^{-1}),(x_1^{-1},1),(x_2x_1^{-2},x_1^{-2}),(x_1^2,x_3),(x_3x_1^{-2},x_1^{-1})\}.
\]

Let $\mathscr{E}$ be the collection of subsets $E\subseteq G^2$ subject to the following conditions:
\begin{itemize}
\item[(1)] $E$ is finite.
\item[(2)] $E$ is a function.
\item[(3)] $E_0\subseteq E$.
\item[(4)] If $(a,b),(ba^{-1},c)\in E$, then $(cax_1^{-1},ax_1^{-1})\in E$.
\item[(5)] If $(a,b)\in E$ and $b=x_1$, then $ba^{-1}\in {\rm dom}(E)$.
\end{itemize}

\begin{lemma}
For any $E\in \mathscr{E}$ and any $a\in G$, there is an extension $E\subseteq E'\in \mathscr{E}$ where the functional equation holds for $a$.
\end{lemma}
\begin{proof}
{\bf Case 1}: Assume $(a,b)\in E$ for some $b\in G$.

If $ba^{-1}\in {\rm dom}(E)$, then we are done by property (4).  So we may reduce to the case when $ba^{-1}\notin {\rm dom}(E)$.

Let $(a_1,b_1),\ldots, (a_n,b_n)$ be the set of pairs in $E$ such that $b_ia_i^{-1}=ba^{-1}$.  Since $ba^{-1}\notin {\rm dom}(E)$, we know that $a_i\neq x_1^2$ from our choice of $E_0$.  Also, we know that $b_i\neq x_1$ by condition (5).

Let $c$ be a generator of $G$ that does not appear in the normal form of any coordinate in $E$ and take
\[
E'=E\cup\{(ba^{-1},c)\}\cup\{(ca_ix_1^{-1},a_ix_1^{-1})\}_{i\in [1,n]}.
\]
Conditions (1), (2), and (3) are clear for $E'$. Condition (5) for $E'$ follows from condition (5) for $E$ and the fact that $a_ix_1^{-1}\neq x_1$ since $a_i\neq x_1^2$.  Condition (4) is a quick case analysis, mostly using the newness of the generator $c$; but note that if $c(ba^{-1})^{-1}=ca_ix_1^{-1}$, then $b_i=x_1$, which we already stated is impossible.

{\bf Case 2}: Assume $a\notin {\rm dom}(E)$.  If $(x,y)\in E$ with $yx^{-1}=a$, then applying Case 1 to $x$, we get $a\in {\rm dom}(E)$, and then reduce to Case 1.  Thus, we may assume there is not such pair.  Then letting $b$ be any generator of $G$ not in the normal form of any element in $E$ or of $a$, take $E':=E\cup\{(a,b)\}$, and again reduce to Case 1.
\end{proof}

The functional equation for 47 is
\[
f^3(1)=1.
\]
Taking $E_0\cup\{x_2,x_4)\}$ as the initial seed works.

Equation 614's functional equation is
\[
f^2(f(x_1^{-1})x_1)=1.
\]
Again taking $E_0\cup\{(x_2,x_4)\}$ works.

The functional equation for 817 is
\[
f(x_1^2)=1.
\]
Using $E_0\cup\{(x_3,x_4)\}$ works.

The functional equation for 3862 is
\[
x_1=f(f(x_1)^{-1})f(x_1).
\]
Taking $E_0\cup\{(x_2^{-1},x_4),(x_4x_2x_1^{-2},x_2x_1^{-2}),(x_4x_2x_1^{-3},x_2x_1^{-3})\}$ works.

\end{document} 