Lbl_1 allows the system to take two different transitions from the initial state, one per flag value, and TLC will check both of these transitions (cf. the number of distinct states that TLC reports).
Another way to understand this is that the existential quantifier occurs on the left of the implication of a putative theorem
Spec => Property
(where by default Property checks absence of deadlock), and therefore has universal force according to the law of logic that asserts the equivalence of
(\E x \in S : F) => G and \A x \in S : (F => G)
when x doesn't occur in G.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/032F36EC-DA67-4D4A-ACE7-0DDB00B724CA%40gmail.com.