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

*From*: Saswata Paul <paulsaswata1@xxxxxxxxx>*Date*: Thu, 29 Aug 2019 14:21:02 -0400*References*: <c3224133-5b5b-4e28-9300-cd4b7f8ac083@googlegroups.com> <CAJSuO--QAZ1=qrR-n+RC63mrK-+sc_8E+1Xa+zqGn-xXngokKg@mail.gmail.com>

That worked! And it makes sense too.

Thank you for pointing that out!

Paul

On Thu, Aug 29, 2019 at 1:54 PM Saksham Chand <schand@xxxxxxxxxxxxxxxxx> wrote:

Types are missing (see the bold below).

<2>3c. \A Q \in Quorum: \E a \in Q : maxVBal[a] \geq 0BY <2>3a, <2>3bDEF TypeOK, BallotsThanks,Saksham--On Thu, Aug 29, 2019 at 1:23 PM Saswata Paul <paulsaswata1@xxxxxxxxx> wrote: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 bOMITTED<2>3b. b \geq 0OMITTED<2>3c. \A Q \in Quorum: \E a \in Q : maxVBal[a] \geq 0BY <2>3a, <2>3bThe 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.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/4PGjVzg4Wfg/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO--QAZ1%3DqrR-n%2BRC63mrK-%2Bsc_8E%2B1Xa%2BzqGn-xXngokKg%40mail.gmail.com.

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/CAHeFUE_UzsS%3DGiS%3DKOU83oUMGX%2B3eT%3DRyORhOnjk86MEEibc3w%40mail.gmail.com.

**References**:**[tlaplus] Stuck on an obvious proof [TLAPS]***From:*Saswata Paul

**Re: [tlaplus] Stuck on an obvious proof [TLAPS]***From:*Saksham Chand

- Prev by Date:
**Re: [tlaplus] Stuck on an obvious proof [TLAPS]** - Next by Date:
**[tlaplus] Re: Where can I download and install themes in the Toolbox?** - Previous by thread:
**Re: [tlaplus] Stuck on an obvious proof [TLAPS]** - Next by thread:
**[tlaplus] specify two different elements in a set** - Index(es):