After some back and forth between different encodings, I got to learn a little more TLA+ and would like to document my findings here.
> When I write [ x \in TypeX |-> f(x) ], is TLC generating all elements
in `TypeX` then computing their image under `f` or does it wait until
its called with an argument `m` to compute its image under `f`?
Yes, TLA+ does enumerate the domain of functions before computing the point in the image. This incurred a ridiculous overhead. We've seen a speedup from 4m46s to 12s to check a silly invariant. :)
Turns out that as long as your recursive calls do not change the higher-order operator being passed around, nested LET expressions work well:
entrypoint(Op(_,_),x,...) ==
LET RECURSIVE f1(...)
RECURSIVE f2(...)
f1(...) == ... Op(f2(....), ...)
f2(...) == ... Op(f1(...), ...)
IN f1(a,b,c,...)
Victor