[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Stuck on an obvious proof [TLAPS]



Hi,

   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 
              OMITTED
        <2>3b. b \geq 0
              OMITTED            
        <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? 


Thank you   

--
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/c3224133-5b5b-4e28-9300-cd4b7f8ac083%40googlegroups.com.