Friedman's finite form of Kruskal's theorem ($\forall k\exists N\forall (T_i{)}_{i\le N}\exists i<j(T_i⪯T_j)$)

For every natural parameter $k$, there is a finite length $N$ such that every sequence of $N$ finite rooted trees satisfying $|T_i|\le k+i$ has an earlier tree homeomorphically embedding into a later tree. It is a true finite-combinatorial principle unprovable in Peano arithmetic and in arithmetical transfinite recursion theory. Each fixed-parameter instance can still be verified by a sufficiently large finite search.