What does the first “non-free” variable mean here when substituting in simple type theory?

See this screenshot of the book "Basic Simple Type Theory". The infinite sequence they refer to is just a way to formalize the concept of having enough variables to work with no matter what. In my case, for practical reasons, all my variables are single unicode chars. I forsee for the next 100 years, that to be plenty of mathematical variables to work with.

So I'm in the process of implementing term substitution and I came across this ambiguity in the book:

What do they mean by the last line? Do they mean the first non-free variable including any bound variables within $$(N P)$$? Or do they mean the first "open, unused, available" variable in all of $$(N P)$$ including any abstractors $$\lambda w$$?

My guess is the latter, since $$z$$ is a dummy variable and of course this can't interfere with other variable useages.

• If I remember correctly, you could without problem have multiple abstractors $\lambda z\cdot( ...\lambda z \cdot ...)$ - they just don't interact with each other. In that case, you can just use the first variable that's not appearing unbound in either $N$ or $P$. Though, if you got enough chars, option #2 of cause can never go wrong – Sudix Feb 4 at 21:29
• Thanks @Sudix you are a gentlebeing and a scholar. – I Said Roll Up n Smoke Adjoint Feb 4 at 21:47