%\usepackage{diagxy}

\documentclass[12pt,final,notitlepage,onecolumn,german]{article}%
\usepackage[all,cmtip]{xy}
\usepackage{lscape}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{color}
\usepackage{amsmath}%
\setcounter{MaxMatrixCols}{30}
%TCIDATA{OutputFilter=latex2.dll}
%TCIDATA{Version=5.50.0.2960}
%TCIDATA{CSTFile=LaTeX article (bright).cst}
%TCIDATA{Created=Sat Mar 27 17:33:36 2004}
%TCIDATA{LastRevised=Friday, February 22, 2013 14:38:47}
%TCIDATA{<META NAME="ViewSettings" CONTENT="0">}
%TCIDATA{<META NAME="GraphicsSave" CONTENT="32">}
%TCIDATA{<META NAME="SaveForMode" CONTENT="1">}
%TCIDATA{BibliographyScheme=Manual}
%BeginMSIPreambleData
\providecommand{\U}[1]{\protect\rule{.1in}{.1in}}
%EndMSIPreambleData
\definecolor{violet}{RGB}{143,0,255}
\definecolor{forestgreen}{RGB}{34, 100, 34}
\voffset=-2.5cm
\hoffset=-2.5cm
\setlength\textheight{24cm}
\setlength\textwidth{15.5cm}
\begin{document}

\begin{center}
\textbf{Permutations, Matrices and Generalized Young Tableaux}

\textit{Donald E. Knuth}

Pacific Journal of Mathematics, vol. 34, no. 3, 1970

\textbf{Errata and comments by Darij Grinberg - I}

\bigskip
\end{center}

Different comments are separated by horizontal lines, like this:

\rule{17cm}{0.3mm}

\textbf{Page 709:} On the third line of page 709 (the title, author and
abstract are not counted as lines), replace $p_{1}+p_{2}+\cdots p_{m}$ by
$p_{1}+p_{2}+\cdots+p_{m}$.

\rule{17cm}{0.3mm}

\textbf{Page 711:} On the first line after the formula (2.1), replace "if
$i>m$ or $j<p_{i}$" by "if $i>m$ or $j>p_{i}$".

\rule{17cm}{0.3mm}

\textbf{Page 712:} After presenting the algorithm $\operatorname*{INSERT}%
\left(  x\right)  $, Knuth writes that: "The parenthesized assertions in steps
I3 and I4 serve to verify that $Y$ remains a generalized Young tableau
throughout the algorithm." This is a little bit inaccurate, because in order
to verify that $Y$ remains a generalized Young tableau\footnote{Here and in
the following, a \textit{generalized Young tableau} means a family $\left(
z_{i,j}\right)  _{\left(  i,j\right)  \in\mathbb{N}^{2}}$ of elements of
$\mathbb{N}\cup\left\{  \infty\right\}  $ with the following
properties:\newline- We have $z_{i,j}=0$ whenever $i$ or $j$ is zero.\newline-
We have $z_{i,j}\leq z_{i,\left(  j+1\right)  }$ and $z_{i,j}<z_{\left(
i+1\right)  ,j}$ for all $\left(  i,j\right)  \in\mathbb{N}^{2}$.\newline-
Only finitely many pairs $\left(  i,j\right)  \in\mathbb{N}^{2}$ satisfy
$z_{i,j}\neq\infty$.} throughout the algorithm, it is not enough to check that
the inequalities (2.3) remain valid (this is indeed a consequence of the
parenthesized assertions in steps I3 and I4), but we must also check that the
leftmost column and the uppermost row of $Y$ remain filled with zeroes.
Fortunately, checking this is very easy: just add the assertions "$i\geq1$"
and "$j\geq1$" into the parentheses in each of steps I2, I3 and I4. Indeed,
these assertions are clearly true after step I1\ \ \ \ \footnote{In fact,
after step I1, we have $i\geq1$ (because $i$ was set to be $1$ in step I1) and
$j\geq1$ (since $y_{1j}=\infty\neq0=y_{10}$, so that $j\neq0$, thus $j\geq
1$).}, and are left invariant by each of the steps I2, I3 and
I4\ \ \ \ \footnote{\textit{Proof.} Step I2 clearly leaves the assertion
$i\geq1$ invariant (since $i$ is not changed in Step I2), and also leaves the
assertion $j\geq1$ invariant (because after Step I2, we have $x_{i}<y_{ij}$
and therefore $y_{i0}=0\leq x_{i}<y_{ij}$, so that $y_{ij}\neq y_{i0}$, so
that $j\neq0$, so that $j\geq1$).
\par
Step I3 clearly leaves both assertions $i\geq1$ and $j\geq1$ invariant (since
neither $i$ nor $j$ is changed in Step I3).
\par
Step I4 also leaves both assertions $i\geq1$ and $j\geq1$ invariant (since
Step I4 leaves $j$ unchanged and either increases $i$ or leaves $i$
unchanged).}, so that nothing goes wrong if we add these two assertions into
the parentheses in each of steps I2, I3 and I4. Adding these two assertions
into the parentheses in each of steps I2, I3 and I4, we see that the algorithm
changes the value of $y_{ij}$ only for certain pairs $\left(  i,j\right)  $
satisfying $i\geq1$ and $j\geq1$; in particular, the leftmost column and the
uppermost row of $Y$ are never changed, so they remain filled with zeroes
throughout the algorithm (because they were filled with zeroes initially).

\rule{17cm}{0.3mm}

\textbf{Page 713:} It might be reasonable to stress that the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ is only defined for generalized
Young tableaux $Y$ and pairs $\left(  s,t\right)  $ satisfying the relations
$s\geq1$, $t\geq1$, $y_{s,t}\neq\infty$ and $y_{s,\left(  t+1\right)
}=y_{\left(  s+1\right)  ,t}=\infty$.

\rule{17cm}{0.3mm}

\textbf{Page 713:} What I wrote above about the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ also pertains to the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $: In order to prove that "$Y$
remains a generalized Young tableau" throughout the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $, we must not only check that the
inequalities (2.3) remain valid (this is indeed a consequence of the
parenthesized assertions in steps D3 and D4), but we must also check that the
leftmost column and the uppermost row of $Y$ remain filled with zeroes.
Fortunately, checking this is very easy: just add the assertions "$i\geq1$"
and "$j\geq1$" into the parentheses in each of steps D2, D3 and D4. Indeed,
these assertions are clearly true after step D1\ \ \ \ \footnote{In fact,
after step D1, we have $i\geq1$ (because $i$ was set to be $t$ in step D1, and
because $t\geq1$) and $j\geq1$ (since $j$ was set to be $s$ in step D1, and
because $s\geq1$).}, and are left invariant by each of the steps D2, D3 and
D4\ \ \ \ \footnote{\textit{Proof.} Step D2 clearly leaves the assertion
$i\geq1$ invariant (since $i$ is either left unchanged or increased by Step
D2), and leaves the assertion $j\geq1$ invariant (since $j$ isn't changed by
Step D2).
\par
Step D3 obviously leaves both assertions $i\geq1$ and $j\geq1$ invariant
(since neither $i$ nor $j$ is changed in Step D3).
\par
Step D4 leaves the assertion $i\geq1$ invariant (because Step D4 decreases $i$
by $1$ only if $i\neq1$, so that $i$ can never be decreased to $0$ in Step D4)
and leaves the assertion $j\geq1$ invariant (since $j$ is not changed in Step
D4).}, so that nothing goes wrong if we add these two assertions into the
parentheses in each of steps D2, D3 and D4. Adding these two assertions into
the parentheses in each of steps D2, D3 and D4, we see that the algorithm
changes the value of $y_{ij}$ only for certain pairs $\left(  i,j\right)  $
satisfying $i\geq1$ and $j\geq1$; in particular, the leftmost column and the
uppermost row of $Y$ are never changed, so they remain filled with zeroes
throughout the algorithm (because they were filled with zeroes initially).

\rule{17cm}{0.3mm}

\textbf{Page 713:} Here, Knuth gives a brief argument why "the deletion
algorithm recomputes the sequences (2.5) determined by the insertion
algorithm, and it restores $Y$ to its original condition". Let me try to
detail this argument. First, let us introduce a basic notation:

\begin{quote}
\textbf{Convention A.0.} \textbf{(a)} In the following, we will use the
abbreviation "GYT" for "generalized Young tableau".

\textbf{(b)} In the following, "\textit{number}" will mean an element of
$\mathbb{N}\cup\left\{  \infty\right\}  $. Thus, we will be counting both $0$
and $\infty$ as numbers (but not as positive integers).

\textbf{(c)} In the following, we defined the relation $<_{\infty}$ on the set
$\mathbb{N}\cup\left\{  \infty\right\}  $ by%
\[
\left(  \left(  a<_{\infty}b\ \Longleftrightarrow\ \left(  a<b\text{ and
}a\neq\infty\right)  \right)  \ \ \ \ \ \ \ \ \ \ \text{for all }%
a\in\mathbb{N}\cup\left\{  \infty\right\}  \text{ and }b\in\mathbb{N}%
\cup\left\{  \infty\right\}  \right)  .
\]
So this relation $<_{\infty}$ differs from $<$ only in the fact that
$\infty<\infty$ is true but $\infty<_{\infty}\infty$ is false.

\textbf{Definition A.1.} If $Y$ is a GYT, and $\alpha$ and $\beta$ are two
nonnegative integers, then $Y_{\alpha,\beta}$ will denote the element of the
GYT $Y$ in row $\alpha$ and column $\beta$ (where the rows are counted from
$0$ and the columns also are counted from $0$). In other words, $Y_{\alpha
,\beta}$ denotes what Knuth calls $y_{\alpha\beta}$ on page 711.
\end{quote}

This definition makes one wonder why we are introducing a new notation for
something that Knuth has already given a name. The reason is that we will use
$Y_{\alpha,\beta}$ and $Y$ as \textit{immutable} variables, whereas we will
use $y_{\alpha\beta}$ as \textit{mutable} variables. Here is the precise
convention of what will be mutable:

\begin{quote}
\textbf{Convention A.2.} When we will be speaking of the algorithm
$\operatorname*{INSERT}\left(  x\right)  $, applied to some GYT $Y$, we will
use $i$, $j$, $r_{\alpha}$, $x_{\alpha}$, $y_{\alpha,\beta}$, $s$ and $t$ (for
$\alpha$ and $\beta$ nonnegative integers) as \textit{mutable} variables (i.
e., we will be able to speak of "the value of $y_{\alpha,\beta}$ after step
I1" and of "the value of $y_{\alpha,\beta}$ after step I5", and these two
values are in general not the same), whereas $Y$ (and therefore $Y_{\alpha
,\beta}$ for any nonnegative integers $\alpha$ and $\beta$) and $x$ are to be
understood as \textit{immutable} variables\footnote{Note that we are deviating
from Knuth's notations here: Knuth uses $Y$ as a mutable variable, so he can
make statements like "$Y$ remains a generalized Young tableau throughout the
algorithm". (We have also made such statements above, during our previous
comments. But we will not make them in this comment.)} (so that it makes no
sense to speak of "the GYT $Y$ after the algorithm" or "the GYT $Y$ before the
algorithm", because $Y$ always means the GYT that we started with).
\end{quote}

Now, let us introduce some further \textit{immutable} variables for the values
of $r_{\alpha}$, $x_{\alpha}$, $y_{\alpha\beta}$, $s$ and $t$ \textit{after
the termination of the algorithm }$\operatorname*{INSERT}\left(  x\right)  $:

\begin{quote}
\textbf{Definition A.3.} Let $Y$ be a GYT, and $x$ be a positive integer.

As we know, the algorithm $\operatorname*{INSERT}\left(  x\right)  $, applied
to the GYT $Y$, yields a new GYT. We cannot denote this new GYT by $Y$ again,
since $Y$ is an immutable variable and thus always denotes the \textit{old}
GYT that we had before applying $\operatorname*{INSERT}\left(  x\right)  $.
Instead, we will denote by $\operatorname*{ins}\left(  Y,x\right)  $ the GYT
that is obtained by applying the algorithm $\operatorname*{INSERT}\left(
x\right)  $ to $Y$.\ \ \ \ \footnote{Note that when we say "the GYT that is
obtained by applying the algorithm $\operatorname*{INSERT}\left(  x\right)  $
to $Y$", we mean the GYT that we receive \textit{after the algorithm
}$\operatorname*{INSERT}\left(  x\right)  $ \textit{applied to }$Y$
\textit{has terminated}, rather than some intermediate snapshot of the GYT
during the execution of the algorithm.} In other words, we will denote by
$\operatorname*{ins}\left(  Y,x\right)  $ the GYT $\left(  y_{\alpha,\beta
}\right)  _{\left(  \alpha,\beta\right)  \in\mathbb{N}^{2}}$ after the
termination of the algorithm $\operatorname*{INSERT}\left(  x\right)  $
applied to $Y$.

The algorithm $\operatorname*{INSERT}\left(  x\right)  $, applied to the GYT
$Y$, not only yields a new GYT $\operatorname*{ins}\left(  Y,x\right)  $, but
also computes certain numbers $s$, $t$, $x_{1}$, $x_{2}$, $...$, $x_{s+1}$,
$r_{1}$, $r_{2}$, $...$, $r_{s}$ (where "number" means an element of
$\mathbb{N}\cup\left\{  \infty\right\}  $). Let us give these numbers some new
names to stress their dependence on $Y$ and $x$: We will denote by
$\mathbf{s}\left(  Y,x\right)  $ and $\mathbf{t}\left(  Y,x\right)  $ the
values of $s$ and $t$ after the termination of the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ applied to $Y$. Also, for every
$\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  +1\right\}  $, we
will denote by $\mathbf{x}_{\alpha}\left(  Y,x\right)  $ the value of
$x_{\alpha}$ after the termination of the algorithm $\operatorname*{INSERT}%
\left(  x\right)  $ applied to $Y$. Finally, for every $\alpha\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $, we will denote by
$\mathbf{r}_{\alpha}\left(  Y,x\right)  $ the value of $r_{\alpha}$ after the
termination of the algorithm $\operatorname*{INSERT}\left(  x\right)  $
applied to $Y$.

Clearly, the relations (2.5) rewrite as%
\begin{align*}
x  &  =\mathbf{x}_{1}\left(  Y,x\right)  <\mathbf{x}_{2}\left(  Y,x\right)
<\cdots<\mathbf{x}_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  ;\\
\mathbf{r}_{1}\left(  Y,x\right)   &  \geq\mathbf{r}_{2}\left(  Y,x\right)
\geq\cdots\geq\mathbf{r}_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  .
\end{align*}
Also, the fact that $x_{s+1}=\infty$ at the end of the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ rewrites as $\mathbf{x}%
_{s+1}\left(  Y,x\right)  =\infty$.
\end{quote}

Let us write down some basic facts about $\operatorname*{INSERT}\left(
x\right)  $:

\begin{quote}
\textbf{Proposition A.4.} Let $Y$ be a GYT, and $x$ be a positive integer.

\textbf{(a)} We have $\mathbf{x}_{1}\left(  Y,x\right)  =x$.

\textbf{(b)} For every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  $, the number $\mathbf{r}_{\alpha}\left(  Y,x\right)  $
is the smallest $p\in\mathbb{N}$ such that $\mathbf{x}_{\alpha}\left(
Y,x\right)  <Y_{\alpha,p}$.

\textbf{(c)} For every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  $, the number $\mathbf{r}_{\alpha}\left(  Y,x\right)  $
is the highest $p\in\mathbb{N}$ such that $\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{\alpha,p}<_{\infty}\mathbf{x}_{\alpha+1}\left(
Y,x\right)  $.

\textbf{(d)} For every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  $, we have $\mathbf{x}_{\alpha+1}\left(  Y,x\right)
=Y_{\alpha,\mathbf{r}_{\alpha}\left(  Y,x\right)  }$.

\textbf{(e)} For every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  $, we have $\mathbf{x}_{\alpha}\left(  Y,x\right)
=\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\alpha
,\mathbf{r}_{\alpha}\left(  Y,x\right)  }$.

\textbf{(f)} For every $\alpha\in\mathbb{N}$ and $\beta\in\mathbb{N}$, we have
$\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\alpha,\beta
}=Y_{\alpha,\beta}$ unless $\left(  \alpha\in\left\{  1,2,...,\mathbf{s}%
\left(  Y,x\right)  \right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(
Y,x\right)  \right)  $.

\textbf{(g)} We have $\mathbf{s}\left(  Y,x\right)  \geq1$, $\mathbf{t}\left(
Y,x\right)  \geq1$, $\left(  \operatorname*{ins}\left(  Y,x\right)  \right)
_{\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  }\neq\infty$
and $\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\mathbf{s}%
\left(  Y,x\right)  ,\left(  \mathbf{t}\left(  Y,x\right)  +1\right)
}=\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\left(
\mathbf{s}\left(  Y,x\right)  +1\right)  ,\mathbf{t}\left(  Y,x\right)
}=\infty$.

\textbf{(h)} We have $\mathbf{t}\left(  Y,x\right)  =\mathbf{r}_{\mathbf{s}%
\left(  Y,x\right)  }\left(  Y,x\right)  $.

\textbf{(i)} We have $\mathbf{x}_{\mathbf{s}\left(  Y,x\right)  +1}\left(
Y,x\right)  =\infty$.

\textbf{(j)} The numbers $\mathbf{x}_{1}\left(  Y,x\right)  $, $\mathbf{x}%
_{2}\left(  Y,x\right)  $, $...$, $\mathbf{x}_{\mathbf{s}\left(  Y,x\right)
}\left(  Y,x\right)  $ are positive integers (i. e., none of them is $\infty$)
and satisfy $\mathbf{x}_{1}\left(  Y,x\right)  <\mathbf{x}_{2}\left(
Y,x\right)  <...<\mathbf{x}_{\mathbf{s}\left(  Y,x\right)  }\left(
Y,x\right)  $.

\textbf{(k)} The numbers $\mathbf{r}_{1}\left(  Y,x\right)  $, $\mathbf{r}%
_{2}\left(  Y,x\right)  $, $...$, $\mathbf{r}_{\mathbf{s}\left(  Y,x\right)
}\left(  Y,x\right)  $ are positive integers (i. e., none of them is $\infty$)
and satisfy $\mathbf{r}_{1}\left(  Y,x\right)  \geq\mathbf{r}_{2}\left(
Y,x\right)  \geq...\geq\mathbf{r}_{\mathbf{s}\left(  Y,x\right)  }\left(
Y,x\right)  $.
\end{quote}

\textit{Proof of Proposition A.4.} We annotate the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ with some additional Hoare assertions:

\begin{quote}
\textbf{Algorithm }$\operatorname*{INSERT}\left(  x\right)  $\textbf{ applied
to a GYT }$Y$:

\textbf{I1.} [Hoare assertions:

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]

Set $i\leftarrow1$, set $x_{i}\leftarrow x$, and set $j$ to some value such
that $y_{1,j}=\infty$.

