The Prüfer code of a tree on a finite set of natural labels

Let $S\subseteq\mathbb N$ be finite with $|S|=n\ge2$, and let $T$ be a tree whose vertex set is $S$. Here $n-2$ denotes the unique natural number $m$ satisfying $m+2=n$. The Prüfer code is the word of length $n-2$ on $S$ obtained by repeating the following operation until two vertices remain:

1. choose the least labelled leaf $v$;
2. record the unique neighbour of $v$;
3. delete $v$ and its incident edge.

A nontrivial tree has a leaf, so the least one exists (Every tree with at least two vertices has at least two leaves, The well-ordering principle). Deleting a leaf from a tree with at least three vertices leaves a tree: paths between the remaining vertices never need the deleted leaf, and no cycle is introduced. Thus every stage is defined. Each stage removes one vertex, so precisely $n-2$ symbols are recorded.

The usual formulation has $S=n=\{0,1,\ldots,n-1\}$, using natural numbers as their von Neumann initial segments (The natural numbers $\mathbb{N}$ (von Neumann), The cardinality $\lvert A\rvert$ of a finite set). Allowing an arbitrary finite subset of natural labels is essential because every intermediate label set produced by deletion is again such a subset.