The TREE function assigns to a positive integer 
the greatest possible length 
of a sequence 
of nonempty finite unordered rooted
trees satisfying the following conditions. The vertices
of each rooted tree have labels from 
, and 
has at most 
vertices. No earlier 
may be related to a later 
by the comparison 
defined below (Friedman 2006).
Order the vertices of a rooted tree by declaring 
when 
lies on the unique path from the root to 
, including its endpoints. Write 
for the meet in this order. The
relation 
means that there is an injection 
from the vertices of 
to those of 
that preserves labels exactly and, for every pair of vertices 
of 
, satisfies
 |
The injection need not send the root of 
to the root of 
. Labels are compared by equality,
not by their numerical order (Gallier 1991).
For fixed 
,
only finitely many choices occur at each position, up to graph
isomorphism preserving roots and labels. If admissible sequences
had unbounded lengths, their finite prefixes would form a finitely branching infinite
rooted tree. König's
lemma would give an infinite admissible sequence,
contrary to Kruskal's tree theorem. Thus
is finite (Gallier 1991).
The first two values are 
and 
.
With two labels, the first single-vertex rooted
tree excludes its label from all later rooted trees.
To permit a third rooted tree, the second must consist
of two joined vertices bearing the other label. The
third is then the single-vertex rooted
tree with that label, after which no continuation is possible. The case 
is illustrated by Numberphile
(2017).
Prepending a single-vertex rooted tree with a new label to an admissible sequence
gives 
.
Thus 
.
The inverse threshold
 |
is defined for every nonnegative integer 
. Its values begin 1, 1, 2, 2, 3, ...
(OEIS A300402), indexed from 
.
? A Survey of Some Results in Proof Theory." Ann.
Pure and Appl. Logic 53, 199-260, 1991.