\textbf{I2.} [Hoare assertions:

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$ except of those satisfying $\left(  \alpha\in\left\{
1,2,...,i-1\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- For all $\alpha\in\left\{  1,2,...,i-1\right\}  $, we have $y_{\alpha,
r_{\alpha}} = x_{\alpha}$.

- For all $\alpha\in\left\{  1,2,...,i-1\right\}  $, we have $Y_{\alpha,
r_{\alpha}} = x_{\alpha+1}$.

- We have $x_{1}=x$.

- For all $\alpha\in\left\{  1,2,...,i-1\right\}  $, the number $r_{\alpha}$
is the highest $p\in\mathbb{N}$ such that $y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- For all $\alpha\in\left\{  1,2,...,i-1\right\}  $, the number $r_{\alpha}$
is the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<Y_{\alpha,p}$.

- Furthermore, $y_{\left(  i-1\right)  ,j}<x_{i}<y_{i,j}$ and $x_{i}\neq
\infty$.

- We have $i\geq1$ and $j\geq1$.

- The numbers $x_{1}$, $x_{2}$, $...$, $x_{i}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $x_{1}<x_{2}<...<x_{i}$.

- The numbers $r_{1}$, $r_{2}$, $...$, $r_{i-1}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $r_{1}\geq r_{2}\geq...\geq r_{i-1}$.

- If $i>1$, then $r_{i-1}\geq j$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]

If $x_{i}<y_{i,\left(  j-1\right)  }$, decrease $j$ by $1$ and repeat this
step. Otherwise set $x_{i+1}\leftarrow y_{i,j}$ and set $r_{i}\leftarrow j$.

\textbf{I3.} [Hoare assertions:

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$ except of those satisfying $\left(  \alpha\in\left\{
1,2,...,i-1\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- For all $\alpha\in\left\{  1,2,...,i-1\right\}  $, we have $y_{\alpha,
r_{\alpha}} = x_{\alpha}$.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, we have $Y_{\alpha,
r_{\alpha}} = x_{\alpha+1}$.

- We have $x_{1}=x$.

- For all $\alpha\in\left\{  1,2,...,i-1\right\}  $, the number $r_{\alpha}$
is the highest $p\in\mathbb{N}$ such that $y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, the number $r_{\alpha}$ is
the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<Y_{\alpha,p}$.

- Furthermore, $y_{i,\left(  j-1\right)  }\leq x_{i}<x_{i+1}=y_{i,j}\leq
y_{i,\left(  j+1\right)  }$, $y_{\left(  i-1\right)  ,j}<x_{i}<x_{i+1}%
=y_{i,j}<y_{\left(  i+1\right)  ,j}$, $r_{i}=j$ and $x_{i}\neq\infty$.

- We have $i\geq1$ and $j\geq1$.

- The numbers $x_{1}$, $x_{2}$, $...$, $x_{i}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $x_{1}<x_{2}<...<x_{i}$.

- The numbers $r_{1}$, $r_{2}$, $...$, $r_{i}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $r_{1}\geq r_{2}\geq...\geq r_{i}$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]

Set $y_{i,j}\leftarrow x_{i}$.

\textbf{I4.} [Hoare assertions:

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$ except of those satisfying $\left(  \alpha\in\left\{
1,2,...,i\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, we have $y_{\alpha,
r_{\alpha}} = x_{\alpha}$.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, we have $Y_{\alpha,
r_{\alpha}} = x_{\alpha+1}$.

- We have $x_{1}=x$.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, the number $r_{\alpha}$ is
the highest $p\in\mathbb{N}$ such that $y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, the number $r_{\alpha}$ is
the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<Y_{\alpha,p}$.

- Furthermore, $y_{i,\left(  j-1\right)  }\leq y_{i,j}=x_{i}<x_{i+1}\leq
y_{i,\left(  j+1\right)  }$, $y_{\left(  i-1\right)  ,j}<y_{i,j}=x_{i}%
<x_{i+1}<y_{\left(  i+1\right)  ,j}$, $r_{i}=j$ and $x_{i}\neq\infty$.

- We have $i\geq1$ and $j\geq1$.

- The numbers $x_{1}$, $x_{2}$, $...$, $x_{i}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $x_{1}<x_{2}<...<x_{i}$.

- The numbers $r_{1}$, $r_{2}$, $...$, $r_{i}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $r_{1}\geq r_{2}\geq...\geq r_{i}$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]

If $x_{i+1}\neq\infty$, increase $i$ by $1$ and return to step \textbf{I2}.

\textbf{I5.} [Hoare assertions:

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$ except of those satisfying $\left(  \alpha\in\left\{
1,2,...,i\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, we have $y_{\alpha,
r_{\alpha}} = x_{\alpha}$.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, we have $Y_{\alpha,
r_{\alpha}} = x_{\alpha+1}$.

- We have $x_{1}=x$.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, the number $r_{\alpha}$ is
the highest $p\in\mathbb{N}$ such that $y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- For all $\alpha\in\left\{  1,2,...,i\right\}  $, the number $r_{\alpha}$ is
the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<Y_{\alpha,p}$.

- We have $r_{i}=j$.

- Now the conditions $y_{i,j}\neq\infty$ and $x_{i+1}=y_{i,\left(  j+1\right)
}=y_{\left(  i+1\right)  ,j}=\infty$ hold.

- We have $i\geq1$ and $j\geq1$.

- The numbers $x_{1}$, $x_{2}$, $...$, $x_{i}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $x_{1}<x_{2}<...<x_{i}$.

- The numbers $r_{1}$, $r_{2}$, $...$, $r_{i}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $r_{1}\geq r_{2}\geq...\geq r_{i}$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]

Set $s\leftarrow i$ and $t\leftarrow j$, and terminate the algorithm.

\textbf{End of the algorithm.} [Hoare assertions:

- We have $i=s$ and $j=t$.

- Now the conditions $y_{s,t}\neq\infty$ and $x_{s+1}=y_{s,\left(  t+1\right)
}=y_{\left(  s+1\right)  ,t}=\infty$ hold.

- Furthermore, $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative
integers $\alpha$ and $\beta$ except of those satisfying $\left(  \alpha
\in\left\{  1,2,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, we have $y_{\alpha,
r_{\alpha}} = x_{\alpha}$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, we have $Y_{\alpha,
r_{\alpha}} = x_{\alpha+1}$.

- We have $x_{1}=x$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, the number $r_{\alpha}$ is
the highest $p\in\mathbb{N}$ such that $y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, the number $r_{\alpha}$ is
the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<Y_{\alpha,p}$.

- We have $r_{s}=t$.

- We have $s\geq1$ and $t\geq1$.

- The numbers $x_{1}$, $x_{2}$, $...$, $x_{s}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $x_{1}<x_{2}<...<x_{s}$.

- The numbers $r_{1}$, $r_{2}$, $...$, $r_{s}$ are positive integers (i. e.,
none of them is $\infty$) and satisfy $r_{1}\geq r_{2}\geq...\geq r_{s}$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]
\end{quote}

It is completely straightforward to verify that these new Hoare assertions are
indeed respected by every step of the algorithm. We are leaving this
verification to the reader.\footnote{This verification requires checking the
following lemmata:
\par
\textbf{Lemma }$A_{I1}$\textbf{.} At the beginning of the execution of the
algorithm $\operatorname*{INSERT}\left(  x\right)  $, the Hoare assertions of
Step I1 are satisfied.
\par
\textbf{Lemma }$A_{I1\rightarrow I2}$\textbf{.} If we perform Step I1 at a
moment when the Hoare assertions of Step I1 are satisfied, then after this
step the Hoare assertions of Step I2 are satisfied.
\par
\textbf{Lemma }$A_{I2\rightarrow I2}$\textbf{.} If we perform Step I2 at a
moment when the Hoare assertions of Step I2 are satisfied and when
$x_{i}<y_{i,\left(  j-1\right)  }$ holds, then after this step the Hoare
assertions of Step I2 are satisfied.
\par
\textbf{Lemma }$A_{I2\rightarrow I3}$\textbf{.} If we perform Step I2 at a
moment when the Hoare assertions of Step I2 are satisfied and when
$x_{i}<y_{i,\left(  j-1\right)  }$ does not hold, then after this step the
Hoare assertions of Step I3 are satisfied.
\par
\textbf{Lemma }$A_{I3\rightarrow I4}$\textbf{.} If we perform Step I3 at a
moment when the Hoare assertions of Step I3 are satisfied, then after this
step the Hoare assertions of Step I4 are satisfied.
\par
\textbf{Lemma }$A_{I4\rightarrow I2}$\textbf{.} If we perform Step I4 at a
moment when the Hoare assertions of Step I4 are satisfied and when
$x_{i+1}\neq\infty$ holds, then after this step the Hoare assertions of Step
I2 are satisfied.
\par
\textbf{Lemma }$A_{I4\rightarrow I5}$\textbf{.} If we perform Step I4 at a
moment when the Hoare assertions of Step I4 are satisfied and when
$x_{i+1}\neq\infty$ does not hold, then after this step the Hoare assertions
of Step I5 are satisfied.
\par
\textbf{Lemma }$A_{I5\rightarrow}$\textbf{.} If we perform Step I5 at a moment
when the Hoare assertions of Step I5 are satisfied, then after this step the
Hoare assertions of the end of the algorithm are satisfied.
\par
Verifying these assertions is somewhat of a lengthy chore since there are many
Hoare assertions to be checked, but most of them are trivial to check. As an
example, let us show one part of the verification (actually, one of the
hardest parts):
\par
\textbf{Lemma A.4a.} If we perform Step I2 at a moment when the Hoare
assertions of Step I2 are satisfied and when $x_{i}<y_{i,\left(  j-1\right)
}$ does not hold, then after this step the assertion "For all $\alpha
\in\left\{  1,2,...,i\right\}  $, the number $r_{\alpha}$ is the smallest
$p\in\mathbb{N}$ such that $x_{\alpha}<Y_{\alpha,p}$" is satisfied.
\par
(Proving this Lemma A.4a is part of the proof of Lemma $\mathcal{A}%
_{I2\rightarrow I3}$. The other parts of the proof of Lemma $\mathcal{A}%
_{I2\rightarrow I3}$, and also the proofs of the other lemmata, are similar
and often easier.)
\par
\textit{Proof of Lemma A.4a.} Consider a moment when the Hoare assertions of
Step I2 are satisfied and when $x_{i}<y_{i,\left(  j-1\right)  }$ does not
hold.
\par
First let us notice that the value of $i$ before Step I2 equals the value of
$i$ after the Step I2 (because Step I2 does not change $i$). Thus, in the
following, we will refer to the variable $i$ without specifying whether we
mean its value before Step I2 or its value after Step I2.
\par
Now, let $\alpha\in\left\{  1,2,...,i\right\}  $ be arbitrary. Then, we must
be in one of the following two cases:
\par
\textit{Case 1:} We have $\alpha\in\left\{  1,2,...,i-1\right\}  $.
\par
\textit{Case 2:} We have $\alpha=i$.
\par
First let us consider Case 1. In this case, $\alpha\in\left\{
1,2,...,i-1\right\}  $, so that $\alpha\neq i$ and $\alpha\neq i+1$. Before we
perform the Step I2, the Hoare assertions of Step I2 are satisfied (by our
assumption). Hence, before we perform the Step I2, we have
\[
r_{\alpha}=\left(  \text{the smallest }p\in\mathbb{N}\text{ such that
}x_{\alpha}<Y_{\alpha,p}\right)
\]
(because one of the Hoare assertions of Step I2 is "For all $\alpha\in\left\{
1,2,...,i-1\right\}  $, the number $r_{\alpha}$ is the smallest $p\in
\mathbb{N}$ such that $x_{\alpha}<Y_{\alpha,p}$"). Since the performing of
Step I2 does not change any of the variables $r_{\alpha}$, $x_{\alpha}$ and
$Y_{\alpha,p}$ (in fact, Step I2 only changes $x_{i+1}$ and $r_{i}$, so that
it does not change $r_{\alpha}$ (since $i\neq\alpha$) and it does not change
$x_{\alpha}$ (since $\alpha\neq i+1$), and it does not change $Y_{\alpha,p}$
either (since $Y_{\alpha,p}$ is an immutable variable)), this yields that
after this step we still have%
\[
r_{\alpha}=\left(  \text{the smallest }p\in\mathbb{N}\text{ such that
}x_{\alpha}<Y_{\alpha,p}\right)  .
\]
Thus, we have proven that in Case 1, after the Step I2 is performed, the
number $r_{\alpha}$ is the smallest $p\in\mathbb{N}$ such that $x_{\alpha
}<Y_{\alpha,p}$.
\par
Now let us consider Case 2. In this case, $\alpha=i$.
\par
Before we perform the Step I2, the Hoare assertions of Step I2 are satisfied
(by our assumption). Since one of the Hoare assertions of Step I2 is "The
family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT", this yields that the family $\left(
y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)  \in\mathbb{N}^{2}}$ is
a GYT before Step I2. Since Step I2 does not change the family $\left(
y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)  \in\mathbb{N}^{2}}$
(because Step I2 only changes $x_{i+1}$ and $r_{i}$), this yields that the
family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is still a GYT after Step I2. Thus, each row of $\left(
y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)  \in\mathbb{N}^{2}}$ is
weakly increasing after Step I2. Thus, after Step I2, we have%
\begin{equation}
y_{i,u}\leq y_{i,v}\ \ \ \ \ \ \ \ \ \ \text{for any }u\in\mathbb{N}\text{ and
}v\in\mathbb{N}\text{ satisfying }u\leq v. \label{A4a.pf.1}%
\end{equation}
\par
Before we perform the Step I2, the Hoare assertions of Step I2 are satisfied
(by our assumption). Since one of the Hoare assertions of Step I2 is
"Furthermore, $y_{\left(  i-1\right)  ,j}<x_{i}<y_{i,j}$ and $x_{i}\neq\infty
$", this yields the following: Before we perform the Step I2, we have
$y_{\left(  i-1\right)  ,j}<x_{i}<y_{i,j}$ and $x_{i}\neq\infty$. Since the
performing of Step I2 does not change any of the variables $y_{\left(
i-1\right)  ,j}$, $x_{i}$ and $y_{i,j}$ (in fact, Step I2 only changes
$x_{i+1}$ and $r_{i}$), this yields that after this step we still have
$y_{\left(  i-1\right)  ,j}<x_{i}<y_{i,j}$ and $x_{i}\neq\infty$.
\par
Before we perform the Step I2, the relation $x_{i}<y_{i,\left(  j-1\right)  }$
does not hold (by our assumption). Hence, before we perform the Step I2, we
have $y_{i,\left(  j-1\right)  }\leq x_{i}$. Since the performing of Step I2
does not change any of the variables $y_{i,\left(  j-1\right)  }$ and $x_{i}$
(in fact, Step I2 only changes $x_{i+1}$ and $r_{i}$), this yields that after
this step we still have $y_{i,\left(  j-1\right)  }\leq x_{i}$. Combined with
$x_{i}\neq\infty$, this yields that we do \textit{not} have $x_{i}%
<y_{i,\left(  j-1\right)  }$ after Step I2. Hence, for every nonnegative
integer $k<j$, we do \textit{not} have $x_{i}<y_{i,k}$ after Step I2 (because
otherwise, we would have $x_{i}<y_{i,k}$ and thus%
\[
x_{i}<y_{i,k}\leq y_{i,\left(  j-1\right)  }\ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{by (\ref{A4a.pf.1}) (applied to }u=k\text{ and }v=j-1\text{),}\\
\text{since }k\leq j-1\text{ (because }k<j\text{ and because }k\text{ and
}j\text{ are integers)}%
\end{array}
\right)  ,
\]
contradicting the fact that we do \textit{not} have $x_{i}<y_{i,\left(
j-1\right)  }$ after Step I2).
\par
Hence, after the Step I2 is performed,
\begin{align}
r_{\alpha}  &  =r_{i}\ \ \ \ \ \ \ \ \ \ \left(  \text{since }\alpha=i\right)
\nonumber\\
&  =j\ \ \ \ \ \ \ \ \ \ \left(  \text{since Step I2 set }r_{i}\text{ to
}j\text{ without changing any of }i\text{ or }j\right) \nonumber\\
&  =\left(  \text{the smallest }p\in\mathbb{N}\text{ such that }x_{i}%
<y_{i,p}\right) \label{A.4.pf.-1}\\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since we have }x_{i}<y_{i,j}\text{ after Step I2,}\\
\text{but for every nonnegative integer }k<j\text{, we do \textit{not} have
}x_{i}<y_{i,k}\text{ after Step I2}%
\end{array}
\right)  .\nonumber
\end{align}
\par
On the other hand, before we perform the Step I2, the Hoare assertions of Step
I2 are satisfied (by our assumption). Hence, before we perform the Step I2, we
have
\begin{equation}
\left(
\begin{array}
[c]{c}%
y_{\alpha,\beta}=Y_{\alpha,\beta}\ \ \ \ \ \ \ \ \ \ \text{for all nonnegative
integers }\alpha\text{ and }\beta\\
\text{except of those satisfying }\left(  \alpha\in\left\{
1,2,...,i-1\right\}  \text{ and }\beta=r_{\alpha}\right)
\end{array}
\right)  \label{A.4.pf.0}%
\end{equation}
(because one of the Hoare assertions of Step I2 is "We have $y_{\alpha,\beta
}=Y_{\alpha,\beta}$ for all nonnegative integers $\alpha$ and $\beta$ except
of those satisfying $\left(  \alpha\in\left\{  1,2,...,i-1\right\}  \text{ and
}\beta=r_{\alpha}\right)  $"). Thus, before we perform the Step I2, we have%
\[
y_{i,p}=Y_{i,p}\ \ \ \ \ \ \ \ \ \ \text{for all }p\in\mathbb{N}%
\]
(by (\ref{A.4.pf.0}) (applied to $\alpha=i$ and $\beta=p$), since $i$ and $p$
do \textit{not} satisfy $\left(  i\in\left\{  1,2,...,i-1\right\}  \text{ and
}p=r_{i}\right)  $ (because $i\in\left\{  1,2,...,i-1\right\}  $ is clearly
wrong)). Since the performing of Step I2 does not change any of the variables
$y_{i,p}$ and $Y_{i,p}$ (in fact, Step I2 only changes $x_{i+1}$ and $r_{i}$),
this yields that after this step we still have%
\begin{equation}
y_{i,p}=Y_{i,p}\ \ \ \ \ \ \ \ \ \ \text{for all }p\in\mathbb{N}.
\label{A.4.pf.-2}%
\end{equation}
Hence, after the Step I2 is performed, we have%
\begin{align*}
r_{\alpha}  &  =\left(  \text{the smallest }p\in\mathbb{N}\text{ such that
}x_{i}<y_{i,p}\right)  \ \ \ \ \ \ \ \ \ \ \left(  \text{by (\ref{A.4.pf.-1}%
)}\right) \\
&  =\left(  \text{the smallest }p\in\mathbb{N}\text{ such that }x_{i}%
<Y_{i,p}\right)  \ \ \ \ \ \ \ \ \ \ \left(  \text{by (\ref{A.4.pf.-2}%
)}\right)  .
\end{align*}
Thus, we have proven that in Case 2, after the Step I2 is performed, the
number $r_{\alpha}$ is the smallest $p\in\mathbb{N}$ such that $x_{\alpha
}<Y_{\alpha,p}$.
\par
Hence, in each of the two cases 1 and 2, we have shown that after the Step I2
is performed, the number $r_{\alpha}$ is the smallest $p\in\mathbb{N}$ such
that $x_{\alpha}<Y_{\alpha,p}$. Since cases 1 and 2 cover all possibilities,
we have thus completely proven that after the Step I2 is performed, the number
$r_{\alpha}$ is the smallest $p\in\mathbb{N}$ such that $x_{\alpha}%
<Y_{\alpha,p}$. Since we have proven this for every $\alpha\in\left\{
1,2,...,i\right\}  $, we thus have shown that the assertion "For all
$\alpha\in\left\{  1,2,...,i\right\}  $, the number $r_{\alpha}$ is the
smallest $p\in\mathbb{N}$ such that $x_{\alpha}<Y_{\alpha,p}$" is satisfied
after we perform Step I2. This proves Lemma A.4a.}

Since Proposition A.4 does not mention any mutable variables, the validity of
Proposition A.4 does not depend on the state of the algorithm.

For the rest of the proof of Proposition A.4, we will work in the situation
after the termination of the algorithm $\operatorname*{INSERT}\left(
x\right)  $ applied to $Y$ (this is allowed since the validity of Proposition
A.4 does not depend on the state of the algorithm). This means that whenever
we will mention one of the mutable variables (e. g., the variable $x_{\alpha}$
for some $\alpha$, or the variable $i$), we will mean the value of this
variable after the termination of the algorithm $\operatorname*{INSERT}\left(
x\right)  $ applied to $Y$.

Recall that we denoted by $\mathbf{s}\left(  Y,x\right)  $ and $\mathbf{t}%
\left(  Y,x\right)  $ the values of $s$ and $t$ after the termination of the
algorithm $\operatorname*{INSERT}\left(  x\right)  $ applied to $Y$. Since we
are working in the situation after the termination of the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ applied to $Y$, this means that we
have $\mathbf{s}\left(  Y,x\right)  =s$ and $\mathbf{t}\left(  Y,x\right)  =t$.

For every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  +1\right\}
$, we have denoted by $\mathbf{x}_{\alpha}\left(  Y,x\right)  $ the value of
$x_{\alpha}$ after the termination of the algorithm $\operatorname*{INSERT}%
\left(  x\right)  $ applied to $Y$. Since we are working in the situation
after the termination of the algorithm $\operatorname*{INSERT}\left(
x\right)  $ applied to $Y$, this means that we have $\mathbf{x}_{\alpha
}\left(  Y,x\right)  =x_{\alpha}$ for every $\alpha\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  +1\right\}  $. Applied to $\alpha+1$
instead of $\alpha$, this yields that $\mathbf{x}_{\alpha+1}\left(
Y,x\right)  =x_{\alpha+1}$ for every $\alpha\in\left\{  0,1,...,\mathbf{s}%
\left(  Y,x\right)  \right\}  $.

For every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}
$, we have denoted by $\mathbf{r}_{\alpha}\left(  Y,x\right)  $ the value of
$r_{\alpha}$ after the termination of the algorithm $\operatorname*{INSERT}%
\left(  x\right)  $ applied to $Y$. Since we are working in the situation
after the termination of the algorithm $\operatorname*{INSERT}\left(
x\right)  $ applied to $Y$, this means that we have $\mathbf{r}_{\alpha
}\left(  Y,x\right)  =r_{\alpha}$ for every $\alpha\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $.

We have denoted by $\operatorname*{ins}\left(  Y,x\right)  $ the GYT $\left(
y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)  \in\mathbb{N}^{2}}$
after the termination of the algorithm $\operatorname*{INSERT}\left(
x\right)  $ applied to $Y$. Since we are working in the situation after the
termination of the algorithm $\operatorname*{INSERT}\left(  x\right)  $
applied to $Y$, this means that we have $\operatorname*{ins}\left(
Y,x\right)  =\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$. Hence,%
\begin{equation}
\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\alpha,\beta
}=y_{\alpha,\beta}\ \ \ \ \ \ \ \ \ \ \text{for every }\left(  \alpha
,\beta\right)  \in\mathbb{N}^{2}. \label{A.4.pf.1}%
\end{equation}


\textbf{(a)} We have%
\begin{align*}
&  \mathbf{x}_{1}\left(  Y,x\right) \\
&  =x_{1}\ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{x}_{\alpha}\left(
Y,x\right)  =x_{\alpha}\text{ for every }\alpha\in\left\{  1,2,...,\mathbf{s}%
\left(  Y,x\right)  +1\right\}  \right) \\
&  =x\ \ \ \ \ \ \ \ \ \ \left(  \text{because of the Hoare assertion "}%
x_{1}=x\text{" at the end of the algorithm }\operatorname*{INSERT}\left(
x\right)  \right)  .
\end{align*}
This proves Proposition A.4 \textbf{(a)}.

\textbf{(b)} Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies%
\[
\mathbf{r}_{\alpha}\left(  Y,x\right)  =r_{\alpha}=\left(  \text{the smallest
}p\in\mathbb{N}\text{ such that }x_{\alpha}<Y_{\alpha,p}\right)
\]
(by the Hoare assertion "For all $\alpha\in\left\{  1,2,...,s\right\}  $, the
number $r_{\alpha}$ is the smallest $p\in\mathbb{N}$ such that $x_{\alpha
}<Y_{\alpha,p}$" at the end of the algorithm $\operatorname*{INSERT}\left(
x\right)  $ applied to $Y$). Since $s=\mathbf{s}\left(  Y,x\right)  $ and
$x_{\alpha}=\mathbf{x}_{\alpha}\left(  Y,x\right)  $, this rewrites as
follows: Every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)
\right\}  $ satisfies
\[
\mathbf{r}_{\alpha}\left(  Y,x\right)  =\left(  \text{the smallest }%
p\in\mathbb{N}\text{ such that }\mathbf{x}_{\alpha}\left(  Y,x\right)
<Y_{\alpha,p}\right)  .
\]
This proves Proposition A.4 \textbf{(b)}.

\textbf{(c)} Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies%
\[
\mathbf{r}_{\alpha}\left(  Y,x\right)  =r_{\alpha}=\left(  \text{the highest
}p\in\mathbb{N}\text{ such that }y_{\alpha,p}<_{\infty}x_{\alpha+1}\right)
\]
(by the Hoare assertion "For all $\alpha\in\left\{  1,2,...,s\right\}  $, the
number $r_{\alpha}$ is the highest $p\in\mathbb{N}$ such that $y_{\alpha
,p}<_{\infty}x_{\alpha+1}$" at the end of the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ applied to $Y$). Since
$s=\mathbf{s}\left(  Y,x\right)  $, $x_{\alpha+1}=\mathbf{x}_{\alpha+1}\left(
Y,x\right)  $ and $y_{\alpha,p}=\left(  \operatorname*{ins}\left(  Y,x\right)
\right)  _{\alpha,p}$ (since (\ref{A.4.pf.1}) (applied to $\left(
\alpha,\beta\right)  =\left(  \alpha,p\right)  $) yields $\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{\alpha,p}=y_{\alpha,p}$),
this rewrites as follows: Every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  $ satisfies%
\[
\mathbf{r}_{\alpha}\left(  Y,x\right)  =\left(  \text{the highest }%
p\in\mathbb{N}\text{ such that }\left(  \operatorname*{ins}\left(  Y,x\right)
\right)  _{\alpha,p}<_{\infty}\mathbf{x}_{\alpha+1}\left(  Y,x\right)
\right)  .
\]
This proves Proposition A.4 \textbf{(c)}.

\textbf{(d)} Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies
$\mathbf{x}_{\alpha+1}\left(  Y,x\right)  =x_{\alpha+1}=Y_{\alpha,r_{\alpha}}$
(because of the Hoare assertion "For all $\alpha\in\left\{  1,2,...,s\right\}
$, we have $Y_{\alpha,r_{\alpha}}=x_{\alpha+1}$" at the end of the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ applied to $Y$). Since
$s=\mathbf{s}\left(  Y,x\right)  $ and $r_{\alpha}=\mathbf{r}_{\alpha}\left(
Y,x\right)  $, this rewrites as follows: Every $\alpha\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $ satisfies $\mathbf{x}%
_{\alpha+1}\left(  Y,x\right)  =Y_{\alpha,\mathbf{r}_{\alpha}\left(
Y,x\right)  }$. This proves Proposition A.4 \textbf{(d)}.

\textbf{(e)} Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies
$\mathbf{x}_{\alpha}\left(  Y,x\right)  =x_{\alpha}=y_{\alpha,r_{\alpha}}$
(because of the Hoare assertion "For all $\alpha\in\left\{  1,2,...,s\right\}
$, we have $y_{\alpha,r_{\alpha}}=x_{\alpha}$" at the end of the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ applied to $Y$). Since
$s=\mathbf{s}\left(  Y,x\right)  $ and $y_{\alpha,r_{\alpha}}=\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{\alpha,r_{\alpha}}$ (since
(\ref{A.4.pf.1}) (applied to $\left(  \alpha,\beta\right)  =\left(
\alpha,r_{\alpha}\right)  $) yields $\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{\alpha,r_{\alpha}}=y_{\alpha,r_{\alpha}}$), this
rewrites as follows: Every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  $ satisfies $\mathbf{x}_{\alpha}\left(  Y,x\right)
=\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\alpha,r_{\alpha}}%
$. Since $r_{\alpha}=\mathbf{r}_{\alpha}\left(  Y,x\right)  $, this rewrites
as follows: Every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)
\right\}  $ satisfies $\mathbf{x}_{\alpha}\left(  Y,x\right)  =\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{\alpha,\mathbf{r}_{\alpha
}\left(  Y,x\right)  }$. This proves Proposition A.4 \textbf{(e)}.

