Hi,
I was intrigued by a statement proved by TLAPS 1.5.2 on my Windows 10 machine. If we look at Paxos.tla in the examples directory, the proof of THEOREM Invariant -> <2>1 TypeOK' -> <3>1. PROVE for Phase1a(b), we have, (line 295)
<3>1. ASSUME NEW b \in Ballots, Phase1a(b) PROVE TypeOK'
BY <3>1 DEF TypeOK, Phase1a, Send, Messages
If I change this to:
<3>1. ASSUME NEW b \in Ballots, Phase1a(b) PROVE TypeOK'
BY <3>1, PTL DEF TypeOK, Phase1a, Send\*, Messages
I comment out Messages definition and add PTL, the proof goes through. In fact you can comment out the whole DEF. Is this expected behaviour or a bug?
Note that it doesn't prove on my Linux machine.
Thanks,
Saksham Chand