[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] How can this lemma (involving ) be applied?
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.