\textbf{(f)} Let $\alpha\in\mathbb{N}$ and $\beta\in\mathbb{N}$. Then, we have
$y_{\alpha,\beta}=Y_{\alpha,\beta}$ unless $\left(  \alpha\in\left\{
1,2,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $ (because of the
Hoare assertion "Furthermore, $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all
nonnegative integers $\alpha$ and $\beta$ except of those satisfying $\left(
\alpha\in\left\{  1,2,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $"
at the end of the algorithm $\operatorname*{INSERT}\left(  x\right)  $ applied
to $Y$). Since $s=\mathbf{s}\left(  Y,x\right)  $, $r_{\alpha}=\mathbf{r}%
_{\alpha}\left(  Y,x\right)  $ and $y_{\alpha,\beta}=\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{\alpha,\beta}$ (by
(\ref{A.4.pf.1})), this rewrites as follows: We have $\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{\alpha,\beta}=Y_{\alpha
,\beta}$ unless $\left(  \alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,x\right)
\right)  $. This proves Proposition A.4 \textbf{(f)}.

\textbf{(g)} We have $\mathbf{s}\left(  Y,x\right)  =s\geq1$ (due to the Hoare
assertion "We have $s\geq1$ and $t\geq1$" at the end of the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ applied to $Y$) and $\mathbf{t}%
\left(  Y,x\right)  =t\geq1$ (due to the Hoare assertion "We have $s\geq1$ and
$t\geq1$" at the end of the algorithm $\operatorname*{INSERT}\left(  x\right)
$ applied to $Y$). Besides, due to the Hoare assertion "Now the conditions
$y_{s,t}\neq\infty$ and $x_{s+1}=y_{s,\left(  t+1\right)  }=y_{\left(
s+1\right)  ,t}=\infty$ hold", we have $y_{s,t}\neq\infty$ and $x_{s+1}%
=y_{s,\left(  t+1\right)  }=y_{\left(  s+1\right)  ,t}=\infty$.

Now,%
\begin{align*}
\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\mathbf{s}\left(
Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  }  &  =\left(  \operatorname*{ins}%
\left(  Y,x\right)  \right)  _{s,t}\ \ \ \ \ \ \ \ \ \ \left(  \text{since
}\mathbf{s}\left(  Y,x\right)  =s\text{ and }\mathbf{t}\left(  Y,x\right)
=t\right) \\
&  =y_{s,t}\ \ \ \ \ \ \ \ \ \ \left(  \text{due to (\ref{A.4.pf.1}), applied
to }\left(  \alpha,\beta\right)  =\left(  s,t\right)  \right) \\
&  \neq\infty,
\end{align*}%
\begin{align*}
\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\mathbf{s}\left(
Y,x\right)  ,\left(  \mathbf{t}\left(  Y,x\right)  +1\right)  }  &  =\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{s,\left(  t+1\right)
}\ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{s}\left(  Y,x\right)
=s\text{ and }\mathbf{t}\left(  Y,x\right)  =t\right) \\
&  =y_{s,\left(  t+1\right)  }\ \ \ \ \ \ \ \ \ \ \left(  \text{due to
(\ref{A.4.pf.1}), applied to }\left(  \alpha,\beta\right)  =\left(
s,t+1\right)  \right) \\
&  =\infty,
\end{align*}
and%
\begin{align*}
\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\left(
\mathbf{s}\left(  Y,x\right)  +1\right)  ,\mathbf{t}\left(  Y,x\right)  }  &
=\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\left(  s+1\right)
,t}\ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{s}\left(  Y,x\right)
=s\text{ and }\mathbf{t}\left(  Y,x\right)  =t\right) \\
&  =y_{\left(  s+1\right)  ,t}\ \ \ \ \ \ \ \ \ \ \left(  \text{due to
(\ref{A.4.pf.1}), applied to }\left(  \alpha,\beta\right)  =\left(
s+1,t\right)  \right) \\
&  =\infty.
\end{align*}
This proves Proposition A.4 \textbf{(g)}.

\textbf{(h)} We have $\mathbf{r}_{\alpha}\left(  Y,x\right)  =r_{\alpha}$ for
every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $.
Applied to $\alpha=\mathbf{s}\left(  Y,x\right)  $, this yields%
\begin{align*}
\mathbf{r}_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)   &
=r_{\mathbf{s}\left(  Y,x\right)  }=r_{s}\ \ \ \ \ \ \ \ \ \ \left(
\text{since }\mathbf{s}\left(  Y,x\right)  =s\right) \\
&  =t\ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{due to the Hoare assertion "We have }r_{s}=t\text{" at the end}\\
\text{of the algorithm }\operatorname*{INSERT}\left(  x\right)  \text{ applied
to }Y
\end{array}
\right) \\
&  =\mathbf{t}\left(  Y,x\right)  .
\end{align*}
This proves Proposition A.4 \textbf{(h)}.

\textbf{(i)} We have $\mathbf{x}_{\alpha}\left(  Y,x\right)  =x_{\alpha}$ for
every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  +1\right\}  $.
Applying this to $\alpha=\mathbf{s}\left(  Y,x\right)  +1$, we obtain%
\begin{align*}
\mathbf{x}_{\mathbf{s}\left(  Y,x\right)  +1}\left(  Y,x\right)   &
=x_{\mathbf{s}\left(  Y,x\right)  +1}=x_{s+1}\ \ \ \ \ \ \ \ \ \ \left(
\text{since }\mathbf{s}\left(  Y,x\right)  =s\right) \\
&  =\infty
\end{align*}
(by the Hoare assertion "Now the conditions $y_{s,t}\neq\infty$ and
$x_{s+1}=y_{s,\left(  t+1\right)  }=y_{\left(  s+1\right)  ,t}=\infty$ hold"
at the end of the algorithm $\operatorname*{INSERT}\left(  x\right)  $ applied
to $Y$). This proves Proposition A.4 \textbf{(i)}.

\textbf{(j)} By the Hoare assertion "The numbers $x_{1}$, $x_{2}$, $...$,
$x_{s}$ are positive integers (i. e., none of them is $\infty$) and satisfy
$x_{1}<x_{2}<...<x_{s}$" at the end of the algorithm $\operatorname*{INSERT}%
\left(  x\right)  $ applied to $Y$, we know that the numbers $x_{1}$, $x_{2}$,
$...$, $x_{s}$ are positive integers (i. e., none of them is $\infty$) and
satisfy $x_{1}<x_{2}<...<x_{s}$. Since $s=\mathbf{s}\left(  Y,x\right)  $,
this rewrites as follows: The numbers $x_{1}$, $x_{2}$, $...$, $x_{\mathbf{s}%
\left(  Y,x\right)  }$ are positive integers (i. e., none of them is $\infty$)
and satisfy $x_{1}<x_{2}<...<x_{\mathbf{s}\left(  Y,x\right)  }$. Since
$x_{1}=\mathbf{x}_{1}\left(  Y,x\right)  $, $x_{2}=\mathbf{x}_{2}\left(
Y,x\right)  $, $...$, $x_{\mathbf{s}\left(  Y,x\right)  }=\mathbf{x}%
_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  $ (because $x_{\alpha
}=\mathbf{x}_{\alpha}\left(  Y,x\right)  $ for every $\alpha\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  +1\right\}  $), this rewrites as
follows: The numbers $\mathbf{x}_{1}\left(  Y,x\right)  $, $\mathbf{x}%
_{2}\left(  Y,x\right)  $, $...$, $\mathbf{x}_{\mathbf{s}\left(  Y,x\right)
}\left(  Y,x\right)  $ are positive integers (i. e., none of them is $\infty$)
and satisfy $\mathbf{x}_{1}\left(  Y,x\right)  <\mathbf{x}_{2}\left(
Y,x\right)  <...<\mathbf{x}_{\mathbf{s}\left(  Y,x\right)  }\left(
Y,x\right)  $. This proves Proposition A.4 \textbf{(j)}.

\textbf{(k)} By the Hoare assertion "The numbers $r_{1}$, $r_{2}$, $...$,
$r_{s}$ are positive integers (i. e., none of them is $\infty$) and satisfy
$r_{1}\geq r_{2}\geq...\geq r_{s}$" at the end of the algorithm
$\operatorname*{INSERT}\left(  x\right)  $ applied to $Y$, we know that the
numbers $r_{1}$, $r_{2}$, $...$, $r_{s}$ are positive integers (i. e., none of
them is $\infty$) and satisfy $r_{1}\geq r_{2}\geq...\geq r_{s}$. Since
$s=\mathbf{s}\left(  Y,x\right)  $, this rewrites as follows: The numbers
$r_{1}$, $r_{2}$, $...$, $r_{\mathbf{s}\left(  Y,x\right)  }$ are positive
integers (i. e., none of them is $\infty$) and satisfy $r_{1}\geq r_{2}%
\geq...\geq r_{\mathbf{s}\left(  Y,x\right)  }$. Since $r_{1}=\mathbf{r}%
_{1}\left(  Y,x\right)  $, $r_{2}=\mathbf{r}_{2}\left(  Y,x\right)  $, $...$,
$r_{\mathbf{s}\left(  Y,x\right)  }=\mathbf{r}_{\mathbf{s}\left(  Y,x\right)
}\left(  Y,x\right)  $ (because $r_{\alpha}=\mathbf{r}_{\alpha}\left(
Y,x\right)  $ for every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  $), this rewrites as follows: The numbers $\mathbf{r}%
_{1}\left(  Y,x\right)  $, $\mathbf{r}_{2}\left(  Y,x\right)  $, $...$,
$\mathbf{r}_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  $ are positive
integers (i. e., none of them is $\infty$) and satisfy $\mathbf{r}_{1}\left(
Y,x\right)  \geq\mathbf{r}_{2}\left(  Y,x\right)  \geq...\geq\mathbf{r}%
_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  $. This proves
Proposition A.4 \textbf{(k)}.

The proof of Proposition A.4 is now complete.

We now will formulate the analogue of Convention A.2 for the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $:

\begin{quote}
\textbf{Convention A.5.} When we will be speaking of the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $, applied to some GYT $Y$, we will
use $i$, $j$, $r_{\alpha}$, $x_{\alpha}$, $y_{\alpha,\beta}$ and $x$ (for
$\alpha$ and $\beta$ nonnegative integers) as \textit{mutable} variables (i.
e., we will be able to speak of "the value of $y_{\alpha,\beta}$ after step
D1" and of "the value of $y_{\alpha,\beta}$ after step D5", and these two
values are in general not the same), whereas $Y$ (and therefore $Y_{\alpha
,\beta}$ for any nonnegative integers $\alpha$ and $\beta$) and $s$ and $t$
are to be understood as \textit{immutable} variables\footnote{Note that we are
deviating from Knuth's notations here: Knuth uses $Y$ as a mutable variable,
so he can make statements like "$Y$ remains a generalized Young tableau
throughout the algorithm". (We have also made such statements above, during
our previous comments. But we will not make them in this comment.)} (so that
it makes no sense to speak of "the GYT $Y$ after the algorithm" or "the GYT
$Y$ before the algorithm", because $Y$ always means the GYT that we started with).
\end{quote}

Now, let us introduce some further \textit{immutable} variables for the values
of $r_{\alpha}$, $x_{\alpha}$, $y_{\alpha\beta}$ and $x$ \textit{after the
termination of the algorithm }$\operatorname*{DELETE}\left(  s,t\right)  $:

\begin{quote}
\textbf{Definition A.6.} Let $Y$ be a GYT, and $s$ and $t$ be two nonnegative
integers satisfying $s\geq1$, $t\geq1$, $Y_{s,t}\neq\infty$ and $Y_{s,\left(
t+1\right)  }=Y_{\left(  s+1\right)  ,t}=\infty$.

As we know, the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $,
applied to the GYT $Y$, yields a new GYT. We cannot denote this new GYT by $Y$
again, since $Y$ is an immutable variable and thus always denotes the
\textit{old} GYT that we had before applying $\operatorname*{DELETE}\left(
s,t\right)  $. Instead, we will denote by $\operatorname*{del}\left(
Y,s,t\right)  $ the GYT that is obtained by applying the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ to $Y$.\ \ \ \ \footnote{Note
that when we say "the GYT that is obtained by applying the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ to $Y$", we mean the GYT that we
receive \textit{after the algorithm }$\operatorname*{DELETE}\left(
s,t\right)  $ \textit{applied to }$Y$ \textit{has terminated}, rather than
some intermediate snapshot of the GYT during the execution of the algorithm.}
In other words, we will denote by $\operatorname*{del}\left(  Y,s,t\right)  $
the GYT $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ after the termination of the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$.

The algorithm $\operatorname*{DELETE}\left(  s,t\right)  $, applied to the GYT
$Y$, not only yields a new GYT $\operatorname*{del}\left(  Y,s,t\right)  $,
but also computes certain numbers $x$, $x_{1}$, $x_{2}$, $...$, $x_{s+1}$,
$r_{1}$, $r_{2}$, $...$, $r_{s}$ (where "number" means an element of
$\mathbb{N}\cup\left\{  \infty\right\}  $). Let us give these numbers some new
names to stress their dependence on $Y$ and $s$ and $t$: We will denote by
$\mathbf{x}\left(  Y,s,t\right)  $ the value of $x$ after the termination of
the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$.
Also, for every $\alpha\in\left\{  1,2,...,s+1\right\}  $, we will denote by
$\mathbf{x}_{\alpha}\left(  Y,s,t\right)  $ the value of $x_{\alpha}$ after
the termination of the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $
applied to $Y$. Finally, for every $\alpha\in\left\{  1,2,...,s\right\}  $, we
will denote by $\mathbf{r}_{\alpha}\left(  Y,s,t\right)  $ the value of
$r_{\alpha}$ after the termination of the algorithm $\operatorname*{DELETE}%
\left(  s,t\right)  $ applied to $Y$.
\end{quote}

Let us write down some basic facts about $\operatorname*{DELETE}\left(
s,t\right)  $ (the analogues of Proposition A.4):

\begin{quote}
\textbf{Proposition A.7.} Let $Y$ be a GYT, and $s$ and $t$ be two nonnegative
integers satisfying $s\geq1$, $t\geq1$, $Y_{s,t}\neq\infty$ and $Y_{s,\left(
t+1\right)  }=Y_{\left(  s+1\right)  ,t}=\infty$.

\textbf{(a)} We have $\mathbf{x}_{s+1}\left(  Y,s,t\right)  =\infty$.

\textbf{(b)} For every $\alpha\in\left\{  1,2,...,s\right\}  $, the number
$\mathbf{r}_{\alpha}\left(  Y,s,t\right)  $ is the smallest $p\in\mathbb{N}$
such that $\mathbf{x}_{\alpha}\left(  Y,s,t\right)  <\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{\alpha,p}$.

\textbf{(c)} For every $\alpha\in\left\{  1,2,...,s\right\}  $, the number
$\mathbf{r}_{\alpha}\left(  Y,s,t\right)  $ is the highest $p\in\mathbb{N}$
such that $Y_{\alpha,p}<_{\infty}\mathbf{x}_{\alpha+1}\left(  Y,s,t\right)  $.

\textbf{(d)} For every $\alpha\in\left\{  1,2,...,s\right\}  $, we have
$\mathbf{x}_{\alpha+1}\left(  Y,s,t\right)  =\left(  \operatorname*{del}%
\left(  Y,s,t\right)  \right)  _{\alpha,\mathbf{r}_{\alpha}\left(
Y,s,t\right)  }$.

\textbf{(e)} For every $\alpha\in\left\{  1,2,...,s\right\}  $, we have
$\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =Y_{\alpha,\mathbf{r}_{\alpha
}\left(  Y,s,t\right)  }$.

\textbf{(f)} For every $\alpha\in\mathbb{N}$ and $\beta\in\mathbb{N}$, we have
$\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{\alpha,\beta
}=Y_{\alpha,\beta}$ unless $\left(  \alpha\in\left\{  1,2,...,s\right\}
\text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,s,t\right)  \right)  $.

\textbf{(g)} We have $\mathbf{x}\left(  Y,s,t\right)  =\mathbf{x}_{1}\left(
Y,s,t\right)  $.

\textbf{(h)} The number $\mathbf{x}\left(  Y,s,t\right)  $ is a positive integer.

\textbf{(i)} For every $\alpha\in\left\{  1,2,...,s\right\}  $, the number
$\mathbf{x}_{\alpha}\left(  Y,s,t\right)  $ is a positive integer.

\textbf{(j)} We have $\mathbf{r}_{s}\left(  Y,s,t\right)  =t$.
\end{quote}

\textit{Proof of Proposition A.7.} We annotate the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ with some additional Hoare assertions:

\begin{quote}
\textbf{Algorithm }$\operatorname*{DELETE}\left(  s,t\right)  $\textbf{
applied to a GYT }$Y$:

\textbf{D1.} [Hoare assertions:

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.

- The numbers $s$ and $t$ are two nonnegative integers satisfying $s\geq1$,
$t\geq1$, $Y_{s,t}\neq\infty$ and $Y_{s,\left(  t+1\right)  }=Y_{\left(
s+1\right)  ,t}=\infty$. ]

Set $j\leftarrow t$, set $i\leftarrow s$, and set $x_{s+1}\leftarrow\infty$.

