\section{Cofinality}
Our main result hinges on a specific property of countable, confluent systems: the \emph{cofinality property}. We will discuss the notion of cofinality and the theorems related to it below.

\begin{definition}[Cofinality]<Thesis.cofinal>
  Let \arsdef{A}{A}{} be an ARS. Let $B \subseteq A$.
  \begin{defnumerate}
    \item $B$ is \emph{cofinal} in $\AA$ if every $a \in A$ reduces to an element in $B$: $\forall a \in A, \exists b \in B, a \toto b$.

    % \begin{noindent}
\begin{leancode}
def cofinal (s: Set α) :=
  ∀a, ∃b ∈ s, r∗ a b
\end{leancode}
% \end{noindent}

    \item A reduction sequence $a_0 \to a_1 \to \cdots$ is cofinal in $\AA$ if the set of elements in the sequence is cofinal in $\AA$.
    % \begin{noindent}
\begin{leancode}
def cofinal_reduction {N: ℕ∞} {f: ℕ → α} (hseq: reduction_seq r N f) :=
  cofinal r hseq.elems
\end{leancode}
% \end{noindent}

    \item $\AA$ has the \emph{cofinality property} (\CP) if for every $a \in A$, there exists a corresponding reduction sequence $a = a_0 \to a_1 \to \cdots$ which is cofinal in $\mathcal{G}(a)$, the reduction graph of $a$.
    % \begin{noindent}
\begin{leancode}
def cofinality_property :=
  ∀a, ∃N f, ∃(hseq: reduction_seq (A.reduction_graph a).ars.union_rel N f),
    cofinal_reduction hseq ∧ hseq.start = a
\end{leancode}
% \end{noindent}

    \item $\AA$ has the \emph{componentwise cofinality property} (\CPC) if for every $a \in A$, there exists a corresponding reduction sequence $a = a_0 \to a_1 \to \cdots$ which is cofinal in $\mathcal{C}(a)$, the \emph{component} of $a$.
    % \begin{noindent}
\begin{leancode}
def cofinality_property_conv :=
  ∀a, ∃N f, ∃(hseq: reduction_seq (A.component a).ars.union_rel N f),
    cofinal_reduction hseq ∧ hseq.start = a
\end{leancode}
% \end{noindent}
  \end{defnumerate}
\end{definition}

