I have been working on a proof using TLAPS, but I seem to be stuck at a simple step which should be very obvious.
So the following is a snippet from my proof :
<2>3a. \A Q \in Quorum: \E a \in Q : maxVBal[a] \geq b
<2>3b. b \geq 0
<2>3c. \A Q \in Quorum: \E a \in Q : maxVBal[a] \geq 0
BY <2>3a, <2>3b
The BY proof for step <2>3c is not going through.
Shouldn't <2>3c be a simple logical consequence of <2>3a and <2>3b ? (Unless I am making an extremely silly error)
Is there a syntax/semantic error that is preventing the proof from going through or is it some limitation of the back end solvers that requires this simple proof to be broken even further?