\textbf{D2.} [Hoare assertions:

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$ except of those satisfying $\left(  \alpha\in\left\{
i+1,i+2,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- For all $\alpha\in\left\{  i+1,i+2,...,s\right\}  $, we have $Y_{\alpha
,r_{\alpha}}=x_{\alpha}$.

- For all $\alpha\in\left\{  i+1,i+2,...,s\right\}  $, we have $y_{\alpha
,r_{\alpha}}=x_{\alpha+1}$.

- We have $x_{s+1}=\infty$.

- For all $\alpha\in\left\{  i+1,i+2,...,s\right\}  $, the number $r_{\alpha}$
is the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<y_{\alpha,p}$.

- For all $\alpha\in\left\{  i+1,i+2,...,s\right\}  $, the number $r_{\alpha}$
is the highest $p\in\mathbb{N}$ such that $Y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- The number $x_{\alpha}$ is a positive integer (thus neither $0$ nor $\infty
$) for every $\alpha\in\left\{  i+1,i+2,...,s\right\}  $.

- Furthermore, $y_{i,j}<x_{i+1}<y_{\left(  i+1\right)  ,j}$ and $y_{i,j}%
\neq\infty$.

- We have $i\geq1$, $j\geq1$ and $i\leq s$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]

If $y_{i,\left(  j+1\right)  }<x_{i+1}$ and $y_{i,\left(  j+1\right)  }%
\neq\infty$, increase $j$ by $1$ and repeat this step. Otherwise set
$x_{i}\leftarrow y_{i,j}$ and set $r_{i}\leftarrow j$.

\textbf{D3.} [Hoare assertions:

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$ except of those satisfying $\left(  \alpha\in\left\{
i+1,i+2,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- For all $\alpha\in\left\{  i,i+1,...,s\right\}  $, we have $Y_{\alpha
,r_{\alpha}}=x_{\alpha}$.

- For all $\alpha\in\left\{  i+1,i+2,...,s\right\}  $, we have $y_{\alpha
,r_{\alpha}}=x_{\alpha+1}$.

- We have $x_{s+1}=\infty$.

- For all $\alpha\in\left\{  i+1,i+2,...,s\right\}  $, the number $r_{\alpha}$
is the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<y_{\alpha,p}$.

- For all $\alpha\in\left\{  i,i+1,...,s\right\}  $, the number $r_{\alpha}$
is the highest $p\in\mathbb{N}$ such that $Y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- The number $x_{\alpha}$ is a positive integer (thus neither $0$ nor $\infty
$) for every $\alpha\in\left\{  i,i+1,...,s\right\}  $.

- Furthermore, $y_{i,\left(  j-1\right)  }\leq y_{i,j}=x_{i}<x_{i+1}\leq
y_{i,\left(  j+1\right)  }$, $y_{\left(  i-1\right)  ,j}<y_{i,j}=x_{i}%
<x_{i+1}<y_{\left(  i+1\right)  ,j}$, $r_{i}=j$ and $x_{i}\neq\infty$.

- We have $i\geq1$, $j\geq1$ and $i\leq s$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]

Set $y_{i,j}\leftarrow x_{i+1}$.

\textbf{D4.} [Hoare assertions:

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$ except of those satisfying $\left(  \alpha\in\left\{
i,i+1,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- For all $\alpha\in\left\{  i,i+1,...,s\right\}  $, we have $Y_{\alpha
,r_{\alpha}}=x_{\alpha}$.

- For all $\alpha\in\left\{  i,i+1,...,s\right\}  $, we have $y_{\alpha
,r_{\alpha}}=x_{\alpha+1}$.

- We have $x_{s+1}=\infty$.

- For all $\alpha\in\left\{  i,i+1,...,s\right\}  $, the number $r_{\alpha}$
is the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<y_{\alpha,p}$.

- For all $\alpha\in\left\{  i,i+1,...,s\right\}  $, the number $r_{\alpha}$
is the highest $p\in\mathbb{N}$ such that $Y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- The number $x_{\alpha}$ is a positive integer (thus neither $0$ nor $\infty
$) for every $\alpha\in\left\{  i,i+1,...,s\right\}  $.

- Furthermore, $y_{i,\left(  j-1\right)  }\leq x_{i}<x_{i+1}=y_{i,j}\leq
y_{i,\left(  j+1\right)  }$, $y_{\left(  i-1\right)  ,j}<x_{i}<x_{i+1}%
=y_{i,j}<y_{\left(  i+1\right)  ,j}$, $r_{i}=j$ and $x_{i}\neq\infty$.

- We have $i\geq1$, $j\geq1$ and $i\leq s$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]

If $i\neq1$, decrease $i$ by $1$ and return to step \textbf{D2}.

\textbf{D5.} [Hoare assertions:

- We have $i=1$.

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$ except of those satisfying $\left(  \alpha\in\left\{
1,2,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, we have $Y_{\alpha
,r_{\alpha}}=x_{\alpha}$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, we have $y_{\alpha
,r_{\alpha}}=x_{\alpha+1}$.

- We have $x_{s+1}=\infty$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, the number $r_{\alpha}$ is
the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<y_{\alpha,p}$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, the number $r_{\alpha}$ is
the highest $p\in\mathbb{N}$ such that $Y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- The number $x_{\alpha}$ is a positive integer (thus neither $0$ nor $\infty
$) for every $\alpha\in\left\{  1,2,...,s\right\}  $.

- Furthermore, $y_{1,\left(  j-1\right)  }\leq x_{1}<x_{2}=y_{1,j}\leq
y_{1,\left(  j+1\right)  }$, $y_{0,j}<x_{1}<x_{2}=y_{1,j}<y_{\left(
i+1\right)  ,j}$, $r_{1}=j$ and $x_{1}\neq\infty$.

- We have $i\geq1$, $j\geq1$ and $i\leq s$.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]

Set $x\leftarrow x_{1}$, and terminate the algorithm.

\textbf{End of the algorithm.} [Hoare assertions:

- We have $x_{1}=x$.

- We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all nonnegative integers
$\alpha$ and $\beta$ except of those satisfying $\left(  \alpha\in\left\{
1,2,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $.

- We have $x\neq\infty$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, we have $Y_{\alpha
,r_{\alpha}}=x_{\alpha}$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, we have $y_{\alpha
,r_{\alpha}}=x_{\alpha+1}$.

- We have $x_{s+1}=\infty$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, the number $r_{\alpha}$ is
the smallest $p\in\mathbb{N}$ such that $x_{\alpha}<y_{\alpha,p}$.

- For all $\alpha\in\left\{  1,2,...,s\right\}  $, the number $r_{\alpha}$ is
the highest $p\in\mathbb{N}$ such that $Y_{\alpha,p}<_{\infty}x_{\alpha+1}$.

- The number $x_{\alpha}$ is a positive integer (thus neither $0$ nor $\infty
$) for every $\alpha\in\left\{  1,2,...,s\right\}  $.

- The family $\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)
\in\mathbb{N}^{2}}$ is a GYT.]
\end{quote}

It is completely straightforward to verify that these new Hoare assertions are
indeed respected by every step of the algorithm. We are leaving this
verification to the reader.\footnote{It is similar to the corresponding part
of the proof of Proposition A.4.}

Since Proposition A.7 does not mention any mutable variables, the validity of
Proposition A.7 does not depend on the state of the algorithm.

For the rest of the proof of Proposition A.7, we will work in the situation
after the termination of the algorithm $\operatorname*{DELETE}\left(
s,t\right)  $ applied to $Y$ (this is allowed since the validity of
Proposition A.7 does not depend on the state of the algorithm). This means
that whenever we will mention one of the mutable variables (e. g., the
variable $x_{\alpha}$ for some $\alpha$, or the variable $i$), we will mean
the value of this variable after the termination of the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$.

Recall that we denoted by $\mathbf{x}\left(  Y,s,t\right)  $ the value of $x$
after the termination of the algorithm $\operatorname*{DELETE}\left(
s,t\right)  $ applied to $Y$. Since we are working in the situation after the
termination of the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $
applied to $Y$, this means that we have $\mathbf{x}\left(  Y,s,t\right)  =x$.

For every $\alpha\in\left\{  1,2,...,s+1\right\}  $, we have denoted by
$\mathbf{x}_{\alpha}\left(  Y,s,t\right)  $ the value of $x_{\alpha}$ after
the termination of the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $
applied to $Y$. Since we are working in the situation after the termination of
the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$,
this means that we have $\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =x_{\alpha}$
for every $\alpha\in\left\{  1,2,...,s+1\right\}  $. Applied to $\alpha+1$
instead of $\alpha$, this yields that $\mathbf{x}_{\alpha+1}\left(
Y,s,t\right)  =x_{\alpha+1}$ for every $\alpha\in\left\{  0,1,...,s\right\}  $.

For every $\alpha\in\left\{  1,2,...,s\right\}  $, we have denoted by
$\mathbf{r}_{\alpha}\left(  Y,s,t\right)  $ the value of $r_{\alpha}$ after
the termination of the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $
applied to $Y$. Since we are working in the situation after the termination of
the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$,
this means that we have $\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =r_{\alpha}$
for every $\alpha\in\left\{  1,2,...,s\right\}  $.

We have denoted by $\operatorname*{del}\left(  Y,s,t\right)  $ the GYT
$\left(  y_{\alpha,\beta}\right)  _{\left(  \alpha,\beta\right)  \in
\mathbb{N}^{2}}$ after the termination of the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$. Since we are
working in the situation after the termination of the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$, this means that
we have $\operatorname*{del}\left(  Y,s,t\right)  =\left(  y_{\alpha,\beta
}\right)  _{\left(  \alpha,\beta\right)  \in\mathbb{N}^{2}}$. Hence,%
\begin{equation}
\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{\alpha,\beta
}=y_{\alpha,\beta}\ \ \ \ \ \ \ \ \ \ \text{for every }\left(  \alpha
,\beta\right)  \in\mathbb{N}^{2}. \label{A.7.pf.1}%
\end{equation}


\textbf{(a)} We have%
\begin{align*}
&  \mathbf{x}_{s+1}\left(  Y,s,t\right) \\
&  =x_{s+1}\ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{x}_{\alpha}\left(
Y,s,t\right)  =x_{\alpha}\text{ for every }\alpha\in\left\{
1,2,...,s+1\right\}  \right) \\
&  =\infty\ \ \ \ \ \ \ \ \ \ \left(  \text{because of the Hoare assertion
"}x_{s+1}=\infty\text{" at the end of the algorithm }\operatorname*{DELETE}%
\left(  s,t\right)  \right)  .
\end{align*}
This proves Proposition A.7 \textbf{(a)}.

\textbf{(b)} Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies%
\[
\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =r_{\alpha}=\left(  \text{the
smallest }p\in\mathbb{N}\text{ such that }x_{\alpha}<y_{\alpha,p}\right)
\]
(by the Hoare assertion "For all $\alpha\in\left\{  1,2,...,s\right\}  $, the
number $r_{\alpha}$ is the smallest $p\in\mathbb{N}$ such that $x_{\alpha
}<y_{\alpha,p}$" at the end of the algorithm $\operatorname*{DELETE}\left(
s,t\right)  $ applied to $Y$). Since $y_{\alpha,p}=\left(  \operatorname*{del}%
\left(  Y,s,t\right)  \right)  _{\alpha,p}$ (because (\ref{A.7.pf.1}) (applied
to $\left(  \alpha,\beta\right)  =\left(  \alpha,p\right)  $) yields $\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{\alpha,p}=y_{\alpha,p}$)
and $x_{\alpha}=\mathbf{x}_{\alpha}\left(  Y,s,t\right)  $, this rewrites as
follows: Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies
\[
\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =\left(  \text{the smallest }%
p\in\mathbb{N}\text{ such that }\mathbf{x}_{\alpha}\left(  Y,s,t\right)
<\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{\alpha,p}\right)
.
\]
This proves Proposition A.7 \textbf{(b)}.

\textbf{(c)} Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies%
\[
\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =r_{\alpha}=\left(  \text{the highest
}p\in\mathbb{N}\text{ such that }Y_{\alpha,p}<_{\infty}x_{\alpha+1}\right)
\]
(by the Hoare assertion "For all $\alpha\in\left\{  1,2,...,s\right\}  $, the
number $r_{\alpha}$ is the highest $p\in\mathbb{N}$ such that $Y_{\alpha
,p}<_{\infty}x_{\alpha+1}$" at the end of the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$). Since
$x_{\alpha+1}=\mathbf{x}_{\alpha+1}\left(  Y,s,t\right)  $, this rewrites as
follows: Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies%
\[
\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =\left(  \text{the highest }%
p\in\mathbb{N}\text{ such that }Y_{\alpha,p}<_{\infty}\mathbf{x}_{\alpha
+1}\left(  Y,s,t\right)  \right)  .
\]
This proves Proposition A.7 \textbf{(c)}.

\textbf{(d)} Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies
$\mathbf{x}_{\alpha+1}\left(  Y,s,t\right)  =x_{\alpha+1}=y_{\alpha,r_{\alpha
}}$ (because of the Hoare assertion "For all $\alpha\in\left\{
1,2,...,s\right\}  $, we have $y_{\alpha,r_{\alpha}}=x_{\alpha+1}$" at the end
of the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$).
Since $y_{\alpha,r_{\alpha}}=\left(  \operatorname*{del}\left(  Y,s,t\right)
\right)  _{\alpha,r_{\alpha}}$ (since (\ref{A.7.pf.1}) (applied to $\left(
\alpha,\beta\right)  =\left(  \alpha,r_{\alpha}\right)  $) yields $\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{\alpha,r_{\alpha}%
}=y_{\alpha,r_{\alpha}}$), this rewrites as follows: Every $\alpha\in\left\{
1,2,...,s\right\}  $ satisfies $\mathbf{x}_{\alpha+1}\left(  Y,s,t\right)
=\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{\alpha,r_{\alpha
}}$. Since $r_{\alpha}=\mathbf{r}_{\alpha}\left(  Y,s,t\right)  $, this
rewrites as follows: Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies
$\mathbf{x}_{\alpha+1}\left(  Y,s,t\right)  =\left(  \operatorname*{del}%
\left(  Y,s,t\right)  \right)  _{\alpha,\mathbf{r}_{\alpha}\left(
Y,s,t\right)  }$. This proves Proposition A.7 \textbf{(d)}.

\textbf{(e)} Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies
$\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =x_{\alpha}=Y_{\alpha,r_{\alpha}}$
(because of the Hoare assertion "For all $\alpha\in\left\{  1,2,...,s\right\}
$, we have $Y_{\alpha,r_{\alpha}}=x_{\alpha}$" at the end of the algorithm
$\operatorname*{DELETE}\left(  s,t\right)  $ applied to $Y$). Since
$r_{\alpha}=\mathbf{r}_{\alpha}\left(  Y,s,t\right)  $, this rewrites as
follows: Every $\alpha\in\left\{  1,2,...,s\right\}  $ satisfies
$\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =Y_{\alpha,\mathbf{r}_{\alpha
}\left(  Y,s,t\right)  }$. This proves Proposition A.7 \textbf{(e)}.

\textbf{(f)} Let $\alpha\in\mathbb{N}$ and $\beta\in\mathbb{N}$. Then, we have
$y_{\alpha,\beta}=Y_{\alpha,\beta}$ unless $\left(  \alpha\in\left\{
1,2,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $ (because of the
Hoare assertion "We have $y_{\alpha,\beta}=Y_{\alpha,\beta}$ for all
nonnegative integers $\alpha$ and $\beta$ except of those satisfying $\left(
\alpha\in\left\{  1,2,...,s\right\}  \text{ and }\beta=r_{\alpha}\right)  $"
at the end of the algorithm $\operatorname*{DELETE}\left(  s,t\right)  $
applied to $Y$). Since $r_{\alpha}=\mathbf{r}_{\alpha}\left(  Y,s,t\right)  $
and $y_{\alpha,\beta}=\left(  \operatorname*{del}\left(  Y,s,t\right)
\right)  _{\alpha,\beta}$ (by (\ref{A.7.pf.1})), this rewrites as follows: We
have $\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{\alpha
,\beta}=Y_{\alpha,\beta}$ unless $\left(  \alpha\in\left\{  1,2,...,s\right\}
\text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,s,t\right)  \right)  $. This
proves Proposition A.7 \textbf{(f)}.

\textbf{(g)} We have%
\begin{align*}
\mathbf{x}_{1}\left(  Y,s,t\right)   &  =x_{1}\ \ \ \ \ \ \ \ \ \ \left(
\text{since }\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =x_{\alpha}\text{ for
every }\alpha\in\left\{  1,2,...,s+1\right\}  \right) \\
&  =x\ \ \ \ \ \ \ \ \ \ \left(  \text{because of the Hoare assertion "}%
x_{1}=x\text{" at the end of the algorithm }\operatorname*{DELETE}\left(
s,t\right)  \right) \\
&  =\mathbf{x}\left(  Y,s,t\right)  .
\end{align*}
This proves Proposition A.7 \textbf{(g)}.

\textbf{(h)} We have the Hoare assertion "The number $x_{\alpha}$ is a
positive integer (thus neither $0$ nor $\infty$) for every $\alpha\in\left\{
1,2,...,s\right\}  $" at the end of the algorithm $\operatorname*{DELETE}%
\left(  s,t\right)  $. Thus we know that $x_{\alpha}$ is a positive integer
for every $\alpha\in\left\{  1,2,...,s\right\}  $. Applying this to $\alpha=1$
(this is allowed since $s\geq1$ and thus $1\in\left\{  1,2,...,s\right\}  $),
we conclude that $x_{1}$ is a positive integer. Since $x_{1}=\mathbf{x}\left(
Y,s,t\right)  $ (as we proved during the proof of Proposition A.7
\textbf{(g)}), this rewrites as follows: The number $\mathbf{x}\left(
Y,s,t\right)  $ is a positive integer. This proves Proposition A.7
\textbf{(h)}.

\textbf{(i)} Due to the Hoare assertion "The number $x_{\alpha}$ is a positive
integer (thus neither $0$ nor $\infty$) for every $\alpha\in\left\{
1,2,...,s\right\}  $" at the end of the algorithm $\operatorname*{DELETE}%
\left(  s,t\right)  $, we know that the number $x_{\alpha}$ is a positive
integer for every $\alpha\in\left\{  1,2,...,s\right\}  $. Since $x_{\alpha
}=\mathbf{x}_{\alpha}\left(  Y,s,t\right)  $ for every $\alpha\in\left\{
1,2,...,s+1\right\}  $, this rewrites as follows: The number $\mathbf{x}%
_{\alpha}\left(  Y,s,t\right)  $ is a positive integer for every $\alpha
\in\left\{  1,2,...,s\right\}  $. This proves Proposition A.7 \textbf{(i)}.

\textbf{(j)} By Proposition A.7 \textbf{(c)} (applied to $\alpha=s$), the
number $\mathbf{r}_{s}\left(  Y,s,t\right)  $ is the highest $p\in\mathbb{N}$
such that $Y_{s,p}<_{\infty}\mathbf{x}_{s+1}\left(  Y,s,t\right)  $. Thus,%
\begin{align*}
\mathbf{r}_{s}\left(  Y,s,t\right)   &  =\left(  \text{the highest }%
p\in\mathbb{N}\text{ such that }Y_{s,p}<_{\infty}\underbrace{\mathbf{x}%
_{s+1}\left(  Y,s,t\right)  }_{\substack{=\infty\\\text{(by Proposition A.7
\textbf{(a)})}}}\right) \\
&  =\left(  \text{the highest }p\in\mathbb{N}\text{ such that }Y_{s,p}%
<_{\infty}\infty\right) \\
&  =t\ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since we have }Y_{s,t}<_{\infty}\infty\text{ (because }Y_{s,t}\neq
\infty\text{) but}\\
\text{ we do not have }Y_{s,\left(  t+1\right)  }<_{\infty}\infty\text{
(because }Y_{s,\left(  t+1\right)  }=\infty\text{)}%
\end{array}
\right)  .
\end{align*}
This proves Proposition A.7 \textbf{(j)}.

The proof of Proposition A.7 is now complete.

We now state the property which Knuth laconically subsumes by "the deletion
algorithm recomputes the sequences (2.5) determined by the insertion
algorithm, and it restores $Y$ to its original condition":

\begin{quote}
\textbf{Proposition A.8.} Let $Y$ be a GYT, and $x$ be a positive integer.

\textbf{(a)} The family $\operatorname*{ins}\left(  Y,x\right)  $ is a GYT and
satisfies $\mathbf{s}\left(  Y,x\right)  \geq1$, $\mathbf{t}\left(
Y,x\right)  \geq1$, $\left(  \operatorname*{ins}\left(  Y,x\right)  \right)
_{\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  }\neq\infty$
and $\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\mathbf{s}%
\left(  Y,x\right)  ,\left(  \mathbf{t}\left(  Y,x\right)  +1\right)
}=\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\left(
\mathbf{s}\left(  Y,x\right)  +1\right)  ,\mathbf{t}\left(  Y,x\right)
}=\infty$. Thus, the algorithm $\operatorname*{DELETE}\left(  \mathbf{s}%
\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  \right)  $ can be applied
to the GYT $\operatorname*{ins}\left(  Y,x\right)  $.

\textbf{(b)} We have $\operatorname*{del}\left(  \operatorname*{ins}\left(
Y,x\right)  ,\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)
\right)  =Y$.

\textbf{(c)} For every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  +1\right\}  $, we have $\mathbf{x}_{\alpha}\left(  Y,x\right)
=\mathbf{x}_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)
,\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  \right)  $.

\textbf{(d)} For every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  $, we have $\mathbf{r}_{\alpha}\left(  Y,x\right)
=\mathbf{r}_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)
,\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  \right)  $.

\textbf{(e)} We have $\mathbf{x}\left(  \operatorname*{ins}\left(  Y,x\right)
,\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  \right)  =x$.
\end{quote}

Before we prove this proposition (the proof will be rather simple, since the
main work - the proof of Propositions A.4 and A.7 - has already been done),
let us point out what Proposition A.8 intuitively means: Proposition A.8
\textbf{(a)} shows that, after we have applied $\operatorname*{INSERT}\left(
x\right)  $ to a GYT $Y$, we can then apply $\operatorname*{DELETE}\left(
s,t\right)  $ to the resulting GYT, where $s$ and $t$ are the numbers computed
by $\operatorname*{INSERT}\left(  x\right)  $ (we have denoted these numbers
by $\mathbf{s}\left(  Y,x\right)  $ and $\mathbf{t}\left(  Y,x\right)  $).
Proposition A.8 \textbf{(b)} and \textbf{(e)} show that this application of
$\operatorname*{DELETE}\left(  s,t\right)  $ gives us our GYT $Y$ and our
integer $x$ back. Proposition A.8 \textbf{(c)} shows that it recomputes the
sequence $\left(  x_{1},x_{2},...,x_{s+1}\right)  $ which was already
constructed by $\operatorname*{INSERT}\left(  x\right)  $. Proposition A.8
\textbf{(d)} shows that it recomputes the sequence $\left(  r_{1}%
,r_{2},...,r_{s}\right)  $ which was already constructed by
$\operatorname*{INSERT}\left(  x\right)  $.

So let us now prove Proposition A.8.

\textit{Proof of Proposition A.8.} We know that $\operatorname*{ins}\left(
Y,x\right)  $ is a GYT. Also, from Proposition A.4 \textbf{(g)}, we know that
$\mathbf{s}\left(  Y,x\right)  \geq1$, $\mathbf{t}\left(  Y,x\right)  \geq1$,
$\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\mathbf{s}\left(
Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  }\neq\infty$ and $\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{\mathbf{s}\left(
Y,x\right)  ,\left(  \mathbf{t}\left(  Y,x\right)  +1\right)  }=\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{\left(  \mathbf{s}\left(
Y,x\right)  +1\right)  ,\mathbf{t}\left(  Y,x\right)  }=\infty$. Thus, the
algorithm $\operatorname*{DELETE}\left(  \mathbf{s}\left(  Y,x\right)
,\mathbf{t}\left(  Y,x\right)  \right)  $ can be applied to the GYT
$\operatorname*{ins}\left(  Y,x\right)  $. This proves Proposition A.8
\textbf{(a)}.

Let now $s=\mathbf{s}\left(  Y,x\right)  $ and $t=\mathbf{t}\left(
Y,x\right)  $. Then, $s=\mathbf{s}\left(  Y,x\right)  \geq1$, $t=\mathbf{t}%
\left(  Y,x\right)  \geq1$,
\begin{align*}
\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{s,t}  &  =\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{\mathbf{s}\left(
Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  }\ \ \ \ \ \ \ \ \ \ \left(
\text{since }s=\mathbf{s}\left(  Y,x\right)  \text{ and }t=\mathbf{t}\left(
Y,x\right)  \right) \\
&  \neq\infty,
\end{align*}%
\begin{align*}
\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{s,\left(
t+1\right)  }  &  =\left(  \operatorname*{ins}\left(  Y,x\right)  \right)
_{\mathbf{s}\left(  Y,x\right)  ,\left(  \mathbf{t}\left(  Y,x\right)
+1\right)  }\ \ \ \ \ \ \ \ \ \ \left(  \text{since }s=\mathbf{s}\left(
Y,x\right)  \text{ and }t=\mathbf{t}\left(  Y,x\right)  \right) \\
&  =\infty,
\end{align*}%
\begin{align*}
\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\left(  s+1\right)
,t}  &  =\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\left(
\mathbf{s}\left(  Y,x\right)  +1\right)  ,\mathbf{t}\left(  Y,x\right)
}\ \ \ \ \ \ \ \ \ \ \left(  \text{since }s=\mathbf{s}\left(  Y,x\right)
\text{ and }t=\mathbf{t}\left(  Y,x\right)  \right) \\
&  =\infty.
\end{align*}
These properties yield that we can apply Proposition A.7 to
$\operatorname*{ins}\left(  Y,x\right)  $ instead of $Y$.

Now let us prove Proposition A.8 \textbf{(c)} and \textbf{(d)}. First of all,
since $s=\mathbf{s}\left(  Y,x\right)  $, we have $\mathbf{x}_{s+1}\left(
Y,x\right)  =\mathbf{x}_{\mathbf{s}\left(  Y,x\right)  +1}\left(  Y,x\right)
=\infty$ (by Proposition A.4 \textbf{(i)}). Also, $\mathbf{x}_{s+1}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  =\infty$ (by Proposition
A.7 \textbf{(a)}, applied to $\operatorname*{ins}\left(  Y,x\right)  $ instead
of $Y$). Thus,
\begin{equation}
\mathbf{x}_{s+1}\left(  Y,x\right)  =\infty=\mathbf{x}_{s+1}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  . \label{A.8.pf.0}%
\end{equation}


Since $s=\mathbf{s}\left(  Y,x\right)  \in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  $, we can apply Proposition A.4 \textbf{(c)} to
$\alpha=s$, and conclude that the number $\mathbf{r}_{s}\left(  Y,x\right)  $
is the highest $p\in\mathbb{N}$ such that $\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{s,p}<_{\infty}\mathbf{x}_{s+1}\left(  Y,x\right)  $.

Since $s\in\left\{  1,2,...,s\right\}  $, we can apply Proposition A.7
\textbf{(c)} to $s$ and $\operatorname*{ins}\left(  Y,x\right)  $ instead of
$\alpha$ and $Y$, and conclude that the number $\mathbf{r}_{s}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  $ is the highest
$p\in\mathbb{N}$ such that $\left(  \operatorname*{ins}\left(  Y,x\right)
\right)  _{s,p}<_{\infty}\mathbf{x}_{s+1}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  $.

Hence,%
\begin{align}
\mathbf{r}_{s}\left(  Y,x\right)   &  =\left(  \text{the highest }%
p\in\mathbb{N}\text{ such that }\left(  \operatorname*{ins}\left(  Y,x\right)
\right)  _{s,p}<_{\infty}\underbrace{\mathbf{x}_{s+1}\left(  Y,x\right)
}_{\substack{=\mathbf{x}_{s+1}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \\\text{(by (\ref{A.8.pf.0}))}}}\right) \nonumber\\
&  =\left(  \text{the highest }p\in\mathbb{N}\text{ such that }\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{s,p}<_{\infty}%
\mathbf{x}_{s+1}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\right) \nonumber\\
&  =\mathbf{r}_{s}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
. \label{A.8.pf.0b}%
\end{align}


Since $s\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $, we can
apply Proposition A.4 \textbf{(e)} to $\alpha=s$, and conclude that
$\mathbf{x}_{s}\left(  Y,x\right)  =\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{s,\mathbf{r}_{s}\left(  Y,x\right)  }$. Since
$s\in\left\{  1,2,...,s\right\}  $, we can apply Proposition A.7 \textbf{(e)}
to $s$ and $\operatorname*{ins}\left(  Y,x\right)  $ instead of $\alpha$ and
$Y$, and conclude that $\mathbf{x}_{s}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  =\left(  \operatorname*{ins}\left(  Y,x\right)
\right)  _{s,\mathbf{r}_{s}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  }$. Thus,%
\begin{align}
\mathbf{x}_{s}\left(  Y,x\right)   &  =\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{s,\mathbf{r}_{s}\left(  Y,x\right)  }=\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{s,\mathbf{r}_{s}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  }\nonumber\\
&  \ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{r}_{s}\left(  Y,x\right)
=\mathbf{r}_{s}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\text{ by (\ref{A.8.pf.0b})}\right) \nonumber\\
&  =\mathbf{x}_{s}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
. \label{A.8.pf.0c}%
\end{align}


We are next going to prove that every $\ell\in\left\{  0,1,...,s-1\right\}  $
satisfies%
\begin{equation}
\left(  \mathbf{x}_{s-\ell}\left(  Y,x\right)  =\mathbf{x}_{s-\ell}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{s-\ell}\left(
Y,x\right)  =\mathbf{r}_{s-\ell}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \right)  . \label{A.8.pf.1}%
\end{equation}


\textit{Proof of (\ref{A.8.pf.1}).} We will prove (\ref{A.8.pf.1}) by
induction over $\ell$:

\textit{Induction base:} Due to (\ref{A.8.pf.0c}) and (\ref{A.8.pf.0b}), we
have
\[
\left(  \mathbf{x}_{s}\left(  Y,x\right)  =\mathbf{x}_{s}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{s}\left(
Y,x\right)  =\mathbf{r}_{s}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \right)  .
\]
Since $s=s-0$, this rewrites as%
\[
\left(  \mathbf{x}_{s-0}\left(  Y,x\right)  =\mathbf{x}_{s-0}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{s-0}\left(
Y,x\right)  =\mathbf{r}_{s-0}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \right)  .
\]
In other words, (\ref{A.8.pf.0}) holds for $\ell=0$. This completes the
induction base.

\textit{Induction step:} Let $\lambda\in\left\{  1,2,...,s-1\right\}  $ be
arbitrary. Assume that (\ref{A.8.pf.1}) holds for $\ell=\lambda-1$. We must
now prove that (\ref{A.8.pf.1}) holds for $\ell=\lambda$.

Since (\ref{A.8.pf.1}) holds for $\ell=\lambda-1$, we have%
\[
\left(  \mathbf{x}_{s-\left(  \lambda-1\right)  }\left(  Y,x\right)
=\mathbf{x}_{s-\left(  \lambda-1\right)  }\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  \ \ \ \ \ \ \ \ \ \ \text{and}%
\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{s-\left(  \lambda-1\right)  }\left(
Y,x\right)  =\mathbf{r}_{s-\left(  \lambda-1\right)  }\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  \right)  .
\]
Since $s-\left(  \lambda-1\right)  =s-\lambda+1$, this rewrites as follows:%
\begin{equation}
\left(  \mathbf{x}_{s-\lambda+1}\left(  Y,x\right)  =\mathbf{x}_{s-\lambda
+1}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{s-\lambda
+1}\left(  Y,x\right)  =\mathbf{r}_{s-\lambda+1}\left(  \operatorname*{ins}%
\left(  Y,x\right)  ,s,t\right)  \right)  . \label{A.8.pf.3}%
\end{equation}


Since $\lambda\in\left\{  1,2,...,s-1\right\}  $, we have $1\leq\lambda\leq
s-1$, so that $1\leq s-\lambda\leq s-1$, so that $s-\lambda\in\left\{
1,2,...,s\right\}  =\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $
(because $s=\mathbf{s}\left(  Y,x\right)  $). Thus, we can apply Proposition
A.4 \textbf{(c)} to $\alpha=s-\lambda$, and conclude that the number
$\mathbf{r}_{s-\lambda}\left(  Y,x\right)  $ is the highest $p\in\mathbb{N}$
such that $\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\left(
s-\lambda\right)  ,p}<_{\infty}\mathbf{x}_{s-\lambda+1}\left(  Y,x\right)  $.

