A confusion about the TREE function. I know, from Kruskal's tree theorem, that the sequence of trees mentioned in the TREE function cannot be infinite. However, why can't the sequence of trees get arbitarily large, so that there is no infinite sequence, but there are arbitarily large sequences? As far as I know, Kruskal's theorem doesn't exclude such a possibility.
 A: Note that the argument below is hinted at in the first couple sentences of this part of the wiki article on Kruskal's theorem, although it doesn't say explicitly why Konig's lemma applies.

Let's say that an $n$-TREE sequence is a finite sequence $(T_i)_{1\le i\le m}$ of rooted $\{1,...,n\}$-labelled trees where $T_i$ has at most $i$ vertices and for $1\le i<j\le m$ we have $T_i\not\le T_j$.
I've bolded the key part, the vertex counting condition; this is the crucial point which allows us to apply compactness in the form of Konig's lemma to get the desired result.
Specifically, note that the set of $n$-TREE sequences forms a tree $\mathfrak{T}_n$ itself, ordered by extension - so if $\langle T_1, T_2\rangle$ is an $n$-TREE sequence, then both $\langle T_1\rangle$ and $\langle T_1,T_2\rangle$ are nodes on $\mathfrak{T}_n$ and $\langle T_1,T_2\rangle$ is an immediate successor of $\langle T_1\rangle$ on $\mathfrak{T}_n$.
Now Kruskal's tree theorem says that $\mathfrak{T}_n$ has no infinite paths, which as you observe isn't quite what we want. But for each $i$ there are only finitely many $\{1,...,n\}$-labelled trees with at most $i$ vertices. So $\mathfrak{T}_n$ is finitely branching, and we can apply Konig's lemma to conclude that if it were infinite it would have an infinite path. This lets us get from the absence of infinite paths to the absence of arbitrarily long paths.
