Yes, and in fact, capturing "prior" values with bindings and closing over them in temporal operator thunks is how you talk about some relation between s and s' in a Bombadil formula (not having that particular syntax though). It's a deliberate way of embedding this LTL flavor in JS/TS in the most natural and ergonomic way I could think of. I didn't want a deep EDSL or even a new bespoke spec language that people (and LLMs) would have to learn, and to have to write tools for. Now you can write Bombadil specs with a good LSP and be able to import packages off of npm or whathaveyou. Most web devs will probably be comfy with JS or TS, so that's why I chose that style.

I hope that makes sense?

Thanks for the nice feedback!