Reverse row deletion

Let $U$ be a standard tableau with distinct real entries (Tableaux and standard tableaux) and let $b=(s,t)$ be a removable node of $[\mathrm{shape}(U)]$ (so $t={\lambda }_s$ for $\lambda =\mathrm{shape}(U)$). The reverse row deletion $U-b$ is the following procedure. Set $i:=s$ and $x_{s+1}:=+\mathrm{\infty }$ (a symbol larger than every real number). While $i\ge 1$: let $j$ be the largest index with $1\le j\le {\lambda }_i$ and $U(i,j)<x_{i+1}$ (for $i=s$ this is $j={\lambda }_s=t$, the box $b$), set $x_i:=U(i,j)$ and overwrite the entry of box $(i,j)$ by $x_{i+1}$ (for $i=s$ this empties the box $b$); if $i=1$ stop, otherwise replace $i$ by $i-1$ and repeat. The procedure terminates after exactly $s$ row visits, since $i$ strictly decreases and stops at $1$. Its result is the filling $V$ of $[\mathrm{shape}(U)]\setminus \{b\}$ obtained by the overwrites, and the expelled letter is $x_1$. We write $(V,x_1):=U-b$.

The index $j$ exists at every step, and $V$ is a standard tableau, so the procedure is well defined. For existence: after a row $i+1$ has been processed, the carried letter $x_{i+1}$ was the entry of the box $(i+1,j_{i+1})$ before that box was overwritten, where $j_{i+1}$ is the position used in row $i+1$; the box $(i,j_{i+1})$ of the row above lies in the diagram, because $j_{i+1}\le {\lambda }_{i+1}\le {\lambda }_i$, and by column strictness of $U$ it carries an entry strictly smaller than $x_{i+1}$; hence the set over which $j$ is defined is nonempty, and it is finite, so $j$ is well defined. For standardness of $V$: at the moment row $i$ is processed it is still the unmodified row $i$ of $U$, and $j$ is the largest index with $U(i,j)<x_{i+1}$, so $U(i,j-1)<x_{i+1}<U(i,j+1)$ when those neighbours exist, which keeps the row strictly increasing after the overwrite; the entry above the overwritten box is $U(i-1,j)<U(i,j)<x_{i+1}$; and the entry below, $U(i+1,j)$ after row $i+1$ has been processed, is larger than $x_{i+1}$: if $j=j_{i+1}$ it is the overwriting letter $x_{i+2}>x_{i+1}$, and if $j>j_{i+1}$ it is the unchanged entry in column $j$ of row $i+1$, which exceeds the unchanged entry $U(i+1,j_{i+1})=x_{i+1}$ by row strictness. Thus all strict inequalities of a standard tableau hold in $V$. Finally, every entry of $U$ other than $x_1$ survives in $V$ with multiplicity one: each row visit moves one entry upward into the box it overwrites and the single box $b$ is emptied, so the multiset of entries of $V$ is that of $U$ with $x_1$ deleted; in particular $x_1$ is not an entry of $V$. No choice is used: the procedure is deterministic and all data are finite.