Since $s-\lambda\in\left\{  1,2,...,s\right\}  $, we can apply Proposition A.7
\textbf{(c)} to $s-\lambda$ and $\operatorname*{ins}\left(  Y,x\right)  $
instead of $\alpha$ and $Y$, and conclude that the number $\mathbf{r}%
_{s-\lambda}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  $ is
the highest $p\in\mathbb{N}$ such that $\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{\left(  s-\lambda\right)  ,p}<_{\infty}\mathbf{x}%
_{s-\lambda+1}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  $.

Hence,%
\begin{align}
\mathbf{r}_{s-\lambda}\left(  Y,x\right)   &  =\left(  \text{the highest }%
p\in\mathbb{N}\text{ such that }\left(  \operatorname*{ins}\left(  Y,x\right)
\right)  _{\left(  s-\lambda\right)  ,p}<_{\infty}\underbrace{\mathbf{x}%
_{s-\lambda+1}\left(  Y,x\right)  }_{\substack{=\mathbf{x}_{s-\lambda
+1}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  \\\text{(by
(\ref{A.8.pf.3}))}}}\right) \nonumber\\
&  =\left(  \text{the highest }p\in\mathbb{N}\text{ such that }\left(
\operatorname*{ins}\left(  Y,x\right)  \right)  _{\left(  s-\lambda\right)
,p}<_{\infty}\mathbf{x}_{s-\lambda+1}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  \right) \nonumber\\
&  =\mathbf{r}_{s-\lambda}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  . \label{A.8.pf.4}%
\end{align}


Since $s-\lambda\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $,
we can apply Proposition A.4 \textbf{(e)} to $\alpha=s-\lambda$, and conclude
that $\mathbf{x}_{s-\lambda}\left(  Y,x\right)  =\left(  \operatorname*{ins}%
\left(  Y,x\right)  \right)  _{\left(  s-\lambda\right)  ,\mathbf{r}%
_{s-\lambda}\left(  Y,x\right)  }$. Since $s-\lambda\in\left\{
1,2,...,s\right\}  $, we can apply Proposition A.7 \textbf{(e)} to $s-\lambda$
and $\operatorname*{ins}\left(  Y,x\right)  $ instead of $\alpha$ and $Y$, and
conclude that $\mathbf{x}_{s-\lambda}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  =\left(  \operatorname*{ins}\left(  Y,x\right)
\right)  _{\left(  s-\lambda\right)  ,\mathbf{r}_{s-\lambda}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  }$. Thus,%
\begin{align*}
\mathbf{x}_{s-\lambda}\left(  Y,x\right)   &  =\left(  \operatorname*{ins}%
\left(  Y,x\right)  \right)  _{\left(  s-\lambda\right)  ,\mathbf{r}%
_{s-\lambda}\left(  Y,x\right)  }=\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{\left(  s-\lambda\right)  ,\mathbf{r}_{s-\lambda
}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  }\\
&  \ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{r}_{s-\lambda}\left(
Y,x\right)  =\mathbf{r}_{s-\lambda}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  \text{ by (\ref{A.8.pf.4})}\right) \\
&  =\mathbf{x}_{s-\lambda}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  .
\end{align*}
Combined with (\ref{A.8.pf.4}), this yields that%
\[
\left(  \mathbf{x}_{s-\lambda}\left(  Y,x\right)  =\mathbf{x}_{s-\lambda
}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{s-\lambda
}\left(  Y,x\right)  =\mathbf{r}_{s-\lambda}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  \right)  .
\]
In other words, (\ref{A.8.pf.1}) holds for $\ell=\lambda$. This completes the
induction step. Thus, the induction proof of (\ref{A.8.pf.1}) is complete.

Now, it is easy to see that for every $\alpha\in\left\{  1,2,...,s+1\right\}
$, we have $\mathbf{x}_{\alpha}\left(  Y,x\right)  =\mathbf{x}_{\alpha}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  $%
.\ \ \ \ \footnote{\textit{Proof.} Let $\alpha\in\left\{  1,2,...,s+1\right\}
$. Then, we must be in one of the following two cases:
\par
\textit{Case 1:} We have $\alpha\in\left\{  1,2,...,s\right\}  $.
\par
\textit{Case 2:} We have $\alpha=s+1$.
\par
First let us consider Case 1. In this case, $\alpha\in\left\{
1,2,...,s\right\}  $, so that $s-\alpha\in\left\{  0,1,...,s-1\right\}  $.
Hence, (\ref{A.8.pf.1}) (applied to $\ell=s-\alpha$) yields%
\[
\left(  \mathbf{x}_{s-\left(  s-\alpha\right)  }\left(  Y,x\right)
=\mathbf{x}_{s-\left(  s-\alpha\right)  }\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  \ \ \ \ \ \ \ \ \ \ \text{and}%
\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{s-\left(s-\alpha\right)}\left(  Y,x\right)  =\mathbf{r}%
_{s-\left(s-\alpha\right)}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  \right)
.
\]
Since $s-\left(  s-\alpha\right)  =\alpha$, this rewrites as follows:%
\[
\left(  \mathbf{x}_{\alpha}\left(  Y,x\right)  =\mathbf{x}_{\alpha}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{\alpha}\left(
Y,x\right)  =\mathbf{r}_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \right)  .
\]
Thus, the relation $\mathbf{x}_{\alpha}\left(  Y,x\right)  =\mathbf{x}%
_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  $ is
proven in Case 1.
\par
Now, let us consider Case 2. In this case, $\alpha=s+1$, so that the relation
$\mathbf{x}_{\alpha}\left(  Y,x\right)  =\mathbf{x}_{\alpha}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  $ directly follows from
(\ref{A.8.pf.0}).
\par
Thus, the relation $\mathbf{x}_{\alpha}\left(  Y,x\right)  =\mathbf{x}%
_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  $ is
proven in both cases 1 and 2. This completes the proof of $\mathbf{x}_{\alpha
}\left(  Y,x\right)  =\mathbf{x}_{\alpha}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  $.} Since $s=\mathbf{s}\left(  Y,x\right)  $ and
$t=\mathbf{t}\left(  Y,x\right)  $, this rewrites as follows: For every
$\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  +1\right\}  $, we
have $\mathbf{x}_{\alpha}\left(  Y,x\right)  =\mathbf{x}_{\alpha}\left(
\operatorname*{ins}\left(  Y,x\right)  ,\mathbf{s}\left(  Y,x\right)
,\mathbf{t}\left(  Y,x\right)  \right)  $. This proves Proposition A.8
\textbf{(c)}.

It is also easy to see that for every $\alpha\in\left\{  1,2,...,s\right\}  $,
we have $\mathbf{r}_{\alpha}\left(  Y,x\right)  =\mathbf{r}_{\alpha}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  $%
.\ \ \ \ \footnote{\textit{Proof.} Let $\alpha\in\left\{  1,2,...,s\right\}
$. Then, $s-\alpha\in\left\{  0,1,...,s-1\right\}  $. Hence, (\ref{A.8.pf.1})
(applied to $\ell=s-\alpha$) yields%
\[
\left(  \mathbf{x}_{s-\left(  s-\alpha\right)  }\left(  Y,x\right)
=\mathbf{x}_{s-\left(  s-\alpha\right)  }\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  \ \ \ \ \ \ \ \ \ \ \text{and}%
\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{s-\left(s-\alpha\right)}\left(  Y,x\right)  =\mathbf{r}%
_{s-\left(s-\alpha\right)}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  \right)
.
\]
Since $s-\left(  s-\alpha\right)  =\alpha$, this rewrites as follows:%
\[
\left(  \mathbf{x}_{\alpha}\left(  Y,x\right)  =\mathbf{x}_{\alpha}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \mathbf{r}_{\alpha}\left(
Y,x\right)  =\mathbf{r}_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \right)  .
\]
Thus, the relation $\mathbf{r}_{\alpha}\left(  Y,x\right)  =\mathbf{r}%
_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  $ is
proven.} Since $s=\mathbf{s}\left(  Y,x\right)  $ and $t=\mathbf{t}\left(
Y,x\right)  $, this rewrites as follows: For every $\alpha\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $, we have $\mathbf{r}%
_{\alpha}\left(  Y,x\right)  =\mathbf{r}_{\alpha}\left(  \operatorname*{ins}%
\left(  Y,x\right)  ,\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(
Y,x\right)  \right)  $. This proves Proposition A.8 \textbf{(d)}.

Now we will prove Proposition A.8 \textbf{(b)}. In order to do this, let
$\left(  \alpha,\beta\right)  \in\mathbb{N}^{2}$ be arbitrary. We are going to
prove that $\left(  \operatorname*{del}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  \right)  _{\alpha,\beta}=Y_{\alpha,\beta}$.

Note that whenever $\alpha\in\left\{  1,2,...,s\right\}  $, we have%
\begin{align}
\mathbf{r}_{\alpha}\left(  Y,x\right)   &  =\mathbf{r}_{\alpha}\left(
\operatorname*{ins}\left(  Y,x\right)  ,\underbrace{\mathbf{s}\left(
Y,x\right)  }_{=s},\underbrace{\mathbf{t}\left(  Y,x\right)  }_{=t}\right)
\nonumber\\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{by Proposition A.8 \textbf{(d)}}\\
\text{(since }\alpha\in\left\{  1,2,...,s\right\}  =\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  \text{ (because }%
s=\mathbf{s}\left(  Y,x\right)  \text{))}%
\end{array}
\right) \nonumber\\
&  =\mathbf{r}_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  . \label{A.8.pf.7}%
\end{align}
But let us not require $\alpha\in\left\{  1,2,...,s\right\}  $ at the moment.

Now, we distinguish between two cases:

\textit{Case 1:} We have $\left(  \alpha\in\left\{  1,2,...,s\right\}  \text{
and }\beta=\mathbf{r}_{\alpha}\left(  Y,x\right)  \right)  $.

\textit{Case 2:} We do not have $\left(  \alpha\in\left\{  1,2,...,s\right\}
\text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,x\right)  \right)  $.

Let us first consider Case 1. Then, $\left(  \alpha\in\left\{
1,2,...,s\right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,x\right)
\right)  $. We have $\alpha\in\left\{  1,2,...,s\right\}  =\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $ (since $s=\mathbf{s}\left(
Y,x\right)  $) and thus $\alpha+1\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  +1\right\}  $. Since $\beta=\mathbf{r}_{\alpha}\left(  Y,x\right)
=\mathbf{r}_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  $ (by (\ref{A.8.pf.7})), we have
\begin{align*}
&  \left(  \operatorname*{del}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \right)  _{\alpha,\beta}\\
&  =\left(  \operatorname*{del}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \right)  _{\alpha,\mathbf{r}_{\alpha}\left(  \operatorname*{ins}%
\left(  Y,x\right)  ,s,t\right)  }=\mathbf{x}_{\alpha+1}\left(
\operatorname*{ins}\left(  Y,x\right)  ,\underbrace{s}_{=\mathbf{s}\left(
Y,x\right)  },\underbrace{t}_{=\mathbf{t}\left(  Y,x\right)  }\right) \\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{because Proposition A.7 \textbf{(d)} (applied to }\operatorname*{ins}%
\left(  Y,x\right)  \text{ instead of }Y\text{)}\\
\text{yields }\mathbf{x}_{\alpha+1}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  =\left(  \operatorname*{del}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  \right)  _{\alpha
,\mathbf{r}_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  }%
\end{array}
\right) \\
&  =\mathbf{x}_{\alpha+1}\left(  \operatorname*{ins}\left(  Y,x\right)
,\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  \right)
=\mathbf{x}_{\alpha+1}\left(  Y,x\right) \\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since Proposition A.8 \textbf{(c)} (applied to }\alpha+1\text{ instead
of }\alpha\text{) yields}\\
\text{ }\mathbf{x}_{\alpha+1}\left(  Y,x\right)  =\mathbf{x}_{\alpha+1}\left(
\operatorname*{ins}\left(  Y,x\right)  ,\mathbf{s}\left(  Y,x\right)
,\mathbf{t}\left(  Y,x\right)  \right)  \text{ (since }\alpha+1\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  +1\right\}  \text{)}%
\end{array}
\right) \\
&  =Y_{\alpha,\mathbf{r}_{\alpha}\left(  Y,x\right)  }%
\ \ \ \ \ \ \ \ \ \ \left(  \text{by Proposition A.4 \textbf{(d)}, since
}\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  \right) \\
&  =Y_{\alpha,\beta}\ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{r}%
_{\alpha}\left(  Y,x\right)  =\beta\right)  .
\end{align*}
Thus, we have shown that $\left(  \operatorname*{del}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  \right)  _{\alpha,\beta
}=Y_{\alpha,\beta}$ in Case 1.

Now let us consider Case 2. In this case, we do not have $\left(  \alpha
\in\left\{  1,2,...,s\right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(
Y,x\right)  \right)  $. Since we have $\mathbf{r}_{\alpha}\left(  Y,x\right)
=\mathbf{r}_{\alpha}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  $ whenever $\alpha\in\left\{  1,2,...,s\right\}  $ (due to
(\ref{A.8.pf.7})), this rewrites as follows: We do not have $\left(  \alpha
\in\left\{  1,2,...,s\right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  \right)  $. Hence,
$\left(  \operatorname*{del}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \right)  _{\alpha,\beta}=\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{\alpha,\beta}$ (because Proposition A.7 \textbf{(f)}
(applied to $\operatorname*{ins}\left(  Y,x\right)  $ instead of $Y$) yields
that $\left(  \operatorname*{del}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  \right)  _{\alpha,\beta}=\left(  \operatorname*{ins}%
\left(  Y,x\right)  \right)  _{\alpha,\beta}$ unless $\left(  \alpha
\in\left\{  1,2,...,s\right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  \right)  $).

On the other hand, recall that we do not have $\left(  \alpha\in\left\{
1,2,...,s\right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,x\right)
\right)  $. Since $\mathbf{s}\left(  Y,x\right)  =s$, this rewrites as
follows: We do not have $\left(  \alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y,x\right)  \right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,x\right)
\right)  $. Hence, $\left(  \operatorname*{ins}\left(  Y,x\right)  \right)
_{\alpha,\beta}=Y_{\alpha,\beta}$ (by Proposition A.4 \textbf{(f)}). Thus,
$\left(  \operatorname*{del}\left(  \operatorname*{ins}\left(  Y,x\right)
,s,t\right)  \right)  _{\alpha,\beta}=\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{\alpha,\beta}=Y_{\alpha,\beta}$. Thus, we have shown
that $\left(  \operatorname*{del}\left(  \operatorname*{ins}\left(
Y,x\right)  ,s,t\right)  \right)  _{\alpha,\beta}=Y_{\alpha,\beta}$ in Case 2.

Hence, in both possible cases 1 and 2, we have proven that $\left(
\operatorname*{del}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\right)  _{\alpha,\beta}=Y_{\alpha,\beta}$. As a consequence, $\left(
\operatorname*{del}\left(  \operatorname*{ins}\left(  Y,x\right)  ,s,t\right)
\right)  _{\alpha,\beta}=Y_{\alpha,\beta}$ is shown for all $\left(
\alpha,\beta\right)  \in\mathbb{N}^{2}$. Thus, $\operatorname*{del}\left(
\operatorname*{ins}\left(  Y,x\right)  ,s,t\right)  =Y$. Since $s=\mathbf{s}%
\left(  Y,x\right)  $ and $t=\mathbf{t}\left(  Y,x\right)  $, this rewrites as
$\operatorname*{del}\left(  \operatorname*{ins}\left(  Y,x\right)
,\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  \right)  =Y$.
This proves Proposition A.8 \textbf{(b)}.

Now it only remains to prove Proposition A.8 \textbf{(e)}. This is easy now:
We have%
\begin{align*}
\mathbf{x}\left(  \operatorname*{ins}\left(  Y,x\right)
,\underbrace{\mathbf{s}\left(  Y,x\right)  }_{=s},\underbrace{\mathbf{t}%
\left(  Y,x\right)  }_{=t}\right)   &  =\mathbf{x}\left(  \operatorname*{ins}%
\left(  Y,x\right)  ,s,t\right)  =\mathbf{x}_{1}\left(  \operatorname*{ins}%
\left(  Y,x\right)  ,\underbrace{s}_{=\mathbf{s}\left(  Y,x\right)
},\underbrace{t}_{=\mathbf{t}\left(  Y,x\right)  }\right) \\
&  \ \ \ \ \ \ \ \ \ \ \left(  \text{by Proposition A.7 \textbf{(g)}, applied
to }\operatorname*{ins}\left(  Y,x\right)  \text{ instead of }Y\right) \\
&  =\mathbf{x}_{1}\left(  \operatorname*{ins}\left(  Y,x\right)
,\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(  Y,x\right)  \right) \\
&  =\mathbf{x}_{1}\left(  Y,x\right)  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since Proposition A.8 \textbf{(c)} (applied to }\alpha=1\text{)
yields}\\
\mathbf{x}_{1}\left(  Y,x\right)  =\mathbf{x}_{1}\left(  \operatorname*{ins}%
\left(  Y,x\right)  ,\mathbf{s}\left(  Y,x\right)  ,\mathbf{t}\left(
Y,x\right)  \right)
\end{array}
\right) \\
&  =x\ \ \ \ \ \ \ \ \ \ \left(  \text{by Proposition A.4 \textbf{(a)}%
}\right)  ,
\end{align*}
so that Proposition A.8 \textbf{(e)} is proven.

Next we will show an analogue of Proposition A.8 for the composition of first
$\operatorname*{DELETE}$ and then $\operatorname*{INSERT}$:

\begin{quote}
\textbf{Proposition A.9.} Let $Y$ be a GYT, and $s$ and $t$ be two nonnegative
integers satisfying $s\geq1$, $t\geq1$, $Y_{s,t}\neq\infty$ and $Y_{s,\left(
t+1\right)  }=Y_{\left(  s+1\right)  ,t}=\infty$.

\textbf{(a)} The family $\operatorname*{del}\left(  Y,s,t\right)  $ is a GYT,
and $\mathbf{x}\left(  Y,s,t\right)  $ is a positive integer. Thus, the
algorithm $\operatorname*{INSERT}\left(  \mathbf{x}\left(  Y,s,t\right)
\right)  $ can be applied to the GYT $\operatorname*{del}\left(  Y,s,t\right)
$.

\textbf{(b)} We have $\operatorname*{ins}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)  \right)  =Y$.

\textbf{(c)} For every $\alpha\in\left\{  1,2,...,s+1\right\}  $, the term
$\mathbf{x}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,\mathbf{x}\left(  Y,s,t\right)  \right)  $ is well-defined and satisfies
$\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =\mathbf{x}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)
\right)  $.

\textbf{(d)} For every $\alpha\in\left\{  1,2,...,s\right\}  $, the term
$\mathbf{r}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,\mathbf{x}\left(  Y,s,t\right)  \right)  $ is well-defined and satisfies
$\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)
\right)  $.

\textbf{(e)} We have $\mathbf{s}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)  \right)  =s$ and $\mathbf{t}%
\left(  \operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(
Y,s,t\right)  \right)  =t$.
\end{quote}

Note that Proposition A.9 is what Knuth laconically puts in words as follows:
"Conversely, if we start with any generalized Young tableau, $Y$, and if we
choose two integers $\left(  s,t\right)  $ such that (2.4) holds, the
procedure $\operatorname*{DELETE}\left(  s,t\right)  $ will specify some
positive integer $x$ in step D5, and $x$ is removed from the tableau; the
subsequent operation $\operatorname*{INSERT}\left(  x\right)  $ will put $x$
back again, recompute $s$ and $t$, and restore $Y$ to its original form."

Before we prove this proposition (the proof is mostly analogous to that of
Proposition A.8), let us point out what Proposition A.9 intuitively means:
Proposition A.9 \textbf{(a)} shows that, after we have applied
$\operatorname*{DELETE}\left(  s,t\right)  $ to a GYT $Y$, we can then apply
$\operatorname*{INSERT}\left(  x\right)  $ to the resulting GYT, where $x$ is
the number computed by $\operatorname*{DELETE}\left(  s,t\right)  $ (we have
denoted this number by $\mathbf{x}\left(  Y,s,t\right)  $). Proposition A.9
\textbf{(b)} and \textbf{(e)} show that this application of
$\operatorname*{INSERT}\left(  x\right)  $ gives us our GYT $Y$ and our
numbers $s$ and $t$ back. Proposition A.9 \textbf{(c)} shows that it
recomputes the sequence $\left(  x_{1},x_{2},...,x_{s+1}\right)  $ which was
already constructed by $\operatorname*{DELETE}\left(  s,t\right)  $.
Proposition A.9 \textbf{(d)} shows that it recomputes the sequence $\left(
r_{1},r_{2},...,r_{s}\right)  $ which was already constructed by
$\operatorname*{DELETE}\left(  s,t\right)  $.

So let us now prove Proposition A.9.

\textit{Proof of Proposition A.9.} We know that $\operatorname*{del}\left(
Y,s,t\right)  $ is a GYT. Also, from Proposition A.7 \textbf{(h)}, we know
that $\mathbf{x}\left(  Y,s,t\right)  $ is a positive integer. Hence, the
algorithm $\operatorname*{INSERT}\left(  \mathbf{x}\left(  Y,s,t\right)
\right)  $ can be applied to the GYT $\operatorname*{del}\left(  Y,s,t\right)
$. This proves Proposition A.9 \textbf{(a)}.

Let now $x=\mathbf{x}\left(  Y,s,t\right)  $. Then, $x$ is a positive integer
(since $\mathbf{x}\left(  Y,s,t\right)  $ is a positive integer). Thus, we can
apply Proposition A.4 to $\operatorname*{del}\left(  Y,s,t\right)  $ instead
of $Y$.

