First row of RSK as a minimum-tail table (source code)

= First row of RSK as a minimum-tail table

For a <permutation> input, the first row of its <RSK> insertion tableau is the <minimum-tail table for increasing subsequences>: its $j$th entry is the least attainable final value of a <strictly increasing subsequence> of <length> $j$ in the processed prefix. Inserting $z$ replaces the first entry larger than $z$, or appends if none exists. In replacement position $r$, the previous entry in position $r-1$ supplies a subsequence that can be extended by $z$. Shorter <minimum> tails were already smaller, and a longer subsequence ending at $z$ would require an old tail in position at least $r$ smaller than $z$, contrary to the replacement rule. This proves the <invariant> inductively. Consequently the first-row <length> is the <longest increasing subsequence> <length>. The row entries need not be a subsequence together: input $2,4,3,1$ gives first row $1,3$, although one occurs after three. They are minima for different lengths, obtained from potentially different subsequences.