[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How can this lemma (involving []) be applied?

Hi Stephan,

Thanks a lot, this is very helpful. In my mental model NEW P and NEW Q approximately meant 'for all (boolean) expressions P and Q', but I now understand the distinctions you've made. It's also nice to see that your proposed proof to the corollary is even shorter than what I had in mind.

Kind regards,