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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Mon, 21 Nov 2022 06:41:50 -0800 (PST)*References*: <57a329dc-6578-4235-ad56-a579e35c2234n@googlegroups.com> <1986E5A8-0341-431E-AF85-8443FFDAD787@gmail.com>

To expand on Stephan's reply, the SUFFICES keyword is actually optional in SUFFICES steps. So just writing an _expression_ without any keyword prepended *is* writing a SUFFICES step.

Andrew

On Sunday, November 20, 2022 at 3:16:56 AM UTC-5 Stephan Merz wrote:

Hi Jaco,the directive "WITNESS e" quite clearly does not require proof, and by analogy (and in order to simplify the grammar) it was decided that "WITNESS e \in S" would not take a proof either but that the fact "e \in S" should follow obviously from the context. What you can do is write something like the following where the first step inserts the required fact in the context.<1>. e \in SBY ...<1>. WITNESS e \in SPersonally, I tend to use WITNESS rarely but usually write something like<1>x. e \in SBY ...<1>y. P(e)BY ...<1>z. \E x \in S : P(x)BY <1>x, <1>yRegards,StephanOn 19 Nov 2022, at 14:15, Jaco van de Pol <jaco...@xxxxxxxxx> wrote:Hi,My "WITNESS x \in y" generates a proof obligation, so it would be nice towrite WITNESS x\in y BY <proof>, but as far as I understand this is notpossible. Is there a reason? Is there a general work around?Thanks for your thoughts,

Jaco van de Pol--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57a329dc-6578-4235-ad56-a579e35c2234n%40googlegroups.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/5ae6ca5e-e749-4373-afce-13ceea4655a1n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] WITNESS BY***From:*Stephan Merz

**References**:**[tlaplus] WITNESS BY***From:*Jaco van de Pol

**Re: [tlaplus] WITNESS BY***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] WITNESS BY** - Next by Date:
**Re: [tlaplus] WITNESS BY** - Previous by thread:
**Re: [tlaplus] WITNESS BY** - Next by thread:
**Re: [tlaplus] WITNESS BY** - Index(es):