Now let us prove Proposition A.9 \textbf{(c)} and \textbf{(d)}. First of all,
$x=\mathbf{x}\left(  Y,s,t\right)  =\mathbf{x}_{1}\left(  Y,s,t\right)  $ (by
Proposition A.7 \textbf{(g)}) and $\mathbf{x}_{1}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  =x$ (by Proposition A.4 \textbf{(a)}, applied
to $\operatorname*{del}\left(  Y,s,t\right)  $ instead of $Y$). Thus,%
\begin{equation}
\mathbf{x}_{1}\left(  Y,s,t\right)  =x=\mathbf{x}_{1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  . \label{A.9.pf.1}%
\end{equation}


Also, Proposition A.4 \textbf{(b)} (applied to $\operatorname*{del}\left(
Y,s,t\right)  $ and $1$ instead of $Y$ and $\alpha$) yields that the number
$\mathbf{r}_{1}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $
is the smallest $p\in\mathbb{N}$ such that $\mathbf{x}_{1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  <\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{1,p}$.

On the other hand, Proposition A.7 \textbf{(b)} (applied to $\alpha=1$) yields
that the number $\mathbf{r}_{1}\left(  Y,s,t\right)  $ is the smallest
$p\in\mathbb{N}$ such that $\mathbf{x}_{1}\left(  Y,s,t\right)  <\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{1,p}$.

Hence,%
\begin{align}
\mathbf{r}_{1}\left(  Y,s,t\right)   &  =\left(  \text{the smallest }%
p\in\mathbb{N}\text{ such that }\underbrace{\mathbf{x}_{1}\left(
Y,s,t\right)  }_{\substack{=\mathbf{x}_{1}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  \\\text{(by (\ref{A.9.pf.1}))}}}<\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{1,p}\right) \nonumber\\
&  =\left(  \text{the smallest }p\in\mathbb{N}\text{ such that }\mathbf{x}%
_{1}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  <\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{1,p}\right) \nonumber\\
&  =\mathbf{r}_{1}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
. \label{A.9.pf.2}%
\end{align}


We are next going to prove that every $\ell\in\left\{  1,2,...,s\right\}  $
satisfies%
\begin{equation}
\left(
\begin{array}
[c]{c}%
\ell\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
;\\
\mathbf{x}_{\ell}\left(  Y,s,t\right)  =\mathbf{x}_{\ell}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{r}_{\ell}\left(  Y,s,t\right)  =\mathbf{r}_{\ell}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\end{array}
\right)  . \label{A.9.pf.3}%
\end{equation}
(Note that the relation (\ref{A.9.pf.3}) is to be understood as implicitly
claiming that the terms $\mathbf{x}_{\ell}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $ and $\mathbf{r}_{\ell}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  $ are well-defined.)

\textit{Proof of (\ref{A.9.pf.3}).} We will prove (\ref{A.9.pf.3}) by
induction over $\ell$:

\textit{Induction base:} Clearly, $1\leq\mathbf{s}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  $ (because Proposition A.4 \textbf{(g)}
(applied to $\operatorname*{del}\left(  Y,s,t\right)  $ instead of $Y$) yields
that $\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\geq1$). Also, due to (\ref{A.9.pf.1}) and (\ref{A.9.pf.2}), we have
$\mathbf{x}_{1}\left(  Y,s,t\right)  =\mathbf{x}_{1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ and $\mathbf{r}%
_{1}\left(  Y,s,t\right)  =\mathbf{r}_{1}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $. Altogether, we have thus shown that%
\[
\left(
\begin{array}
[c]{c}%
1\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{x}_{1}\left(  Y,s,t\right)  =\mathbf{x}_{1}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{r}_{1}\left(  Y,s,t\right)  =\mathbf{r}_{1}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)
\end{array}
\right)  .
\]
In other words, (\ref{A.9.pf.3}) holds for $\ell=1$. This completes the
induction base.

\textit{Induction step:} Let $\lambda\in\left\{  2,3,...,s\right\}  $ be
arbitrary. Assume that (\ref{A.9.pf.3}) holds for $\ell=\lambda-1$. We must
now prove that (\ref{A.9.pf.3}) holds for $\ell=\lambda$.

Since $\lambda\in\left\{  2,3,...,s\right\}  $, we have $\lambda-1\in\left\{
1,2,...,s\right\}  $.

Since (\ref{A.9.pf.3}) holds for $\ell=\lambda-1$, we have%
\begin{equation}
\left(
\begin{array}
[c]{c}%
\lambda-1\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  ;\\
\mathbf{x}_{\lambda-1}\left(  Y,s,t\right)  =\mathbf{x}_{\lambda-1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{r}_{\lambda-1}\left(  Y,s,t\right)  =\mathbf{r}_{\lambda-1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\end{array}
\right)  . \label{A.9.pf.4}%
\end{equation}


Since $\lambda-1\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  $, we have $\lambda-1\in\left\{  1,2,...,\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  \right\}  $. Hence, we can
apply Proposition A.4 \textbf{(d)} to $\operatorname*{del}\left(
Y,s,t\right)  $ and $\lambda-1$ instead of $Y$ and $\alpha$. This yields that
$\mathbf{x}_{\left(  \lambda-1\right)  +1}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  =\left(  \operatorname*{del}\left(  Y,s,t\right)
\right)  _{\left(  \lambda-1\right)  ,\mathbf{r}_{\lambda-1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  }$. Since $\left(
\lambda-1\right)  +1=\lambda$, this rewrites as%
\begin{align*}
\mathbf{x}_{\lambda}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)   &  =\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)
_{\left(  \lambda-1\right)  ,\mathbf{r}_{\lambda-1}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  }\\
&  =\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{\left(
\lambda-1\right)  ,\mathbf{r}_{\lambda-1}\left(  Y,s,t\right)  }%
\ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{r}_{\lambda-1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,s,t\right)  =\mathbf{r}_{\lambda
-1}\left(  Y,s,t\right)  \text{ by (\ref{A.9.pf.4})}\right) \\
&  =\mathbf{x}_{\left(  \lambda-1\right)  +1}\left(  Y,s,t\right) \\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since Proposition A.7 \textbf{(d)} (applied to }\alpha=\lambda-1\text{)
yields}\\
\mathbf{x}_{\left(  \lambda-1\right)  +1}\left(  Y,s,t\right)  =\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{\left(  \lambda-1\right)
,\mathbf{r}_{\lambda-1}\left(  Y,s,t\right)  }\text{ (since }\lambda
-1\in\left\{  1,2,...,s\right\}  \text{)}%
\end{array}
\right) \\
&  =\mathbf{x}_{\lambda}\left(  Y,s,t\right)  \ \ \ \ \ \ \ \ \ \ \left(
\text{since }\left(  \lambda-1\right)  +1=\lambda\right)  ,
\end{align*}
so that%
\begin{equation}
\mathbf{x}_{\lambda}\left(  Y,s,t\right)  =\mathbf{x}_{\lambda}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  . \label{A.9.pf.5}%
\end{equation}
Thus, we have proven a part of (\ref{A.9.pf.3}) for $\ell=\lambda$, but we
have two more to go.

Proposition A.7 \textbf{(i)} (applied to $\alpha=\lambda$) yields that
$\mathbf{x}_{\lambda}\left(  Y,s,t\right)  $ is a positive integer. Hence,
$\mathbf{x}_{\lambda}\left(  Y,s,t\right)  \neq\infty$.

Proposition A.4 \textbf{(i)} (applied to $\operatorname*{del}\left(
Y,s,t\right)  $ instead of $Y$) yields that $\mathbf{x}_{\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  +1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  =\infty$. Thus,%
\[
\mathbf{x}_{\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  +1}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
=\infty\neq\mathbf{x}_{\lambda}\left(  Y,s,t\right)  =\mathbf{x}_{\lambda
}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\]
(by (\ref{A.9.pf.5})), so that $\mathbf{s}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  +1\neq\lambda$. Thus, $\lambda-1\neq\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $. Combined with
$\lambda-1\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  $, this yields $\lambda-1\leq\mathbf{s}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  -1$ (since $\lambda-1$ and $\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ are integers), so that%
\begin{equation}
\lambda\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  . \label{A.9.pf.6}%
\end{equation}
Thus, one more part of (\ref{A.9.pf.3}) is proven for $\ell=\lambda$. Now to
the last one:

Since $\lambda\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  $, we have $\lambda\in\left\{  1,2,...,\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  \right\}  $. Hence,
Proposition A.4 \textbf{(b)} (applied to $\operatorname*{del}\left(
Y,s,t\right)  $ and $\lambda$ instead of $Y$ and $\alpha$) yields that the
number $\mathbf{r}_{\lambda}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  $ is the smallest $p\in\mathbb{N}$ such that $\mathbf{x}_{\lambda
}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  <\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{\lambda,p}$.

On the other hand, Proposition A.7 \textbf{(b)} (applied to $\alpha=\lambda$)
yields that the number $\mathbf{r}_{\lambda}\left(  Y,s,t\right)  $ is the
smallest $p\in\mathbb{N}$ such that $\mathbf{x}_{\lambda}\left(  Y,s,t\right)
<\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{\lambda,p}$.
Hence,%
\begin{align}
\mathbf{r}_{\lambda}\left(  Y,s,t\right)   &  =\left(  \text{the smallest
}p\in\mathbb{N}\text{ such that }\underbrace{\mathbf{x}_{\lambda}\left(
Y,s,t\right)  }_{\substack{=\mathbf{x}_{\lambda}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  \\\text{(by (\ref{A.9.pf.5}))}}}<\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{\lambda,p}\right)
\nonumber\\
&  =\left(  \text{the smallest }p\in\mathbb{N}\text{ such that }%
\mathbf{x}_{\lambda}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  <\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)
_{\lambda,p}\right) \nonumber\\
&  =\mathbf{r}_{\lambda}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  . \label{A.9.pf.7}%
\end{align}


Combining (\ref{A.9.pf.6}), (\ref{A.9.pf.5}) and (\ref{A.9.pf.7}), we get%
\[
\left(
\begin{array}
[c]{c}%
\lambda\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  ;\\
\mathbf{x}_{\lambda}\left(  Y,s,t\right)  =\mathbf{x}_{\lambda}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{r}_{\lambda}\left(  Y,s,t\right)  =\mathbf{r}_{\lambda}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\end{array}
\right)  .
\]
Thus, (\ref{A.9.pf.3}) holds for $\ell=\lambda$. This completes the induction
step. Thus, the induction proof of (\ref{A.9.pf.3}) is complete.

One consequence of (\ref{A.9.pf.3}) is that $s\leq\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $%
\ \ \ \ \footnote{\textit{Proof.} We have $s\in\left\{  1,2,...,s\right\}  $,
so that (\ref{A.9.pf.3}) (applied to $\ell=s$) yields%
\[
\left(
\begin{array}
[c]{c}%
s\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{x}_{s}\left(  Y,s,t\right)  =\mathbf{x}_{s}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{r}_{s}\left(  Y,s,t\right)  =\mathbf{r}_{s}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)
\end{array}
\right)  .
\]
In particular, $s\leq\mathbf{s}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $, qed.}.

Now, it is easy to see that for every $\alpha\in\left\{  1,2,...,s+1\right\}
$, the term $\mathbf{x}_{\alpha}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $ is well-defined and satisfies $\mathbf{x}_{\alpha
}\left(  Y,s,t\right)  =\mathbf{x}_{\alpha}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $.\ \ \ \ \footnote{\textit{Proof.} Let $\alpha
\in\left\{  1,2,...,s+1\right\}  $. Then, we must be in one of the following
two cases:
\par
\textit{Case 1:} We have $\alpha\in\left\{  1,2,...,s\right\}  $.
\par
\textit{Case 2:} We have $\alpha=s+1$.
\par
First let us consider Case 1. In this case, $\alpha\in\left\{
1,2,...,s\right\}  $, so that (\ref{A.9.pf.3}) (applied to $\ell=\alpha$)
yields%
\[
\left(
\begin{array}
[c]{c}%
\alpha\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  ;\\
\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =\mathbf{x}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\end{array}
\right)  .
\]
In particular, this says that the term $\mathbf{x}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ is well-defined. Thus,
in Case 1, we have proved that the term $\mathbf{x}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ is well-defined and
satisfies $\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =\mathbf{x}_{\alpha
}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $.
\par
Now, let us consider Case 2. In this case, $\alpha=s+1$. From (\ref{A.9.pf.3})
(applied to $\ell=s$), we have%
\[
\left(
\begin{array}
[c]{c}%
s\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{x}_{s}\left(  Y,s,t\right)  =\mathbf{x}_{s}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{r}_{s}\left(  Y,s,t\right)  =\mathbf{r}_{s}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)
\end{array}
\right)  .
\]
Since $s\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  $, we have $s+1\leq\mathbf{s}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  +1$, so that $s+1\in\left\{  1,2,...,\mathbf{s}%
\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  +1\right\}  $, and
thus the term $\mathbf{x}_{s+1}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $ is well-defined. Also, from $s\leq\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $, we get $s\in\left\{
1,2,...,\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\right\}  $. Hence, we can apply Proposition A.4 \textbf{(d)} to
$\operatorname*{del}\left(  Y,s,t\right)  $ and $s$ instead of $Y$ and
$\alpha$. This yields that%
\begin{align*}
\mathbf{x}_{s+1}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
&  =\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{s,\mathbf{r}%
_{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  }\\
&  =\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{s,\mathbf{r}%
_{s}\left(  Y,s,t\right)  }\ \ \ \ \ \ \ \ \ \ \left(  \text{since }%
\mathbf{r}_{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
=\mathbf{r}_{s}\left(  Y,s,t\right)  \right) \\
&  =\mathbf{x}_{s+1}\left(  Y,s,t\right)  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since Proposition A.7 \textbf{(d)} (applied to }\alpha=s\text{)}\\
\text{yields }\mathbf{x}_{s+1}\left(  Y,s,t\right)  =\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{s,\mathbf{r}_{s}\left(
Y,s,t\right)  }%
\end{array}
\right)  .
\end{align*}
We have thus proven that the term $\mathbf{x}_{s+1}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  $ is well-defined and satisfies
$\mathbf{x}_{s+1}\left(  Y,s,t\right)  =\mathbf{x}_{s+1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $. Since $s+1=\alpha$,
this rewrites as follows: The term $\mathbf{x}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ is well-defined and
satisfies $\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =\mathbf{x}_{\alpha
}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $. We have thus
proven in Case 2 that the term $\mathbf{x}_{\alpha}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  $ is well-defined and satisfies
$\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =\mathbf{x}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $.
\par
Thus, in each of the cases 1 and 2, we have shown that the term $\mathbf{x}%
_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ is
well-defined and satisfies $\mathbf{x}_{\alpha}\left(  Y,s,t\right)
=\mathbf{x}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  $. This completes the proof that the term $\mathbf{x}_{\alpha
}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ is well-defined
and satisfies $\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =\mathbf{x}_{\alpha
}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $.} Since
$x=\mathbf{x}\left(  Y,s,t\right)  $, this rewrites as follows: For every
$\alpha\in\left\{  1,2,...,s+1\right\}  $, the term $\mathbf{x}_{\alpha
}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(
Y,s,t\right)  \right)  $ is well-defined and satisfies $\mathbf{x}_{\alpha
}\left(  Y,s,t\right)  =\mathbf{x}_{\alpha}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)  \right)  $. This proves
Proposition A.9 \textbf{(c)}.

It is also easy to see that for every $\alpha\in\left\{  1,2,...,s\right\}  $,
the term $\mathbf{r}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  $ is well-defined and satisfies $\mathbf{r}_{\alpha}\left(
Y,s,t\right)  =\mathbf{r}_{\alpha}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $.\ \ \ \ \footnote{\textit{Proof.} Let $\alpha
\in\left\{  1,2,...,s\right\}  $. Then, (\ref{A.9.pf.3}) (applied to
$\ell=\alpha$) yields%
\[
\left(
\begin{array}
[c]{c}%
\alpha\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  ;\\
\mathbf{x}_{\alpha}\left(  Y,s,t\right)  =\mathbf{x}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  ;\\
\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\end{array}
\right)  .
\]
In particular, this says that the term $\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ is well-defined. Thus,
we have proved that the term $\mathbf{r}_{\alpha}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  $ is well-defined and satisfies
$\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $.} Since $x=\mathbf{x}%
\left(  Y,s,t\right)  $, this rewrites as follows: For every $\alpha
\in\left\{  1,2,...,s\right\}  $, the term $\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)
\right)  $ is well-defined and satisfies $\mathbf{r}_{\alpha}\left(
Y,s,t\right)  =\mathbf{r}_{\alpha}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)  \right)  $. This proves
Proposition A.9 \textbf{(d)}.

Let us now prove Proposition A.9 \textbf{(e)}.

First of all, it is easy to show that $s=\mathbf{s}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  $.\ \ \ \ \footnote{\textit{Proof.} Assume
the opposite. Then, $s<\mathbf{s}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $, so that $s+1\leq\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ (since $s$ and
$\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ are
integers). Hence, $s+1\in\left\{  1,2,...,\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  \right\}  $.
\par
By Proposition A.4 \textbf{(j)} (applied to $\operatorname*{del}\left(
Y,s,t\right)  $ instead of $Y$), the numbers $\mathbf{x}_{1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $, $\mathbf{x}_{2}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $, $...$, $\mathbf{x}%
_{\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ are positive
integers (i. e., none of them is $\infty$) and satisfy $\mathbf{x}_{1}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  <\mathbf{x}_{2}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  <...<\mathbf{x}%
_{\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $.
\par
So we know that the numbers $\mathbf{x}_{1}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $, $\mathbf{x}_{2}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $, $...$, $\mathbf{x}_{\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  }\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ are positive integers.
We can rewrite this as follows: For every $\alpha\in\left\{
1,2,...,\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\right\}  $, the number $\mathbf{x}_{\alpha}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $ is a positive integer. Applied to $\alpha=s+1$,
this yields that $\mathbf{x}_{s+1}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $ is a positive integer (since $s+1\in\left\{
1,2,...,\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\right\}  $). Thus, $\mathbf{x}_{s+1}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  \neq\infty$.
\par
Since $s\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  $, we have $s\in\left\{  1,2,...,\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  \right\}  $, so that we
can apply Proposition A.4 \textbf{(d)} to $\operatorname*{del}\left(
Y,s,t\right)  $ and $s$ instead of $Y$ and $\alpha$. This yields that
\begin{align*}
\mathbf{x}_{s+1}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
&  =\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)  _{s,\mathbf{r}%
_{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  }=\left(
\operatorname*{del}\left(  Y,s,t\right)  \right)  _{s,\mathbf{r}_{s}\left(
Y,s,t\right)  }\\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since }\mathbf{r}_{s}\left(  Y,s,t\right)  =\mathbf{r}_{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,s,t\right)  \text{ by Proposition
A.9 \textbf{(d)}}\\
\text{(applied to }s\text{ instead of }\alpha\text{), so that }\mathbf{r}%
_{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,s,t\right)
=\mathbf{r}_{s}\left(  Y,s,t\right)
\end{array}
\right) \\
&  =\mathbf{x}_{s+1}\left(  Y,s,t\right) \\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since Proposition A.7 \textbf{(d)} (applied to }\alpha=s\text{)
yields}\\
\mathbf{x}_{s+1}\left(  Y,s,t\right)  =\left(  \operatorname*{del}\left(
Y,s,t\right)  \right)  _{s,\mathbf{r}_{s}\left(  Y,s,t\right)  }\text{ (since
}s\in\left\{  1,2,...,s\right\}  \text{)}%
\end{array}
\right) \\
&  =\infty\ \ \ \ \ \ \ \ \ \ \left(  \text{by Proposition A.7 \textbf{(a)}%
}\right)  ,
\end{align*}
contradicting $\mathbf{x}_{s+1}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  \neq\infty$. This contradiction shows that our
assumption $s<\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  $ was wrong. Hence, we cannot have $s<\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $. But since we have
$s\leq\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $,
we therefore conclude that $s=\mathbf{s}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $, qed.} Since $x=\mathbf{x}\left(  Y,s,t\right)  $,
this rewrites as $s=\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,\mathbf{x}\left(  Y,s,t\right)  \right)  $.

As a consequence of this, we can easily obtain $t=\mathbf{t}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $%
\ \ \ \ \footnote{\textit{Proof.} By Proposition A.4 \textbf{(h)} (applied to
$\operatorname*{del}\left(  Y,s,t\right)  $ instead of $Y$), we have%
\begin{align*}
\mathbf{t}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)   &
=\mathbf{r}_{\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  }\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
=\mathbf{r}_{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,\underbrace{x}_{=\mathbf{x}\left(  Y,s,t\right)  }\right) \\
&  \ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  =s\right) \\
&  =\mathbf{r}_{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,\mathbf{x}\left(  Y,s,t\right)  \right)  =\mathbf{r}_{s}\left(  Y,s,t\right)
\\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since Proposition A.9 \textbf{(d)} (applied to }\alpha=s\text{)}\\
\text{yields }\mathbf{r}_{s}\left(  Y,s,t\right)  =\mathbf{r}_{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)
\right)
\end{array}
\right) \\
&  =t\ \ \ \ \ \ \ \ \ \ \left(  \text{by Proposition A.7 \textbf{(j)}%
}\right)  .
\end{align*}
Since $x=\mathbf{x}\left(  Y,s,t\right)  $, this rewrites as $\mathbf{t}%
\left(  \operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(
Y,s,t\right)  \right)  =t$, qed.}. Since $x=\mathbf{x}\left(  Y,s,t\right)  $,
this rewrites as $t=\mathbf{t}\left(  \operatorname*{del}\left(  Y,s,t\right)
,\mathbf{x}\left(  Y,s,t\right)  \right)  $.

We have thus proven both $\mathbf{s}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)  \right)  =s$ and $\mathbf{t}%
\left(  \operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(
Y,s,t\right)  \right)  =t$. Hence, Proposition A.9 \textbf{(e)} is proven.

It therefore only remains to prove Proposition A.9 \textbf{(b)}. In order to
do this, let $\left(  \alpha,\beta\right)  \in\mathbb{N}^{2}$ be arbitrary. We
are going to prove that $\left(  \operatorname*{ins}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)
\right)  \right)  _{\alpha,\beta}=Y_{\alpha,\beta}$.

Note that whenever $\alpha\in\left\{  1,2,...,s\right\}  $, we have%
\begin{align}
\mathbf{r}_{\alpha}\left(  Y,s,t\right)   &  =\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\underbrace{\mathbf{x}\left(
Y,s,t\right)  }_{=x}\right)  \ \ \ \ \ \ \ \ \ \ \left(  \text{by Proposition
A.9 \textbf{(d)}}\right) \nonumber\\
&  =\mathbf{r}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  . \label{A.9.pf.9}%
\end{align}
But let us not require $\alpha\in\left\{  1,2,...,s\right\}  $ at the moment.

Now, we distinguish between two cases:

\textit{Case 1:} We have $\left(  \alpha\in\left\{  1,2,...,s\right\}  \text{
and }\beta=\mathbf{r}_{\alpha}\left(  Y,s,t\right)  \right)  $.

\textit{Case 2:} We do not have $\left(  \alpha\in\left\{  1,2,...,s\right\}
\text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,s,t\right)  \right)  $.

Let us first consider Case 1. Then, $\left(  \alpha\in\left\{
1,2,...,s\right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,s,t\right)
\right)  $. Since $\alpha\in\left\{  1,2,...,s\right\}  \subseteq\left\{
1,2,...,\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\right\}  $ (because $s\leq\mathbf{s}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  $), we can apply Proposition A.4 \textbf{(e)} to
$\operatorname*{del}\left(  Y,s,t\right)  $ instead of $Y$, and conclude that
$\mathbf{x}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  =\left(  \operatorname*{ins}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  \right)  _{\alpha,\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  }$. Since $\beta
=\mathbf{r}_{\alpha}\left(  Y,s,t\right)  =\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  $ (by (\ref{A.9.pf.9})),
we have
\begin{align*}
\left(  \operatorname*{ins}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  \right)  _{\alpha,\beta}  &  =\left(  \operatorname*{ins}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  \right)  _{\alpha
,\mathbf{r}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  }=\mathbf{x}_{\alpha}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,\underbrace{x}_{=\mathbf{x}\left(  Y,s,t\right)  }\right) \\
&  =\mathbf{x}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,\mathbf{x}\left(  Y,s,t\right)  \right)  =\mathbf{x}_{\alpha}\left(
Y,s,t\right)  \ \ \ \ \ \ \ \ \ \ \left(  \text{by Proposition A.9
\textbf{(c)}}\right) \\
&  =Y_{\alpha,\mathbf{r}_{\alpha}\left(  Y,s,t\right)  }%
\ \ \ \ \ \ \ \ \ \ \left(  \text{by Proposition A.7 \textbf{(e)}}\right) \\
&  =Y_{\alpha,\beta}\ \ \ \ \ \ \ \ \ \ \left(  \text{since }\mathbf{r}%
_{\alpha}\left(  Y,s,t\right)  =\beta\right)  .
\end{align*}
Thus, we have shown that $\left(  \operatorname*{ins}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)
\right)  \right)  _{\alpha,\beta}=Y_{\alpha,\beta}$ in Case 1.

