[tlaplus] Confusing line in paxos tlaps proof (USE TRUE /\ TRUE)

[Ganesh Rapolu <grapolu@xxxxxxxxxxxx>]

See https://github.com/tlaplus/DrTLAPlus/blob/master/Paxos/Paxos.tla#L238 .

When I ran the proof of lemma SafeAtStable without this line, it fails, but with this line it succeeds.

It also fails if I change this to USE TRUE or USE TRUE \/ TRUE. But what does line actually do?

-- 
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/2518b08d-b9d2-444e-a0a7-4dc63144838bn%40googlegroups.com.