[morelisp]

> How do we know that BB(n) exists for all n?

It's trivial to construct a candidate for each n, which gives a lower bound.