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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 30 Mar 2023 18:25:35 +0200*References*: <a754d530-0927-4337-bff3-3e51e7ea5b55n@googlegroups.com>

If the solvers don’t figure out the witness term for existential goals, you can help by writing WITNESS e \in Nat which transforms the goal \E x \in Nat : P(n) to proving P(e). Note that WITNESS doesn’t take a proof. If it isn’t completely obvious, add a preliminary step that shows e \in Nat. Stephan On 30 Mar 2023, at 18:04, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote: -- 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/FF11075D-DF25-4700-957D-C01C8597F581%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Optimizing proof check time***From:*Andrew Helwer

**References**:**Re: [tlaplus] Optimizing proof check time***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Optimizing proof check time** - Next by Date:
**[tlaplus] Is there any way to typeset the a % b operator as \pmod{b}?** - Previous by thread:
**Re: [tlaplus] Optimizing proof check time** - Next by thread:
**Re: [tlaplus] Optimizing proof check time** - Index(es):