Note that the cofinality property is one of the few properties we define for an ARS instead of a `raw' reduction relation -- this is necessary because it uses the notion of a sub-ARS that we defined in \cref{sec:subars}.

\subsection{Cofinality and confluence}
Cofinality seems like a strange property, but it turns out to have an interesting connection to confluence. It follows almost directly from the definition that an ARS which has the cofinality property must be confluent.
%
\newpage

\begin{lemma}<Thesis.cr_of_cp>\label{thm:cr_of_cp}
  An ARS \arsdef{A}{A}{} which has the cofinality property must be confluent.
  % \begin{noindent}
\begin{leancode}
lemma cr_of_cp:
  cofinality_property A → confluent A.union_rel := ...
\end{leancode}
% \end{noindent}
\end{lemma}

\begin{proof}
  Let $a, b, c \in A$, and $c \otot a \toto b$. By the cofinality property, there is some reduction sequence $s_0 \to s_1 \to \ldots$ which is cofinal in the reduction graph of $a$.

  Since $b$ and $c$ are in the reduction graph of $a$, they reduce to elements $s_b, s_c$ in the cofinal reduction sequence. Without loss of generality, we take $s_b \toto s_c$. Then, our common reduct is $s_c$: we have $a \toto b \toto s_b \toto s_c$ and $a \toto c \toto s_c$.
\end{proof}
%
Surprisingly, the converse holds as well, as long as our ARS is countable -- that is, there is an injective map $A \to \NN$, or equivalently a surjective map $\NN \to A$. In Lean, we model this by saying our type \lean{α} satisfies \leandoc{Countable}.

\begin{lemma}[{\cite[p.\:51]{klop1980}}]<Thesis.cp_of_countable_cr>\label{thm:cp_of_cr_countable}
  Any countable, confluent ARS has the cofinality property.

  % \begin{noindent}
\begin{leancode}
lemma cp_of_countable_cr [cnt: Countable α] (cr: confluent A.union_rel):
    cofinality_property A := ...    
\end{leancode}
% \end{noindent}
\end{lemma}

We have formalized the proof that is given in \cite[p.\:51]{klop1980}.

\begin{proof}
  Let \arsdef{A}{A}{} be an ARS. Assume $\AA$ is confluent. Assume $A$ is countable.

  Fix $a \in A$. We must show that there exists a reduction sequence $a = b_0 \to b_1 \to \cdots$ which is cofinal in $\GG(a)$.

  $\GG(a)$ contains $a$, so it is nonempty. Since $A$ is countable, there exists a function $f \colon \NN \to \GG(a)$ which is surjective. Consider $f$ as a sequence. Every element in the sequence is a reduct of $a$, but they are not necessarily reducts of one another. However, we can use $f$ to build a new sequence $g$:
  \begin{align*}
    g(0)     & = a,                                                   \\
    g(n + 1) & = \text{the common reduct of } g(n) \text{ and } f(n).
  \end{align*}

  Every element in the codomain of both $f$ and $g$ is a reduct of $a$. Hence, a common reduct of $f(i)$ and $g(j)$ always exists, by confluence of $\AA$.

  Note that $g(n)$ forms a reduction sequence w.r.t. $\toto$. That is,
  \[ g(0) \toto g(1) \toto g(2) \toto \cdots \]

  We can expand this reduction sequence into a reduction sequence w.r.t. $\to$,
  \[ g(0) \to \cdots \to g(1) \to \cdots \to g(2) \to \cdots \]

  We wish to show that this sequence is cofinal in $\GG(a)$. Assume $b \in \GG(a)$. Since $f$ is surjective, there must be an $i$ s.t. $f(i) = b$. Then $g(i + 1)$ is a reduct of $b$.
\end{proof}

\subsubsection{Expansion of reduction sequences}
The proof sketch above is relatively easy to formalize, save for one noteworthy detail: the step where $g$ is expanded into a reduction sequence w.r.t. $\to$. This step is only mentioned very briefly in the original proof in \cite{klop1980}, perhaps because \citeauthor{klop1980} considered it obvious that such an expansion is possible.

For finite reduction sequences, we can easily prove this; our inductive definition is again well-suited to such a proof (\leandoc*{Thesis.ReductionSeq.flatten}{ReductionSeq.flatten}). It is easy to convince oneself that this also extends to the infinite case, but formalizing this turns out to be quite involved. We will look at the core parts of our Lean formalization, including some key definitions. The formalization of this expansion is due in part to Edward van de Meent and Daniel Weber on the Lean Zulip \cite{vankampen2024}.

Our eventual goal is to prove that any reflexive-transitive reduction sequence $a_0 \toto a_1 \toto a_2 \toto \cdots$ can be expanded to a reduction sequence $a_0 \to \cdots \to a_1 \to \cdots \to a_2 \to \cdots$. We will begin by proving a similar property for \emph{transitive} reduction sequences, which is simpler because we have the guarantee that there are no `empty' steps.

\begin{lemma}<Thesis.InfReductionSeq.trans_chain>\label{thm:expandstep}
  Any transitive step $a \to^+ b$ can be expanded into a list of elements $[a, \ldots, b]$ such that for any two adjacent elements $x, y$, we have $x \to y$.

  % \begin{noindent}
\begin{leancode}
lemma trans_chain {a b}:
    r⁺ a b → ∃l, l.getLast? = some b ∧ List.Chain r a l := ...
\end{leancode}
% \end{noindent}
\end{lemma}

\begin{proof}
  By structural induction on the transitive step.
\end{proof}

Our formalized lemma makes use of \leandoc{List.Chain}: a list \lean{a::l} satisfying \lean{List.Chain r a l} starts with a, and links each subsequent element via \lean{r}.

