Hi, the reason that the step fails is that for the backends your hypothesis Phase1b(a) gets coalesced into an anonymous predicate. For example, here is the input that Zenon receives: ;; obligation #1 $hyp "a_in" (TLA.in a Acceptors) $hyp "m_in" (TLA.in m a_msgshash_primea) $hyp "a_m1a_in" (TLA.in a_m1a msgs) $hyp "v'152" (a_h97e32460362eba8559dabb07ccf5e9a a) $goal (\/ (TLA.bEx Proposers ((p) (\/ (\/ (\/ (\/ (Phase1a p) (a_Phase2a1a p)) (a_Phase2a11a p)) (a_Phase2a12a p)) (a_Phase2a13a p)))) (TLA.bEx Acceptors ((a_1) (\/ (\/ (Phase1b a_1) (Phase2b a_1)) (PhasePr a_1))))) The hypothesis named "v'152" corresponds to Phase1b(a), and you can see that the predicate has been renamed and doesn't correspond to the one that appears in the conclusion. I don't have a clear explanation yet for why that happens, and I believe it is an error. My hunch is that the PM gets confused by the primed hypotheses in the enclosing SUFFICES steps <4> or <5> and then plays overly cautious. However, I can offer two workarounds: 1. Move your step further up in the proof hierarchy. For example, insert it immediately after step <2>6, like so: <3>0. Next BY <2>6 DEF Next Then, replace <5>6 by <3>0 in the justification of step <5>7. 2. Change lemma SafeAtStable by replacing "Next" on the left-hand side of the implication by "[Next]_vars", then you can omit step <5>6 altogether. We'll again investigate the coalescing algorithm to understand what went wrong here. Thanks for reporting this. Regards, Stephan
|