Hi Lorin,
If you read the section in Specifying Systems that describes how the
TLC model checker works, you will see that to compute the set of
states satisfying your initial predicate Init, it computes all states
satisfying TypeOK and throws away states that don't satisfy the
additional conjuncts. There are 5^25 (about 3*10^17) states
satisfying TypeOK. If you let Init equal TypeOK, TLC quickly runs out
of memory. If let Init equal TypeOK /\ FunctionsAreOnto, TLC runs
forever. These two data points should allow you to figure out what's
going on.
Cheers,
Leslie