In order to prove various other properties of these lists, we wish to have a function \lean{trans_chain' {a b}: r⁺ a b → List α} which satisfies \lean{(trans_chain' hstep).getLast? = some b} and \lean{List.Chain r a (trans_chain' hstep)}, i.e. the property given by \lean{trans_chain}. Unfortunately, we cannot compute such a list, but since we know one must exist, we can still define such a function as long as we mark it \lean{noncomputable}. To do so, we use the function \leandoc{Classical.choose}, which is derived from the type-theoretic axiom of choice.

\begin{definition}<Thesis.InfReductionSeq.trans_chain'>
  If we have a reduction step $h: a \to^+ b$, \lean{Classical.choose (trans_chain h)} is a list of elements $[\ldots, b]$ such that for any two adjacent elements $x, y$, we have $x \to y$.

  % \begin{noindent}
\begin{leancode}
noncomputable def trans_chain' {a b}: r⁺ a b → List α :=
  fun h ↦ Classical.choose (trans_chain h)
\end{leancode}
% \end{noindent}
\end{definition}

Note that \lean{trans_chain'} returns the list without the element $a$; this is convenient because we will want to concatenate multiple lists corresponding to a sequence $a \to^+ b \to^+ c \to^+ \ldots$, and the last element of the first step coincides with the first element of the second step, et cetera. In order to not contain these boundary elements twice, we always omit the first element of a step, and we prepend $a$ later in the process.

The proof that \lean{trans_chain'} satisfies the property of \lean{l} in \lean{trans_chain} is given by \leandoc{Classical.choose_spec}, which has the type \lean{(h: ∃x, p x) → p (Classical.choose h)}. Using this definition, we can for instance prove that such a list is always nonempty:

% \begin{noindent}
\begin{leancode}
lemma trans_chain'.nonempty {a b} (h: r⁺ a b):
    trans_chain' h ≠ [] := ...
\end{leancode}
% \end{noindent}

We can also use \lean{trans_chain'} to define a sequence of lists satisfying the chain property.

\begin{definition}<Thesis.InfReductionSeq.inf_trans_lists>
  A transitive reduction sequence $a_0 \to^+ a_1 \to^+ \cdots$ can be transformed into a sequence of lists $[[\ldots, a_1], [\ldots, a_2], \ldots]$, by applying \lean{trans_chain'} to each step.

  % \begin{noindent}
\begin{leancode}
lemma reduction_seq.inf_step (hseq: reduction_seq r ⊤ f) (n: ℕ):
    r (f n) (f (n + 1)) := ...

noncomputable def inf_trans_lists (f: ℕ → α) (hf: reduction_seq r⁺ ⊤ f): ℕ → List α
| n => trans_chain' (hf.inf_step n)
\end{leancode}
% \end{noindent}
\end{definition}

We now define an auxiliary function \lean{aux}, which allows us to get an element from such a sequence of lists using a pair of indices \lean{(list_idx, elem_idx)}.

\begin{definition}<Thesis.InfReductionSeq.aux>
  The auxiliary function \lean{aux} takes a sequence of lists, a proof that all lists are nonempty, a list index $n$ and an element index $m$, and returns the $m$th element, starting at the $n$th list.

  % \begin{noindent}
\begin{leancode}
variable (l_seq: ℕ → List α) (hne: ∀n, (l_seq n) ≠ [])

noncomputable def aux (list_idx: ℕ) (elem_idx: ℕ) : α :=
  if h: elem_idx < (l_seq list_idx).length then
    (l_seq list_idx)[elem_idx]
  else
    have: elem_idx - (l_seq list_idx).length < elem_idx := by
      have := List.length_pos.mpr (hne list_idx)
      omega
    aux (list_idx + 1) (elem_idx - (l_seq list_idx).length)
\end{leancode}
% \end{noindent}

\end{definition}

Note that \lean{elem_idx} may be larger than the list referred to by \lean{list_idx}; in that case, the index `rolls over' to the next list. This function is defined recursively; to prove that the function is terminating, we use the fact that each list in the sequence is nonempty (\lean{hne}), and therefore \lean{elem_idx} is decreasing. This is one reason we limit ourselves to transitive reduction sequences here -- an equivalent definition for reflexive-transitive reduction sequences may have a potentially infinite amount of empty lists, making \lean{aux} non-terminating.

If \lean{hf: reduction_seq r⁺ ⊤ f}, then our desired expanded sequence is $f(0)$ followed by \lean{aux (inf_trans_lists f hf) (inf_trans_lists.nonempty) 0 n}. We show this as follows.

\begin{lemma}<Thesis.InfReductionSeq.aux_skip>\label{thm:aux_skip}
  The $k$th element starting from list $m + 1$ is reachable starting from list $m$ by adding some $n$ to $k$ (namely, the length of list $m$).

  % \begin{noindent}
\begin{leancode}
lemma aux_skip (m k: ℕ):
    ∃n, aux l_seq hne m (k + n) = aux l_seq hne (m + 1) k := ...
\end{leancode}
% \end{noindent}
\end{lemma}

\begin{proof}
  By definition of \lean{aux}.
\end{proof}

\begin{lemma}<Thesis.InfReductionSeq.aux_skip_i>\label{thm:aux_skip_i}
  We can get the $k$th element of list $m + i$ by getting the $k + n$th element of list $m$, where $n$ is the length of the intermediate lists.

  % \begin{noindent}
\begin{leancode}
lemma aux_skip_i (i m k: ℕ):
    ∃n, aux l_seq hne m (k + n) = aux l_seq hne (m + i) k := ...
\end{leancode}
% \end{noindent}
\end{lemma}

\begin{proof}
  By induction on $i$, along with \cref{thm:aux_skip}.
\end{proof}

\begin{lemma}<Thesis.InfReductionSeq.aux_elem'>\label{thm:aux_elem_prime}
  Let \lean{f: ℕ → α} and \lean{hf: reduction_seq r⁺ ⊤ f} be an infinite transitive reduction sequence. Each element \lean{f n} for $n > 0$ appears as an element in the sequence generated by \lean{aux} using \lean{inf_trans_lists}, starting at the $(n - 1)$th list.

  % \begin{noindent}
\begin{leancode}
lemma aux_elem' (f: ℕ → α) (hf: reduction_seq r⁺ ⊤ f) (n) (hn: n > 0):
    let ls := inf_trans_lists f hf
    f n = aux ls inf_trans_lists.nonempty (n - 1) ((ls (n - 1)).length - 1) := ...
\end{leancode}
% \end{noindent}
\end{lemma}

\begin{proof}
  By definition of \lean{inf_trans_lists} and \lean{trans_chain'}, the $(n - 1)$th list is the list containing the elements $[\ldots, a_n]$. $a_n$ is the last element of this list.
\end{proof}

\begin{lemma}<Thesis.InfReductionSeq.aux_elem>\label{thm:aux_elem}
  Let \lean{f: ℕ → α} and \lean{hf: reduction_seq r⁺ ⊤ f} be an infinite transitive reduction sequence. Each element \lean{f n} for $n > 0$ appears in the sequence generated by \lean{aux} using \lean{inf_trans_lists}, starting at the first list.

  % \begin{noindent}
\begin{leancode}
lemma aux_elem (f: ℕ → α) (hf: reduction_seq r⁺ ⊤ f) (n: ℕ) (hn: n > 0):
    ∃n', f n = aux (inf_trans_lists f hf) inf_trans_lists.nonempty 0 n' := ...
\end{leancode}
% \end{noindent}
\end{lemma}

\begin{proof}
  By \cref{thm:aux_skip_i,thm:aux_elem_prime}.
\end{proof}

\newpage
\begin{lemma}<Thesis.InfReductionSeq.aux_inf_reduction_seq>\label{thm:aux_reduction_seq}
  Let \lean{f: ℕ → α} and \lean{hf: reduction_seq r⁺ ⊤ f} be an infinite transitive reduction sequence. For all list indices \lean{list_idx}, \lean{aux (inf_trans_lists f hf) inf_trans_lists.nonempty list_idx} is an infinite reduction sequence with respect to \lean{r}.

  % \begin{noindent}
\begin{leancode}
lemma aux_inf_reduction_seq (f hf) (list_idx: ℕ):
    reduction_seq r ⊤ (aux (inf_trans_lists f hf) (inf_trans_lists.nonempty) list_idx)
  := ...
\end{leancode}
% \end{noindent}
\end{lemma}

\begin{proof}
  Fix $i$ and $j$. We wish to show \lean{r (aux _ _ i j) (aux _ _ i (j + 1))}.

  We proceed by \emph{functional induction} on \lean{i} and \lean{j} using \lean{aux}'s induction principle. This induction principle is automatically generated by Lean; essentially, it works by following the structure of a recursive function, which forms a valid induction principle because it is terminating. We get the following cases:

  \vspace{0.5em}
  \noindent\emph{Case 1: \lean{j < (inf_trans_lists f hf i).length}}:

  Let's say $l_i$ is the $i$th list generated by \lean{inf_trans_lists f hf}, and $l_{i + 1}$ the $(i + 1)$th. Since $j$ is smaller than the length of the $i$th list, \lean{aux _ _ i j} reduces to $l_i[j]$. Now, we distinguish the case where $j + 1$ is smaller than the length of $l_i$ from the case where $j + 1$ is greater than the length of $l_i$.

  If $j + 1$ is smaller than the length of $l_i$, then \lean{aux _ _ i (j + 1)} reduces to $l_i[j + 1]$. By definition of \lean{inf_trans_lists}, adjacent elements within $l_i$ are linked by $\to$, so we have $l_i[j] \to l_i[j + 1]$, as required.

  If $j + 1$ is larger than the length of $l_i$, then $l_i[j]$ must be the last element of $l_i$. Then \lean{aux _ _ i (j + 1)} reduces to $l_{i + 1}[0]$. By definition of $l_i$, we have $l_i[j] = f(i + 1)$, and by definition of $l_{i + 1}$, we have \lean{List.Chain (f (i + 1)) (inf_trans_lists f hf (i + 1))}. Then we have $l_i[j] \to l_{i + 1}[0]$, as required.

  \vspace{0.5em}
  \noindent\emph{Case 2: \lean{j ≥ (inf_trans_lists f hf i).length}}:

  In this case, we get an induction hypothesis \lean{ih}:
  %
  % \begin{noindent}
\begin{leancode}
ih: r (aux _ _ (i + 1) (j - (inf_trans_lists f hf i).length))
      (aux _ _ (i + 1) (j - (inf_trans_lists f hf i).length + 1))
\end{leancode}
% \end{noindent}
  %
  Again, we wish to show that \lean{r (aux _ _ i j) (aux _ _ i (j + 1))}. Since $j$ is greater than the length of $l_i$, we know \lean{aux _ _ i j = aux _ _ (i + 1) (j - (inf_trans_lists f hf i).length)}. If $j$ is greater than the length of $l_i$, then so is $j + 1$, and we have \lean{aux _ _ i (j + 1) = aux _ _ (i + 1) (j - (inf_trans_lists f hf i) + 1)}. Then our goal is exactly equal to our induction hypothesis.
\end{proof}

\begin{definition}<Thesis.InfReductionSeq.seq>\label{def:seq}
  Let \lean{f: ℕ → α} and \lean{hf: reduction_seq r⁺ ⊤ f} be an infinite transitive reduction sequence. We define the expanded version of \lean{f} as follows:

  % \begin{noindent}
\begin{leancode}
noncomputable def seq: ℕ → α
| 0 => f 0
| n + 1 => aux (inf_trans_lists f hf) inf_trans_lists.nonempty 0 n
\end{leancode}
% \end{noindent}
\end{definition}

\begin{lemma}<Thesis.InfReductionSeq.seq_contains_elems>\label{thm:seq_elem}
  For any \lean{f: ℕ → α} with \lean{hf: reduction_seq r⁺ ⊤ f}, \lean{seq f hf} contains every element in \lean{f}.

  % \begin{noindent}
\begin{leancode}
lemma seq_contains_elems (f hf):
    ∀n, ∃m, f n = seq f hf m := ...
\end{leancode}
% \end{noindent}
\end{lemma}

\begin{proof}
  Fix an index $n$. If $n = 0$, we have \lean{f n = f 0 = seq f hf 0}. If $n > 0$, then by \cref{thm:aux_elem}, we have \lean{f n = aux _ _ 0 n' = seq f hf (n' + 1)} for some $n'$.
\end{proof}

\begin{lemma}<Thesis.InfReductionSeq.seq_inf_reduction_seq>\label{thm:seq_reduction_seq}
  For any \lean{f, hf}, \lean{seq f hf} forms an infinite reduction sequence with respect to \lean{r}.

  % \begin{noindent}
\begin{leancode}
lemma seq_inf_reduction_seq (f hf):
    reduction_seq r ⊤ (seq f hf) := ...
\end{leancode}
% \end{noindent}

\end{lemma}

\begin{proof}
  We only need to prove that \lean{f 0} and \lean{aux _ _ 0 0} are linked by $\to$; the rest follows from \cref{thm:aux_reduction_seq}. Note that \lean{aux _ _ 0 0 = (inf_trans_lists f hf 0)[0] = (trans_chain' (hf.inf_step 0))[0]}, where \lean{hf.inf_step 0: r⁺ (f 0) (f 1)}. By definition of \lean{trans_chain'}, we have \lean{List.Chain r (f 0) (trans_chain' (hf.inf_step 0))}, so in particular \lean{r (f 0) (trans_chain' (hf.inf_step 0))[0]}, as required.
\end{proof}

This leads us to our main expansion theorem:

\begin{theorem}<Thesis.InfReductionSeq.exists_regular_of_trans>
  Any infinite transitive reduction sequence $a_0 \to^+ a_1 \to^+ \cdots$ has an expanded counterpart $a_0 \to \cdots \to a_1 \to \cdots$ which contains all $a_n$ and starts with $a_0$.

  % \begin{noindent}
\begin{leancode}
lemma exists_regular_of_trans (f: ℕ → α) (hf: reduction_seq r⁺ ⊤ f):
    ∃f', reduction_seq r ⊤ f' ∧ (∀n, ∃m, f n = f' m) ∧ f 0 = f' 0 := ...
\end{leancode}
% \end{noindent}
\end{theorem}

\begin{proof}
  Let \lean{f' := seq f hf}. Immediate from \cref{def:seq,thm:seq_elem,thm:seq_reduction_seq}.
\end{proof}

\subsubsection{Extending the expansion to reflexive-transitive reduction sequences}
In order to extend our expansion proof to reflexive-transitive reduction sequences, we define two flavors of infinite reduction sequences:

\begin{definition}[Infinite reduction sequences]<Thesis.reduction_seq.degenerate>~ %
  \begin{defnumerate}
    \item We call an infinite reduction sequence \emph{degenerate} if, from some point onward, it only contains steps from one element to itself.

    % \begin{noindent}
\begin{leancode}
def reduction_seq.degenerate {f} (hseq: reduction_seq r ⊤ f) :=
  ∃n, ∀m ≥ n, f m = f (m + 1)
\end{leancode}
% \end{noindent}
    \item We say an infinite reflexive-transitive reduction sequence has the \emph{transitive step guarantee} if, at any point in the sequence, there is a guaranteed next transitive step.

    % \begin{noindent}
\begin{leancode}
def transitive_step_guarantee {f} (hseq: reduction_seq r ⊤ f) :=
  ∀n, ∃m ≥ n, f m ≠ f (m + 1) ∧ (∀m' ∈ Set.Icc n m, f n = f m')
\end{leancode}
% \end{noindent}
  \end{defnumerate}
\end{definition}

\begin{lemma}<Thesis.InfReductionSeq.finite_of_degenerate>\label{thm:degenerate_finite}
  If an infinite reflexive-transitive reduction sequence $(s_n)$ is degenerate, there is a finite reflexive-transitive reduction sequence $(s'_n)$ which contains all elements of $(s_n)$, and starts with $s_0$.

  % \begin{noindent}
\begin{leancode}
lemma finite_of_degenerate (f: ℕ → α) (hf: reduction_seq r∗ ⊤ f) (hdg: hf.degenerate):
    ∃N: ℕ, ∃f', reduction_seq r∗ N f' ∧ (∀n, ∃m ≤ N, f' m = f n) ∧ f' 0 = f 0 := ...
\end{leancode}
% \end{noindent}
\end{lemma}

\begin{proof}
  Let's say $(s_n)$ is degenerate, with $s_m = s_{m + 1} = s_{m + 2} = \cdots$. Then the sequence $s_0 \toto s_1 \toto \cdots \toto s_m$ contains all elements of $(s_n)$, and starts with $s_0$.
\end{proof}

Given \cref{thm:degenerate_finite}, we can expand a degenerate sequence simply by transforming it into a finite sequence and using \leandoc*{Thesis.ReductionSeq.flatten}{ReductionSeq.flatten}.

\begin{lemma}<Thesis.InfReductionSeq.tsg_of_not_degenerate>\label{thm:tsg_of_not_degenerate}
  If a reflexive-transitive reduction sequence $(s_n)$ is not degenerate, it has the transitive step guarantee.
  % \begin{noindent}
\begin{leancode}
lemma tsg_of_not_degenerate {f} (hseq: reduction_seq r∗ ⊤ f) (hndeg: ¬hseq.degenerate):
    transitive_step_guarantee hseq := ...
\end{leancode}
% \end{noindent}

\end{lemma}

\begin{proof}
  Assume $(s_n)$ is not degenerate, and let $n \in \NN$. Let $S = \{ m \mid m \ge n \land s_m \ne s_{m + 1} \}$. Since $(s_n)$ is not degenerate, $S$ is nonempty. Since $(\NN, <)$ is well-founded, there must be a minimal $m$ such that $m \ge n \land s_m \ne s_{m + 1}$, call it $m^*$.

  We must show that, for all elements $m'$ between $n$ and $m^*$, $s_n = s_m'$. We proceed by contradiction. Let $m'$ be between $n$ and $m^*$, and assume $s_n \ne s_m'$. Since $m^*$ is minimal, any $m$ such that $n \le m < m^*$ must have $s_m = s_{m + 1}$.  But then $s_n = s_{n + 1} = \ldots = s_m'$, contradicting our assumption.
\end{proof}

\begin{definition}<Thesis.InfReductionSeq.trans_idx_step>
  Let $(s_n)$ be an infinite reflexive-transitive reduction sequence which satisfies the transitive step guarantee. Then we can define a derived sequence $(s^+_n)$ as follows:

  \begin{align*}
    s^+_0       & = s_0                                                     \\
    s^+_{i + 1} & = \text{the end of the next transitive step after } s^+_i
  \end{align*}

  Essentially, we view $(s_n)$ as a sequence containing both reflexive and transitive steps, e.g.
  %
  \[ s_0 \to^+ s_1 \to^= s_2 \to^= s_3 \to^+ s_4 \to^= \cdots \]
  % 
  We wish to pick out only $s_0$ along with each end of a transitive step, in this example $s_1$ and $s_4$.

  % \begin{noindent}
\begin{leancode}
variable {f: ℕ → α} (hf: reduction_seq r∗ ⊤ f) (htsg: transitive_step_guarantee hf)

/-- From some index `n` we step to a next index `choose (htsg n) + 1`,
    which is the end of a transitive step. -/
noncomputable def trans_idx_step (n: ℕ): ℕ :=
  choose (htsg n) + 1

/-- By iterating `trans_idx_step` starting at index `0`, we can generate a sequence
    of indices into `f` which represent all transitive steps in `f`. -/
noncomputable def trans_idxs (n: ℕ): ℕ :=
  (trans_idx_step hf htsg)^[n] 0

/-- Applying `f` after `trans_idxs` yields the sequence. -/
noncomputable def trans_seq (n: ℕ): α :=
  f (trans_idxs hf htsg n)   
\end{leancode}
% \end{noindent}
\end{definition}

\begin{lemma}<Thesis.InfReductionSeq.exists_inf_regular_seq_of_not_degenerate>\label{thm:expand_nondegenerate}
  If an infinite reflexive-transitive reduction sequence $(s_n)$ is not degenerate, there exists an infinite transitive reduction sequence $(s^+_n)$ which contains all elements of $(s_n)$, and starts with $s_0$.

  % \begin{noindent}
\begin{leancode}
lemma exists_inf_regular_seq_of_not_degenerate (hnd: ¬hf.degenerate):
    ∃f', reduction_seq r ⊤ f' ∧ (∀n, ∃m, f n = f' m) ∧ f 0 = f' 0 := ...
\end{leancode}
% \end{noindent}
\end{lemma}

To keep this section somewhat brief in contrast to the previous section, we provide only a proof sketch here.

\begin{proof}[Proof sketch.]
  By \cref{thm:tsg_of_not_degenerate}, $(s_n)$ has the transitive step guarantee. Then $(s^+_n)$ is the sequence we're looking for.

  We wish to show that $(s^+_n)$ is an infinite reduction sequence with respect to $\to^+$. Hence, we wish to show that $s^+_i \to^+ s^+_{i + 1}$ for all $i$.

  If we visualize the original sequence $(s_n)$ and the derived sequence $(s^+_n)$ around $s^+_i$, it looks like this:
  %
  \[ \cdots \to^= s_{j - 1} \to^+ s_j = s^+_i \to^= \cdots \to^= s_k \to^+ s_{k + 1} = s^+_{i + 1} \to^= \cdots \]
  %
  Since all steps between $s^+_i$ and $s_k$ are reflexive, we have $s^+_i = s_k$, and thus $s^+_i \to^+ s^+_{i + 1}$, as required.

  By definition, we have $s^+_0 = s_0$. To show that every element of $(s_n)$ appears in $(s^+_n)$, we need some more complicated reasoning. Note that any element of $(s_n)$ which is between two consecutive elements $s^+_k, s^+_{k + 1}$ must equal $s^+_k$ by the reasoning above. To prove that every element appears in $(s^+_n)$, then, it suffices to show that every element $s_i$ is between two consecutive elements $s^+_k, s^+_{k+1}$.

  Note that, with every step, our index in the original sequence increases by at least one. Then the indices in our original sequence tend to infinity, and for every element $s_i$, there must be an element in $(s^+_n)$ which comes after it.

  Take the first element of $(s^+_n)$ which comes after $s_i$, call it $s^+_{k'}$. We cannot have $k' = 0$, because the first element of $(s^+_n)$ is $s_0$, which cannot come \emph{after} $s_i$. Then we must have $k' = k + 1$ for some $k$. The element $s^+_k$ must come before $s_i$, otherwise $k'$ is not minimal. Then every element $s_i$ is between two consecutive elements $s^+_k, s^+_{k + 1}$.
\end{proof}

\begin{theorem}<Thesis.InfReductionSeq.regular_seq_of_rt_seq>
  Every infinite reflexive-transitive reduction sequence $a_0 \toto a_1 \toto \cdots$ has an expanded counterpart $a_0 \to \cdots \to a_1 \to \cdots$ which contains all $a_n$ and starts with $a_0$.

  % \begin{noindent}
\begin{leancode}
lemma regular_seq_of_rt_seq (f: ℕ → α) (hf: reduction_seq r∗ ⊤ f):
    ∃N f', reduction_seq r N f' ∧ (∀n, ∃(m: ℕ) (_: m < N + 1), f n = f' m) ∧
           f 0 = f' 0 := ...
\end{leancode}
% \end{noindent}
\end{theorem}

\begin{proof}
  Immediate from \cref{thm:expand_nondegenerate,thm:degenerate_finite} and \leandoc*{Thesis.ReductionSeq.flatten}{ReductionSeq.flatten}.
\end{proof}

Although this result is barely considered in Klop's proof in \cite{klop1980}, it has taken nearly 600 lines of Lean, and six pages of text, to rigorously formalize. The entire formalization takes up around 3000 lines of Lean, so this is quite a significant part of it. In general, we have found that the core arguments of the proofs are usually easy to translate, but there is occasionally a very small step that turns out to be exceedingly difficult.

\subsection{Equivalence of componentwise definition}
It turns out the componentwise and reduction-graph versions of the cofinality property are equivalent.

\begin{lemma}<Thesis.cp_iff_cp_conv>\label{thm:cp_equiv}
  Let \arsdef{A}{A}{} be an ARS. The regular and componentwise cofinality property are equivalent.

  % \begin{noindent}
\begin{leancode}
lemma cp_iff_cp_conv:
    cofinality_property A ↔ cofinality_property_conv A := ...
\end{leancode}
% \end{noindent}

\end{lemma}

\begin{proof}
  We look at the forward and backward case separately.

  \vspace{0.5em}
  \noindent\emph{Forward case: \CP{} $\implies$ \CPC{}}
  \vspace{0.5em}

  Assume $\AA$ is \CP. Let $a \in A$, and assume $(s_n)$ is a reduction sequence which is cofinal in the reduction graph of $a$. We will show that this sequence is cofinal in the component of $a$.

  Let $b$ be an element in the component of $a$, that is, $a \equiv b$. By \cref{thm:cr_of_cp}, $\AA$ is confluent. By \cref{thm:conf_equiv}, $\AA$ is also conversion confluent. Then, by conversion confluence, $a$ and $b$ have a common reduct, $c$. $c$ is in the reduction graph of $a$, and so has a reduct in $(s_n)$. Then $b$ has a reduct in $(s_n)$, and $(s_n)$ is also cofinal in the component of $a$. Hence, $\AA$ is \CPC{}.

  \vspace{0.5em}
  \noindent\emph{Backward case: \CPC{} $\implies$ \CP{}}

  Assume $\AA$ is \CPC{}. Let $a \in A$, and assume $(s_n)$ is a reduction sequence which is cofinal in the component of $a$. Let $b$ be in the reduction graph of $a$. Then, $b$ is also in the component of $a$, as $\toto\; \subseteq\; \equiv$. Then $b$ has a reduct in $(s_n)$, and $\AA$ is \CP{}.
\end{proof}

We will use the component version of the cofinality property in our proofs of $\CP{} \implies \DCR{}$ and $\CP{} \implies \DCRtwo{}$, later.