Now let us consider Case 2. In this case, we do not have $\left(  \alpha
\in\left\{  1,2,...,s\right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(
Y,s,t\right)  \right)  $. Since $\mathbf{r}_{\alpha}\left(  Y,s,t\right)
=\mathbf{r}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,\mathbf{x}\left(  Y,s,t\right)  \right)  $ for every $\alpha\in\left\{
1,2,...,s\right\}  $ (by Proposition A.9 \textbf{(d)}), this rewrites as
follows: We do not have $\left(  \alpha\in\left\{  1,2,...,s\right\}  \text{
and }\beta=\mathbf{r}_{\alpha}\left(  \operatorname*{del}\left(  Y,s,t\right)
,\mathbf{x}\left(  Y,s,t\right)  \right)  \right)  $. Since $s=\mathbf{s}%
\left(  \operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(
Y,s,t\right)  \right)  $ (by Proposition A.9 \textbf{(e)}), this rewrites as
follows: We do not have $\left(  \alpha\in\left\{  1,2,...,\mathbf{s}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)
\right)  \right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)
\right)  \right)  $. Since $\mathbf{x}\left(  Y,s,t\right)  =x$, this rewrites
as follows: We do not have \newline$\left(  \alpha\in\left\{
1,2,...,\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(  \operatorname*{del}%
\left(  Y,s,t\right)  ,x\right)  \right)  $. Hence, $\left(
\operatorname*{ins}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\right)  _{\alpha,\beta}=\left(  \operatorname*{del}\left(  Y,s,t\right)
\right)  _{\alpha,\beta}$ (because Proposition A.4 \textbf{(f)} (applied to
$\operatorname*{del}\left(  Y,s,t\right)  $ instead of $Y$) yields that
$\left(  \operatorname*{ins}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  \right)  _{\alpha,\beta}=\left(  \operatorname*{del}\left(
Y,s,t\right)  \right)  _{\alpha,\beta}$ unless \newline$\left(  \alpha
\in\left\{  1,2,...,\mathbf{s}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  \right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  \right)  $).

On the other hand, recall that we do not have $\left(  \alpha\in\left\{
1,2,...,s\right\}  \text{ and }\beta=\mathbf{r}_{\alpha}\left(  Y,s,t\right)
\right)  $. Hence, $\left(  \operatorname*{del}\left(  Y,s,t\right)  \right)
_{\alpha,\beta}=Y_{\alpha,\beta}$ (by Proposition A.7 \textbf{(f)}). Thus,
$\left(  \operatorname*{ins}\left(  \operatorname*{del}\left(  Y,s,t\right)
,x\right)  \right)  _{\alpha,\beta}=\left(  \operatorname*{del}\left(
Y,s,t\right)  \right)  _{\alpha,\beta}=Y_{\alpha,\beta}$. Thus, we have shown
that $\left(  \operatorname*{ins}\left(  \operatorname*{del}\left(
Y,s,t\right)  ,x\right)  \right)  _{\alpha,\beta}=Y_{\alpha,\beta}$ in Case 2.

Hence, in both possible cases 1 and 2, we have proven that $\left(
\operatorname*{ins}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\right)  _{\alpha,\beta}=Y_{\alpha,\beta}$. As a consequence, $\left(
\operatorname*{ins}\left(  \operatorname*{del}\left(  Y,s,t\right)  ,x\right)
\right)  _{\alpha,\beta}=Y_{\alpha,\beta}$ is shown for all $\left(
\alpha,\beta\right)  \in\mathbb{N}^{2}$. Thus, $\operatorname*{ins}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,x\right)  =Y$. Since $x=\mathbf{x}%
\left(  Y,s,t\right)  $, this rewrites as $\operatorname*{ins}\left(
\operatorname*{del}\left(  Y,s,t\right)  ,\mathbf{x}\left(  Y,s,t\right)
\right)  =Y$. This proves Proposition A.9 \textbf{(b)}.

\rule{17cm}{0.3mm}

\textbf{Page 714:} I find the proof of Theorem 1 given here somewhat
confusingly written (mainly because it refers to the values of several
variables during the algorithms, only vaguely explaining at what states of the
algorithms these values are being taken). Let me rewrite this proof using
immutable variables.

In the following, I will use Convention A.0, Definition A.1, Convention A.2
and Definition A.3. Let me first reformulate Knuth's Theorem 1 using my notations:

\begin{quote}
\textbf{Theorem B.1.} Let $Y$ be a GYT, and $x$ and $x^{\prime}$ be positive
integers. Let $s=\mathbf{s}\left(  Y,x\right)  $, $t=\mathbf{t}\left(
Y,x\right)  $ and $Y^{\prime}=\operatorname*{ins}\left(  Y,x\right)  $. Let
$s^{\prime}=\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)  $ and $t^{\prime
}=\mathbf{t}\left(  Y^{\prime},x^{\prime}\right)  $. Then, the assertions
$\left(  x\leq x^{\prime}\right)  $, $\left(  s\geq s^{\prime}\right)  $ and
$\left(  t^{\prime}>t\right)  $ are equivalent.
\end{quote}

As I said, Theorem B.1 is exactly the same as Knuth's Theorem 1, but written
down without referring to any mutable variables. Note that this theorem is
nowadays called "row bumping lemma" in literature.

The following proof of Theorem B.1 is almost exactly the same as given by
Knuth, but written using my notations (which are hopefully less ambiguous than Knuth's).

\textit{Proof of Theorem B.1.} Before we prove anything nontrivial, let us
make one obvious remark:%
\begin{equation}
\left(
\begin{array}
[c]{c}%
\text{If }\alpha\text{, }\beta\text{ and }\gamma\text{ are three nonnegative
integers such that}\\
Y_{\alpha,\beta}^{\prime}<_{\infty}Y_{\alpha,\gamma}^{\prime}\text{, then
}\beta<\gamma
\end{array}
\right)  . \label{B.1.pf.0}%
\end{equation}
\footnote{\textit{Proof of (\ref{B.1.pf.0}).} Let $\alpha$, $\beta$ and
$\gamma$ are three nonnegative integers such that $Y_{\alpha,\beta}^{\prime
}<_{\infty}Y_{\alpha,\gamma}^{\prime}$. Then, $\beta<\gamma$ (because
otherwise, we would have $\beta\geq\gamma$, thus $Y_{\alpha,\beta}^{\prime
}\geq Y_{\alpha,\gamma}^{\prime}$ (since $Y^{\prime}$ is a GYT, and thus every
row of $Y^{\prime}$ is weakly increasing), contradicting $Y_{\alpha,\beta
}^{\prime}<_{\infty}Y_{\alpha,\gamma}^{\prime}$). Thus, (\ref{B.1.pf.0}) is
proven.}

\textbf{(a)} We first prove that%
\begin{equation}
\text{if }x\leq x^{\prime}\text{, then }\left(  s\geq s^{\prime}\text{ and
}t^{\prime}>t\right)  . \label{B.1.pf.a}%
\end{equation}


\textit{Proof of (\ref{B.1.pf.a}).} Assume that $x\leq x^{\prime}$. We are
going to prove that every $i\in\left\{  1,2,...,s^{\prime}\right\}  $
satisfies%
\begin{equation}
i\leq s\text{ and }\mathbf{x}_{i}\left(  Y,x\right)  \leq\mathbf{x}_{i}\left(
Y^{\prime},x^{\prime}\right)  \text{.} \label{B.1.pf.a.1}%
\end{equation}


\textit{Proof of (\ref{B.1.pf.a.1}).} We are going to prove (\ref{B.1.pf.a.1})
by induction over $i$:

\textit{Induction base:} Since $s=\mathbf{s}\left(  Y,x\right)  \geq1$ (by
Proposition A.4 \textbf{(g)}), we have $1\leq s$. Also, Proposition A.4
\textbf{(a)} (applied to $Y^{\prime}$ and $x^{\prime}$ instead of $Y$ and $x$)
yields $\mathbf{x}_{1}\left(  Y^{\prime},x^{\prime}\right)  =x^{\prime}$. Now,%
\begin{align*}
\mathbf{x}_{1}\left(  Y,x\right)   &  =x\ \ \ \ \ \ \ \ \ \ \left(  \text{by
Proposition A.4 \textbf{(a)}}\right) \\
&  \leq x^{\prime}=\mathbf{x}_{1}\left(  Y^{\prime},x^{\prime}\right)  .
\end{align*}
So we have proven that $1\leq s$ and $\mathbf{x}_{1}\left(  Y,x\right)
\leq\mathbf{x}_{1}\left(  Y^{\prime},x^{\prime}\right)  $. In other words, we
have proven that (\ref{B.1.pf.a.1}) holds for $i=1$. This completes the
induction base.

\textit{Induction step:} Let $\lambda\in\left\{  1,2,...,s^{\prime}\right\}  $
be such that $\lambda+1\in\left\{  1,2,...,s^{\prime}\right\}  $. Assume that
(\ref{B.1.pf.a.1}) holds for $i=\lambda$. In order to complete the induction
step, we must show that (\ref{B.1.pf.a.1}) holds for $i=\lambda+1$.

Since (\ref{B.1.pf.a.1}) holds for $i=\lambda$, we have%
\[
\lambda\leq s\text{ and }\mathbf{x}_{\lambda}\left(  Y,x\right)
\leq\mathbf{x}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  .
\]


Now, let us prove that $\mathbf{r}_{\lambda}\left(  Y,x\right)  <\mathbf{r}%
_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  $. In fact, $\lambda
\in\left\{  1,2,...,s^{\prime}\right\}  =\left\{  1,2,...,\mathbf{s}\left(
Y^{\prime},x^{\prime}\right)  \right\}  $ (since $s^{\prime}=\mathbf{s}\left(
Y^{\prime},x^{\prime}\right)  $). Hence, by Proposition A.4 \textbf{(b)}
(applied to $\lambda$, $Y^{\prime}$ and $x^{\prime}$ instead of $\alpha$, $Y$
and $x$), the number $\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime
}\right)  $ is the smallest $p\in\mathbb{N}$ such that $\mathbf{x}_{\lambda
}\left(  Y^{\prime},x^{\prime}\right)  <Y_{\lambda,p}^{\prime}$. Hence,
$\mathbf{x}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  <Y_{\lambda
,\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  }^{\prime}$. On the
other hand, $\lambda\leq s=\mathbf{s}\left(  Y,x\right)  $, so that
$\lambda\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $. Hence,
Proposition A.4 \textbf{(e)} (applied to $\alpha=\lambda$) yields
$\mathbf{x}_{\lambda}\left(  Y,x\right)  =\left(
\underbrace{\operatorname*{ins}\left(  Y,x\right)  }_{=Y^{\prime}}\right)
_{\lambda,\mathbf{r}_{\lambda}\left(  Y,x\right)  }=Y_{\lambda,\mathbf{r}%
_{\lambda}\left(  Y,x\right)  }^{\prime}$. Hence,%
\[
Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y,x\right)  }^{\prime}=\mathbf{x}%
_{\lambda}\left(  Y,x\right)  \leq\mathbf{x}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  <Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  }^{\prime}.
\]


Proposition A.4 \textbf{(j)} yields that the numbers $\mathbf{x}_{1}\left(
Y,x\right)  $, $\mathbf{x}_{2}\left(  Y,x\right)  $, $...$, $\mathbf{x}%
_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  $ are positive integers.
In other words, $\mathbf{x}_{\beta}\left(  Y,x\right)  $ is a positive integer
for every $\beta\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $.
Applied to $\beta=\lambda$, this yields that $\mathbf{x}_{\lambda}\left(
Y,x\right)  $ is a positive integer (since $\lambda\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $), so that $\mathbf{x}%
_{\lambda}\left(  Y,x\right)  \neq\infty$. Hence, $Y_{\lambda,\mathbf{r}%
_{\lambda}\left(  Y,x\right)  }^{\prime}=\mathbf{x}_{\lambda}\left(
Y,x\right)  \neq\infty$. Combined with $Y_{\lambda,\mathbf{r}_{\lambda}\left(
Y,x\right)  }^{\prime}<Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  }^{\prime}$, this yields $Y_{\lambda,\mathbf{r}_{\lambda
}\left(  Y,x\right)  }^{\prime}<_{\infty}Y_{\lambda,\mathbf{r}_{\lambda
}\left(  Y^{\prime},x^{\prime}\right)  }^{\prime}$. Hence, $\mathbf{r}%
_{\lambda}\left(  Y,x\right)  <\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  $ (by (\ref{B.1.pf.0}), applied to $\alpha=\lambda$,
$\beta=\mathbf{r}_{\lambda}\left(  Y,x\right)  $ and $\gamma=\mathbf{r}%
_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  $).

Now, $\lambda\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $.
Hence, Proposition A.4 \textbf{(c)} (applied to $\alpha=\lambda$) shows that
the number $\mathbf{r}_{\lambda}\left(  Y,x\right)  $ is the highest
$p\in\mathbb{N}$ such that $\left(  \operatorname*{ins}\left(  Y,x\right)
\right)  _{\lambda,p}<_{\infty}\mathbf{x}_{\lambda+1}\left(  Y,x\right)  $.
Thus, for every $\rho\in\mathbb{N}$ such that $\rho>\mathbf{r}_{\lambda
}\left(  Y,x\right)  $, the relation $\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{\lambda,\rho}<_{\infty}\mathbf{x}_{\lambda+1}\left(
Y,x\right)  $ does \textit{not} hold. Applying this to $\rho=\mathbf{r}%
_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  $, we get: The relation
$\left(  \operatorname*{ins}\left(  Y,x\right)  \right)  _{\lambda
,\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  }<_{\infty
}\mathbf{x}_{\lambda+1}\left(  Y,x\right)  $ does \textit{not} hold (since
$\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  >\mathbf{r}%
_{\lambda}\left(  Y,x\right)  $). In other words, we have $\mathbf{x}%
_{\lambda+1}\left(  Y,x\right)  \leq\left(  \operatorname*{ins}\left(
Y,x\right)  \right)  _{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  }$. Now,%
\begin{align*}
\mathbf{x}_{\lambda+1}\left(  Y,x\right)   &  \leq\left(  \operatorname*{ins}%
\left(  Y,x\right)  \right)  _{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  }=Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  }^{\prime}\ \ \ \ \ \ \ \ \ \ \left(  \text{since
}\operatorname*{ins}\left(  Y,x\right)  =Y^{\prime}\right) \\
&  =\mathbf{x}_{\lambda+1}\left(  Y^{\prime},x^{\prime}\right) \\
&  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{since Proposition A.4 \textbf{(d)} (applied to }Y^{\prime}\text{,
}x^{\prime}\text{ and }\lambda\text{ instead of }Y\text{, }x\text{ and }%
\alpha\text{)}\\
\text{yields }\mathbf{x}_{\lambda+1}\left(  Y^{\prime},x^{\prime}\right)
=Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)
}^{\prime}\text{ (since }\lambda\in\left\{  1,2,...,\mathbf{s}\left(
Y^{\prime},x^{\prime}\right)  \right\}  \text{)}%
\end{array}
\right)  .
\end{align*}


Next, it is easy to see that $\lambda\neq s$\ \ \ \ \footnote{\textit{Proof.}
Assume the contrary. Then, $\lambda=s$, so that $\lambda=s=\mathbf{s}\left(
Y,x\right)  $ and thus $\mathbf{x}_{\lambda+1}\left(  Y,x\right)
=\mathbf{x}_{\mathbf{s}\left(  Y,x\right)  +1}\left(  Y,x\right)  =\infty$ (by
Proposition A.4 \textbf{(i)}). Thus, $\mathbf{x}_{\lambda+1}\left(
Y,x\right)  \leq\mathbf{x}_{\lambda+1}\left(  Y^{\prime},x^{\prime}\right)  $
rewrites as $\infty\leq\mathbf{x}_{\lambda+1}\left(  Y^{\prime},x^{\prime
}\right)  $, so that we have $\mathbf{x}_{\lambda+1}\left(  Y^{\prime
},x^{\prime}\right)  =\infty$.
\par
But Proposition A.4 \textbf{(j)} (applied to $Y^{\prime}$ and $x^{\prime}$
instead of $Y$ and $x$) yields that the numbers $\mathbf{x}_{1}\left(
Y^{\prime},x^{\prime}\right)  $, $\mathbf{x}_{2}\left(  Y^{\prime},x^{\prime
}\right)  $, $...$, $\mathbf{x}_{\mathbf{s}\left(  Y^{\prime},x^{\prime
}\right)  }\left(  Y^{\prime},x^{\prime}\right)  $ are positive integers (i.
e., none of them is $\infty$) and satisfy $\mathbf{x}_{1}\left(  Y^{\prime
},x^{\prime}\right)  <\mathbf{x}_{2}\left(  Y^{\prime},x^{\prime}\right)
<...<\mathbf{x}_{\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)  }\left(
Y^{\prime},x^{\prime}\right)  $. Hence, the numbers $\mathbf{x}_{1}\left(
Y^{\prime},x^{\prime}\right)  $, $\mathbf{x}_{2}\left(  Y^{\prime},x^{\prime
}\right)  $, $...$, $\mathbf{x}_{\mathbf{s}\left(  Y^{\prime},x^{\prime
}\right)  }\left(  Y^{\prime},x^{\prime}\right)  $ are positive integers. In
other words, $\mathbf{x}_{\alpha}\left(  Y^{\prime},x^{\prime}\right)  $ is a
positive integer for every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(
Y^{\prime},x^{\prime}\right)  \right\}  $. Applying this to $\alpha=\lambda
+1$, we conclude that $\mathbf{x}_{\lambda+1}\left(  Y^{\prime},x^{\prime
}\right)  $ is a positive integer (since $\lambda+1\in\left\{
1,2,...,\underbrace{s^{\prime}}_{=\mathbf{s}\left(  Y^{\prime},x^{\prime
}\right)  }\right\}  =\left\{  1,2,...,\mathbf{s}\left(  Y^{\prime},x^{\prime
}\right)  \right\}  $), contradicting $\mathbf{x}_{\lambda+1}\left(
Y^{\prime},x^{\prime}\right)  =\infty$. This contradiction shows that our
assumption was wrong. Hence, we have $\lambda\neq s$, qed.}. Combined with
$\lambda\leq s$, this yields $\lambda+1\leq s$ (since $\lambda$ and $s$ are integers).

We have thus proven that%
\[
\lambda+1\leq s\text{ and }\mathbf{x}_{\lambda+1}\left(  Y,x\right)
\leq\mathbf{x}_{\lambda+1}\left(  Y^{\prime},x^{\prime}\right)  .
\]
Thus, (\ref{B.1.pf.a.1}) holds for $i=\lambda+1$. This completes the induction
step. Hence, (\ref{B.1.pf.a.1}) is proven by induction.

Applying (\ref{B.1.pf.a.1}) to $\lambda=s^{\prime}$, we conclude that
\[
s^{\prime}\leq s\text{ and }\mathbf{x}_{s^{\prime}}\left(  Y,x\right)
\leq\mathbf{x}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  \text{.}%
\]
Thus we have proven $s^{\prime}\leq s$, so that $s\geq s^{\prime}$.

Moreover, $\mathbf{t}\left(  Y,x\right)  =\mathbf{r}_{\mathbf{s}\left(
Y,x\right)  }\left(  Y,x\right)  $ (by Proposition A.4 \textbf{(h)}). Since
$\mathbf{t}\left(  Y,x\right)  =t$ and $\mathbf{s}\left(  Y,x\right)  =s$,
this rewrites as $t=\mathbf{r}_{s}\left(  Y,x\right)  $.

Moreover, $\mathbf{t}\left(  Y^{\prime},x^{\prime}\right)  =\mathbf{r}%
_{\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)  }\left(  Y^{\prime
},x^{\prime}\right)  $ (by Proposition A.4 \textbf{(h)}, applied to
$Y^{\prime}$ and $x^{\prime}$ instead of $Y$ and $x$). Since $\mathbf{t}%
\left(  Y^{\prime},x^{\prime}\right)  =t^{\prime}$ and $\mathbf{s}\left(
Y^{\prime},x^{\prime}\right)  =s^{\prime}$, this rewrites as $t^{\prime
}=\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  $.

By Proposition A.4 \textbf{(k)}, the numbers $\mathbf{r}_{1}\left(
Y,x\right)  $, $\mathbf{r}_{2}\left(  Y,x\right)  $, $...$, $\mathbf{r}%
_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  $ are positive integers
(i. e., none of them is $\infty$) and satisfy $\mathbf{r}_{1}\left(
Y,x\right)  \geq\mathbf{r}_{2}\left(  Y,x\right)  \geq...\geq\mathbf{r}%
_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  $. Since $\mathbf{r}%
_{1}\left(  Y,x\right)  \geq\mathbf{r}_{2}\left(  Y,x\right)  \geq
...\geq\mathbf{r}_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  $, we
have $\mathbf{r}_{\alpha}\left(  Y,x\right)  \geq\mathbf{r}_{\beta}\left(
Y,x\right)  $ for any positive integers $\alpha$ and $\beta$ satisfying
$\alpha\leq\beta\leq\mathbf{s}\left(  Y,x\right)  $. Applying this to
$\alpha=s^{\prime}$ and $\beta=s$, we obtain $\mathbf{r}_{s^{\prime}}\left(
Y,x\right)  \geq\mathbf{r}_{s}\left(  Y,x\right)  $ (since $s^{\prime}\leq
s=\mathbf{s}\left(  Y,x\right)  $).

Since $s^{\prime}\leq s=\mathbf{s}\left(  Y,x\right)  $, we have $s^{\prime
}\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $.

Now, $s^{\prime}=\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)  $, so that
$s^{\prime}\in\left\{  1,2,...,\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)
\right\}  $. Hence, by Proposition A.4 \textbf{(b)} (applied to $s^{\prime}$,
$Y^{\prime}$ and $x^{\prime}$ instead of $\alpha$, $Y$ and $x$), the number
$\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  $ is the
smallest $p\in\mathbb{N}$ such that $\mathbf{x}_{s^{\prime}}\left(  Y^{\prime
},x^{\prime}\right)  <Y_{s^{\prime},p}^{\prime}$. Hence, $\mathbf{x}%
_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  <Y_{s^{\prime}%
,\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  }^{\prime}$. On
the other hand, $s^{\prime}\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)
\right\}  $, so that Proposition A.4 \textbf{(e)} (applied to $\alpha
=s^{\prime}$) yields $\mathbf{x}_{s^{\prime}}\left(  Y,x\right)  =\left(
\underbrace{\operatorname*{ins}\left(  Y,x\right)  }_{=Y^{\prime}}\right)
_{s^{\prime},\mathbf{r}_{s^{\prime}}\left(  Y,x\right)  }=Y_{s^{\prime
},\mathbf{r}_{s^{\prime}}\left(  Y,x\right)  }^{\prime}$. Hence,%
\[
Y_{s^{\prime},\mathbf{r}_{s^{\prime}}\left(  Y,x\right)  }^{\prime}%
=\mathbf{x}_{s^{\prime}}\left(  Y,x\right)  \leq\mathbf{x}_{s^{\prime}}\left(
Y^{\prime},x^{\prime}\right)  <Y_{s^{\prime},\mathbf{r}_{s^{\prime}}\left(
Y^{\prime},x^{\prime}\right)  }^{\prime}.
\]


Proposition A.4 \textbf{(j)} yields that the numbers $\mathbf{x}_{1}\left(
Y,x\right)  $, $\mathbf{x}_{2}\left(  Y,x\right)  $, $...$, $\mathbf{x}%
_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  $ are positive integers.
In other words, $\mathbf{x}_{\beta}\left(  Y,x\right)  $ is a positive integer
for every $\beta\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $.
Applied to $\beta=s^{\prime}$, this yields that $\mathbf{x}_{s^{\prime}%
}\left(  Y,x\right)  $ is a positive integer (since $s^{\prime}\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $), so that $\mathbf{x}%
_{s^{\prime}}\left(  Y,x\right)  \neq\infty$. Thus, $Y_{s^{\prime}%
,\mathbf{r}_{s^{\prime}}\left(  Y,x\right)  }^{\prime}=\mathbf{x}_{s^{\prime}%
}\left(  Y,x\right)  \neq\infty$. Combined with $Y_{s^{\prime},\mathbf{r}%
_{s^{\prime}}\left(  Y,x\right)  }^{\prime}<Y_{s^{\prime},\mathbf{r}%
_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  }^{\prime}$, this yields
$Y_{s^{\prime},\mathbf{r}_{s^{\prime}}\left(  Y,x\right)  }^{\prime}<_{\infty
}Y_{s^{\prime},\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)
}^{\prime}$. Hence, $\mathbf{r}_{s^{\prime}}\left(  Y,x\right)  <\mathbf{r}%
_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  $ (by (\ref{B.1.pf.0}),
applied to $\alpha=s^{\prime}$, $\beta=\mathbf{r}_{s^{\prime}}\left(
Y,x\right)  $ and $\gamma=\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime
}\right)  $). In other words, $\mathbf{r}_{s^{\prime}}\left(  Y^{\prime
},x^{\prime}\right)  >\mathbf{r}_{s^{\prime}}\left(  Y,x\right)  $. Now,%
\[
t^{\prime}=\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)
>\mathbf{r}_{s^{\prime}}\left(  Y,x\right)  \geq\mathbf{r}_{s}\left(
Y,x\right)  =t.
\]


We have thus proven that $s\geq s^{\prime}$ and $t^{\prime}>t$. This proves
(\ref{B.1.pf.a}).

\textbf{(b)} Next we will prove that
\begin{equation}
\text{if }x^{\prime}<x\text{, then }\left(  s^{\prime}>s\text{ and }t\geq
t^{\prime}\right)  . \label{B.1.pf.b}%
\end{equation}


\textit{Proof of (\ref{B.1.pf.b}).} Assume that $x^{\prime}<x$. We are going
to prove that every $i\in\left\{  1,2,...,s+1\right\}  $ satisfies%
\begin{equation}
i\leq s^{\prime}\text{ and }\mathbf{x}_{i}\left(  Y^{\prime},x^{\prime
}\right)  <_{\infty}\mathbf{x}_{i}\left(  Y,x\right)  \text{.}
\label{B.1.pf.b.1}%
\end{equation}


\textit{Proof of (\ref{B.1.pf.b.1}).} We are going to prove (\ref{B.1.pf.b.1})
by induction over $i$:

