The ladder theorem

Let $p$ and $q$ be two column vectors of the same (finite) length. Let $[p \geq q]$ denote that in each row the $p$ -element is at least the $q$ -element, i.e.

$$ [ p \geq q ] \equiv \langle \forall i: p. i \geq q. i \rangle $$

Let sort. $v$ denote the result of sorting column vector v in ascending order. Then the ladder theorem states

(0) $[p\geqslant q]\Rightarrow [\operatorname {sort.}p\geqslant \operatorname {sort.}q]$

Proof We observe for any $x$ and $n \geq 1$

$x$ equals the nth element of sort. $p$

[\left{ {\text{sort.}p\text{ is sorted}}\right} ]

sort. $p$ contains at least $n$ elements $\leq x$

$\equiv { p,i$ a permutation of sort. $p}$

$p$ contains at least $n$ elements $\leq x$ $\Rightarrow { \left\lbrack {p \geq q}\right\rbrack ,\frac{}{\text{the antecedent of }\left( 0\right) }}$

$q$ contains at least $n$ elements $\leq x$

$\equiv \;{qis}{a\text{ permutation of sort.}}g}$

sort. q contains at least n elements $\leq x$

$\Rightarrow \;\left{ {{}^{\prime }\operatorname{sort}.g,\text{ is sorted }}\right}$

the $n$ th element of $\mathit{{sort}.g}$ is $\leq x$

and thus (0) has been established. (End of Proof.)

The ladder theorem is well-known. It tells us that if in a matrix with sorted rows we sort all the columns, the rows remain sorted.

The above proof of the ladder theorem has been recorded

has seen, yet, does. (i) because there are such messy proofs (ii) because I don't succeed in viewing the ladder theorem as "intuitively obvious." (iii) because the above proof is not totally trivial: if you start with observing for any $y$ and $n \geq 1$ :

$y$ equals the nth element of $\operatorname{sort}.g$ [\text{sort. g is sorted}} ]

sort. $q$ contains at least $n$ elements $\leq y$ ,

then you get stuck.

Austin, 16 February 1997

prof. dvr Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712 - 1188

USA