\textit{Induction base:} Recall that one part of Proposition A.4 \textbf{(g)}
states that $\mathbf{s}\left(  Y,x\right)  \geq1$. Applying this part to
$Y^{\prime}$ and $x^{\prime}$ instead of $Y$ and $x$, we obtain $\mathbf{s}%
\left(  Y^{\prime},x^{\prime}\right)  \geq1$. Thus, $1\leq\mathbf{s}\left(
Y^{\prime},x^{\prime}\right)  =s^{\prime}$.

Also, Proposition A.4 \textbf{(a)} (applied to $Y^{\prime}$ and $x^{\prime}$
instead of $Y$ and $x$) yields%
\[
\mathbf{x}_{1}\left(  Y^{\prime},x^{\prime}\right)  =x^{\prime}<x=\mathbf{x}%
_{1}\left(  Y,x\right)  \ \ \ \ \ \ \ \ \ \ \left(  \text{since }%
\mathbf{x}_{1}\left(  Y,x\right)  =x\text{ by Proposition A.4 \textbf{(a)}%
}\right)  .
\]
Since $\mathbf{x}_{1}\left(  Y^{\prime},x^{\prime}\right)  =x^{\prime}%
\neq\infty$, this yields $\mathbf{x}_{1}\left(  Y^{\prime},x^{\prime}\right)
<_{\infty}\mathbf{x}_{1}\left(  Y,x\right)  $.

Thus we have proven that $1\leq s^{\prime}$ and $\mathbf{x}_{1}\left(
Y^{\prime},x^{\prime}\right)  <_{\infty}\mathbf{x}_{1}\left(  Y,x\right)  $.
In other words, we have proven that (\ref{B.1.pf.b.1}) holds for $i=1$. This
completes the induction base.

\textit{Induction step:} Let $\lambda\in\left\{  1,2,...,s+1\right\}  $ be
such that $\lambda+1\in\left\{  1,2,...,s+1\right\}  $. Assume that
(\ref{B.1.pf.b.1}) holds for $i=\lambda$. In order to complete the induction
step, we must show that (\ref{B.1.pf.b.1}) holds for $i=\lambda+1$.

Since (\ref{B.1.pf.b.1}) holds for $i=\lambda$, we have%
\[
\lambda\leq s^{\prime}\text{ and }\mathbf{x}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  <_{\infty}\mathbf{x}_{\lambda}\left(  Y,x\right)  .
\]


Now, let us prove that $\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime
}\right)  \leq\mathbf{r}_{\lambda}\left(  Y,x\right)  $.

In fact, $\lambda\leq s^{\prime}$, so that $\lambda\in\left\{
1,2,...,s^{\prime}\right\}  =\left\{  1,2,...,\mathbf{s}\left(  Y^{\prime
},x^{\prime}\right)  \right\}  $ (since $s^{\prime}=\mathbf{s}\left(
Y^{\prime},x^{\prime}\right)  $). Hence, by Proposition A.4 \textbf{(b)}
(applied to $\lambda$, $Y^{\prime}$ and $x^{\prime}$ instead of $\alpha$, $Y$
and $x$), the number $\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime
}\right)  $ is the smallest $p\in\mathbb{N}$ such that $\mathbf{x}_{\lambda
}\left(  Y^{\prime},x^{\prime}\right)  <Y_{\lambda,p}^{\prime}$. Hence, for
every $\rho\in\mathbb{N}$ satisfying $\rho<\mathbf{r}_{\lambda}\left(
Y^{\prime},x^{\prime}\right)  $, we do \textit{not} have $\mathbf{x}_{\lambda
}\left(  Y^{\prime},x^{\prime}\right)  <Y_{\lambda,\rho}^{\prime}$. Applying
this to $\rho=\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  -1$
(this is allowed since $\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime
}\right)  -1\in\mathbb{N}$\ \ \ \ \footnote{\textit{Proof.} Assume the
opposite. Then, $\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)
-1\notin\mathbb{N}$, so that $\mathbf{r}_{\lambda}\left(  Y^{\prime}%
,x^{\prime}\right)  =0$ (since $\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  \in\mathbb{N}$) and thus $Y_{\lambda,\mathbf{r}_{\lambda
}\left(  Y^{\prime},x^{\prime}\right)  }^{\prime}=Y_{\lambda,0}^{\prime}=0$
(because $Y^{\prime}$ is a GYT, and thus the $0$-th column of $Y^{\prime}$
contains only zeroes). But we have $\mathbf{x}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  <Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  }^{\prime}$ (since $\mathbf{r}_{\lambda}\left(
Y^{\prime},x^{\prime}\right)  $ is the smallest $p\in\mathbb{N}$ such that
$\mathbf{x}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  <Y_{\lambda
,p}^{\prime}$). Thus, $\mathbf{x}_{\lambda}\left(  Y^{\prime},x^{\prime
}\right)  <Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime
}\right)  }^{\prime}=0$, which is impossible. This contradiction shows that
our assumption was wrong, so that $\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  -1\in\mathbb{N}$ is proven.} and $\mathbf{r}_{\lambda
}\left(  Y^{\prime},x^{\prime}\right)  -1<\mathbf{r}_{\lambda}\left(
Y^{\prime},x^{\prime}\right)  $), we conclude that we do \textit{not} have
$\mathbf{x}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  <Y_{\lambda
,\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  -1}^{\prime}$.
Hence, $Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)
-1}^{\prime}\leq\mathbf{x}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  $.

On the other hand, since $\lambda\in\left\{  1,2,...,s+1\right\}  $ and
$\lambda+1\in\left\{  1,2,...,s+1\right\}  $, we have $\lambda\in\left\{
1,2,...,s\right\}  =\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $
(since $s=\mathbf{s}\left(  Y,x\right)  $).

Thus, Proposition A.4 \textbf{(e)} (applied to $\alpha=\lambda$) yields
$\mathbf{x}_{\lambda}\left(  Y,x\right)  =\left(
\underbrace{\operatorname*{ins}\left(  Y,x\right)  }_{=Y^{\prime}}\right)
_{\lambda,\mathbf{r}_{\lambda}\left(  Y,x\right)  }=Y_{\lambda,\mathbf{r}%
_{\lambda}\left(  Y,x\right)  }^{\prime}$. Hence,%
\[
Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)
-1}^{\prime}\leq\mathbf{x}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)
<_{\infty}\mathbf{x}_{\lambda}\left(  Y,x\right)  =Y_{\lambda,\mathbf{r}%
_{\lambda}\left(  Y,x\right)  }^{\prime}.
\]
Hence, $\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)
-1<\mathbf{r}_{\lambda}\left(  Y,x\right)  $ (by (\ref{B.1.pf.0}), applied to
$\alpha=\lambda$, $\beta=\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime
}\right)  -1$ and $\gamma=\mathbf{r}_{\lambda}\left(  Y,x\right)  $), so that
$\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  \leq\mathbf{r}%
_{\lambda}\left(  Y,x\right)  $ (since $\mathbf{r}_{\lambda}\left(  Y^{\prime
},x^{\prime}\right)  $ and $\mathbf{r}_{\lambda}\left(  Y,x\right)  $ are
integers). Thus, $Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime
}\right)  }^{\prime}\leq Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y,x\right)
}^{\prime}$ (because $Y^{\prime}=\operatorname*{ins}\left(  Y,x\right)  $ is a
GYT, and thus every row of $Y^{\prime}$ is weakly increasing).

Proposition A.4 \textbf{(j)} yields that the numbers $\mathbf{x}_{1}\left(
Y,x\right)  $, $\mathbf{x}_{2}\left(  Y,x\right)  $, $...$, $\mathbf{x}%
_{\mathbf{s}\left(  Y,x\right)  }\left(  Y,x\right)  $ are positive integers
(i. e., none of them is $\infty$) and satisfy $\mathbf{x}_{1}\left(
Y,x\right)  <\mathbf{x}_{2}\left(  Y,x\right)  <...<\mathbf{x}_{\mathbf{s}%
\left(  Y,x\right)  }\left(  Y,x\right)  $. Hence, $\mathbf{x}_{1}\left(
Y,x\right)  <\mathbf{x}_{2}\left(  Y,x\right)  <...<\mathbf{x}_{\mathbf{s}%
\left(  Y,x\right)  }\left(  Y,x\right)  <\infty$. Since $\infty
=\mathbf{x}_{\mathbf{s}\left(  Y,x\right)  +1}\left(  Y,x\right)  $ (due to
Proposition A.4 \textbf{(i)}), this rewrites as $\mathbf{x}_{1}\left(
Y,x\right)  <\mathbf{x}_{2}\left(  Y,x\right)  <...<\mathbf{x}_{\mathbf{s}%
\left(  Y,x\right)  }\left(  Y,x\right)  <\mathbf{x}_{\mathbf{s}\left(
Y,x\right)  +1}\left(  Y,x\right)  $. In other words, $\mathbf{x}_{\alpha
}\left(  Y,x\right)  <\mathbf{x}_{\alpha+1}\left(  Y,x\right)  $ for every
$\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $. Applied
to $\alpha=\lambda$, this yields $\mathbf{x}_{\lambda}\left(  Y,x\right)
<\mathbf{x}_{\lambda+1}\left(  Y,x\right)  $ (since $\lambda\in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $).

On the other hand, $\mathbf{x}_{\alpha}\left(  Y,x\right)  $ is a positive
integer for every $\alpha\in\left\{  1,2,...,\mathbf{s}\left(  Y,x\right)
\right\}  $ (since $\mathbf{x}_{1}\left(  Y,x\right)  $, $\mathbf{x}%
_{2}\left(  Y,x\right)  $, $...$, $\mathbf{x}_{\mathbf{s}\left(  Y,x\right)
}\left(  Y,x\right)  $ are positive integers). Applied to $\alpha=\lambda$,
this yields that $\mathbf{x}_{\lambda}\left(  Y,x\right)  $ is a positive
integer. Thus, $\mathbf{x}_{\lambda}\left(  Y,x\right)  \neq\infty$. Combined
with $\mathbf{x}_{\lambda}\left(  Y,x\right)  <\mathbf{x}_{\lambda+1}\left(
Y,x\right)  $, this yields $\mathbf{x}_{\lambda}\left(  Y,x\right)  <_{\infty
}\mathbf{x}_{\lambda+1}\left(  Y,x\right)  $.

Recall that $\lambda\in\left\{  1,2,...,\mathbf{s}\left(  Y^{\prime}%
,x^{\prime}\right)  \right\}  $. Hence, Proposition A.4 \textbf{(d)} (applied
to $\lambda$, $Y^{\prime}$ and $x^{\prime}$ instead of $\alpha$, $Y$ and $x$)
yields%
\[
\mathbf{x}_{\lambda+1}\left(  Y^{\prime},x^{\prime}\right)  =Y_{\lambda
,\mathbf{r}_{\lambda}\left(  Y^{\prime},x^{\prime}\right)  }^{\prime}\leq
Y_{\lambda,\mathbf{r}_{\lambda}\left(  Y,x\right)  }^{\prime}=\mathbf{x}%
_{\lambda}\left(  Y,x\right)  <_{\infty}\mathbf{x}_{\lambda+1}\left(
Y,x\right)  .
\]


Next, it is easy to see that $\lambda\neq s^{\prime}$%
\ \ \ \ \footnote{\textit{Proof.} Assume the contrary. Then, $\lambda
=s^{\prime}$, so that $\lambda=s^{\prime}=\mathbf{s}\left(  Y^{\prime
},x^{\prime}\right)  $ and thus $\mathbf{x}_{\lambda+1}\left(  Y^{\prime
},x^{\prime}\right)  =\mathbf{x}_{\mathbf{s}\left(  Y^{\prime},x^{\prime
}\right)  +1}\left(  Y^{\prime},x^{\prime}\right)  =\infty$ (by Proposition
A.4 \textbf{(i)}, applied to $Y^{\prime}$ and $x^{\prime}$ instead of $Y$ and
$x$). Thus, $\mathbf{x}_{\lambda+1}\left(  Y^{\prime},x^{\prime}\right)
<_{\infty}\mathbf{x}_{\lambda+1}\left(  Y,x\right)  $ rewrites as
$\infty<_{\infty}\mathbf{x}_{\lambda+1}\left(  Y,x\right)  $, which is absurd.
This contradiction shows that our assumption was wrong. Hence, we have
$\lambda\neq s^{\prime}$, qed.}. Combined with $\lambda\leq s^{\prime}$, this
yields $\lambda+1\leq s^{\prime}$ (since $\lambda$ and $s^{\prime}$ are integers).

We have thus proven that%
\[
\lambda+1\leq s^{\prime}\text{ and }\mathbf{x}_{\lambda+1}\left(  Y^{\prime
},x^{\prime}\right)  <_{\infty}\mathbf{x}_{\lambda+1}\left(  Y,x\right)  .
\]
Thus, (\ref{B.1.pf.b.1}) holds for $i=\lambda+1$. This completes the induction
step. Hence, (\ref{B.1.pf.b.1}) is proven by induction.

Applying (\ref{B.1.pf.b.1}) to $i=s+1$, we conclude that
\[
s+1\leq s^{\prime}\text{ and }\mathbf{x}_{s+1}\left(  Y^{\prime},x^{\prime
}\right)  <_{\infty}\mathbf{x}_{s+1}\left(  Y,x\right)  \text{.}%
\]
Thus we have proven $s+1\leq s^{\prime}$, so that $s^{\prime}\geq s+1>s$.

Moreover, $\mathbf{t}\left(  Y,x\right)  =\mathbf{r}_{\mathbf{s}\left(
Y,x\right)  }\left(  Y,x\right)  $ (by Proposition A.4 \textbf{(h)}). Since
$\mathbf{t}\left(  Y,x\right)  =t$ and $\mathbf{s}\left(  Y,x\right)  =s$,
this rewrites as $t=\mathbf{r}_{s}\left(  Y,x\right)  $.

Moreover, $\mathbf{t}\left(  Y^{\prime},x^{\prime}\right)  =\mathbf{r}%
_{\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)  }\left(  Y^{\prime
},x^{\prime}\right)  $ (by Proposition A.4 \textbf{(h)}, applied to
$Y^{\prime}$ and $x^{\prime}$ instead of $Y$ and $x$). Since $\mathbf{t}%
\left(  Y^{\prime},x^{\prime}\right)  =t^{\prime}$ and $\mathbf{s}\left(
Y^{\prime},x^{\prime}\right)  =s^{\prime}$, this rewrites as $t^{\prime
}=\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  $.

Now, let us prove that $\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)
\leq\mathbf{r}_{s}\left(  Y,x\right)  $.

In fact, $s\leq s^{\prime}$, so that $s\in\left\{  1,2,...,s^{\prime}\right\}
=\left\{  1,2,...,\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)  \right\}  $
(since $s^{\prime}=\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)  $). Hence,
by Proposition A.4 \textbf{(b)} (applied to $s$, $Y^{\prime}$ and $x^{\prime}$
instead of $\alpha$, $Y$ and $x$), the number $\mathbf{r}_{s}\left(
Y^{\prime},x^{\prime}\right)  $ is the smallest $p\in\mathbb{N}$ such that
$\mathbf{x}_{s}\left(  Y^{\prime},x^{\prime}\right)  <Y_{s,p}^{\prime}$.
Hence, for every $\rho\in\mathbb{N}$ satisfying $\rho<\mathbf{r}_{s}\left(
Y^{\prime},x^{\prime}\right)  $, we do \textit{not} have $\mathbf{x}%
_{s}\left(  Y^{\prime},x^{\prime}\right)  <Y_{s,\rho}^{\prime}$. Applying this
to $\rho=\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  -1$ (this is
allowed since $\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)
-1\in\mathbb{N}$\ \ \ \ \footnote{\textit{Proof.} Assume the opposite. Then,
$\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  -1\notin\mathbb{N}$, so
that $\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  =0$ (since
$\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  \in\mathbb{N}$) and thus
$Y_{s,\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  }^{\prime}%
=Y_{s,0}^{\prime}=0$ (because $Y^{\prime}$ is a GYT, and thus the $0$-th
column of $Y^{\prime}$ contains only zeroes). But we have $\mathbf{x}%
_{s}\left(  Y^{\prime},x^{\prime}\right)  <Y_{s,\mathbf{r}_{s}\left(
Y^{\prime},x^{\prime}\right)  }^{\prime}$ (since $\mathbf{r}_{s}\left(
Y^{\prime},x^{\prime}\right)  $ is the smallest $p\in\mathbb{N}$ such that
$\mathbf{x}_{s}\left(  Y^{\prime},x^{\prime}\right)  <Y_{s,p}^{\prime}$).
Thus, $\mathbf{x}_{s}\left(  Y^{\prime},x^{\prime}\right)  <Y_{s,\mathbf{r}%
_{s}\left(  Y^{\prime},x^{\prime}\right)  }^{\prime}=0$, which is impossible.
This contradiction shows that our assumption was wrong, so that $\mathbf{r}%
_{s}\left(  Y^{\prime},x^{\prime}\right)  -1\in\mathbb{N}$ is proven.} and
$\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  -1<\mathbf{r}_{s}\left(
Y^{\prime},x^{\prime}\right)  $), we conclude that we do \textit{not} have
$\mathbf{x}_{s}\left(  Y^{\prime},x^{\prime}\right)  <Y_{s,\mathbf{r}%
_{s}\left(  Y^{\prime},x^{\prime}\right)  -1}^{\prime}$. Hence,
$Y_{s,\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  -1}^{\prime}%
\leq\mathbf{x}_{s}\left(  Y^{\prime},x^{\prime}\right)  $.

On the other hand, $s=\mathbf{s}\left(  Y,x\right)  \in\left\{
1,2,...,\mathbf{s}\left(  Y,x\right)  \right\}  $, so that Proposition A.4
\textbf{(e)} (applied to $\alpha=s$) yields $\mathbf{x}_{s}\left(  Y,x\right)
=\left(  \underbrace{\operatorname*{ins}\left(  Y,x\right)  }_{=Y^{\prime}%
}\right)  _{s,\mathbf{r}_{s}\left(  Y,x\right)  }=Y_{s,\mathbf{r}_{s}\left(
Y,x\right)  }^{\prime}$. Hence,%
\begin{align*}
Y_{s,\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  -1}^{\prime}  &
\leq\mathbf{x}_{s}\left(  Y^{\prime},x^{\prime}\right)  <_{\infty}%
\mathbf{x}_{s}\left(  Y,x\right)  \ \ \ \ \ \ \ \ \ \ \left(
\begin{array}
[c]{c}%
\text{because (\ref{B.1.pf.b.1}) (applied to }i=s\text{) yields}\\
s\leq s^{\prime}\text{ and }\mathbf{x}_{s}\left(  Y^{\prime},x^{\prime
}\right)  <_{\infty}\mathbf{x}_{s}\left(  Y,x\right)
\end{array}
\right) \\
&  =Y_{s,\mathbf{r}_{s}\left(  Y,x\right)  }^{\prime}.
\end{align*}
Hence, $\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  -1<\mathbf{r}%
_{s}\left(  Y,x\right)  $ (by (\ref{B.1.pf.0}), applied to $\alpha=s$,
$\beta=\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  -1$ and
$\gamma=\mathbf{r}_{s}\left(  Y,x\right)  $), so that $\mathbf{r}_{s}\left(
Y^{\prime},x^{\prime}\right)  \leq\mathbf{r}_{s}\left(  Y,x\right)  $ (since
$\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  $ and $\mathbf{r}%
_{s}\left(  Y,x\right)  $ are integers).

Proposition A.4 \textbf{(k)} (applied to $Y^{\prime}$ and $x^{\prime}$ instead
of $Y$ and $x$) yields that the numbers $\mathbf{r}_{1}\left(  Y^{\prime
},x^{\prime}\right)  $, $\mathbf{r}_{2}\left(  Y^{\prime},x^{\prime}\right)
$, $...$, $\mathbf{r}_{\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)
}\left(  Y^{\prime},x^{\prime}\right)  $ are positive integers (i. e., none of
them is $\infty$) and satisfy $\mathbf{r}_{1}\left(  Y^{\prime},x^{\prime
}\right)  \geq\mathbf{r}_{2}\left(  Y^{\prime},x^{\prime}\right)  \geq
...\geq\mathbf{r}_{\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)  }\left(
Y^{\prime},x^{\prime}\right)  $. Since $\mathbf{r}_{1}\left(  Y^{\prime
},x^{\prime}\right)  \geq\mathbf{r}_{2}\left(  Y^{\prime},x^{\prime}\right)
\geq...\geq\mathbf{r}_{\mathbf{s}\left(  Y^{\prime},x^{\prime}\right)
}\left(  Y^{\prime},x^{\prime}\right)  $, any two positive integers $\alpha$
and $\beta$ satisfying $\alpha\leq\beta\leq\mathbf{s}\left(  Y^{\prime
},x^{\prime}\right)  $ must satisfy $\mathbf{r}_{\alpha}\left(  Y^{\prime
},x^{\prime}\right)  \geq\mathbf{r}_{\beta}\left(  Y^{\prime},x^{\prime
}\right)  $. Applying this to $\alpha=s$ and $\beta=s^{\prime}$ (this is
allowed since $s\leq s^{\prime}=\mathbf{s}\left(  Y^{\prime},x^{\prime
}\right)  $), we obtain $\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)
\geq\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  $, so that
$\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)  \leq
\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  $. Now,%
\[
t^{\prime}=\mathbf{r}_{s^{\prime}}\left(  Y^{\prime},x^{\prime}\right)
\leq\mathbf{r}_{s}\left(  Y^{\prime},x^{\prime}\right)  \leq\mathbf{r}%
_{s}\left(  Y,x\right)  =t,
\]
so that $t\geq t^{\prime}$.

Thus we have proven that $s^{\prime}>s$ and $t\geq t^{\prime}$. The proof of
(\ref{B.1.pf.b}) is thus complete.

\textbf{(c)} Now it is very easy to complete the proof of Proposition B.1:

First of all,%
\begin{equation}
\text{if }x\leq x^{\prime}\text{, then }s\geq s^{\prime} \label{B.1.pf.c1}%
\end{equation}
(by (\ref{B.1.pf.a})). Second,%
\begin{equation}
\text{if }s\geq s^{\prime}\text{, then }x\leq x^{\prime} \label{B.1.pf.c2}%
\end{equation}
\footnote{\textit{Proof.} Let $s\geq s^{\prime}$. Assume that $x^{\prime}<x$.
Then, $s^{\prime}>s$ (by (\ref{B.1.pf.b})), contradicting $s\geq s^{\prime}$.
This contradiction shows that our assumption that $x^{\prime}<x$ was wrong.
Hence, we must have $x\leq x^{\prime}$, qed.}. By combining (\ref{B.1.pf.c1})
and (\ref{B.1.pf.c2}), we see that
\begin{subequations}
\begin{equation}
\text{the assertions }\left(  x\leq x^{\prime}\right)  \text{ and }\left(
s\geq s^{\prime}\right)  \text{ are equivalent.} \label{B.1.pf.c3}%
\end{equation}


Furthermore,%
\end{subequations}
\begin{equation}
\text{if }x\leq x^{\prime}\text{, then }t^{\prime}>t \label{B.1.pf.c4}%
\end{equation}
(by (\ref{B.1.pf.a})). Second,%
\begin{equation}
\text{if }t^{\prime}>t\text{, then }x\leq x^{\prime} \label{B.1.pf.c5}%
\end{equation}
\footnote{\textit{Proof.} Let $t^{\prime}>t$. Assume that $x^{\prime}<x$.
Then, $t\geq t^{\prime}$ (by (\ref{B.1.pf.b})), contradicting $t^{\prime}>t$.
This contradiction shows that our assumption that $x^{\prime}<x$ was wrong.
Hence, we must have $x\leq x^{\prime}$, qed.}. By combining (\ref{B.1.pf.c4})
and (\ref{B.1.pf.c5}), we see that
\begin{equation}
\text{the assertions }\left(  x\leq x^{\prime}\right)  \text{ and }\left(
t^{\prime}>t\right)  \text{ are equivalent.} \label{B.1.pf.c6}%
\end{equation}


By combining (\ref{B.1.pf.c3}) and (\ref{B.1.pf.c6}), we see that the
assertions $\left(  x\leq x^{\prime}\right)  $, $\left(  s\geq s^{\prime
}\right)  $ and $\left(  t^{\prime}>t\right)  $ are equivalent. This proves
Theorem B.1.

\rule{17cm}{0.3mm}


\end{document}