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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 29 Mar 2023 21:13:10 +0200*References*: <9003123c-4c17-4c5a-9338-42f79676fd4cn@googlegroups.com>

Like so: THEOREM TypeCorrect == Spec => []TypeOK THEOREM Invariance == Spec => []Invariant <1>1. Init => Invariant. \* you may add TypeOK on the left-hand side but it’s probably useless <1>2. TypeOK /\ Invariant /\ [Next]_v => Invariant’ <1>. QED BY <1>1, <1>2, TypeCorrect, PTL DEF Spec Appealing to the previously proved theorem TypeCorrect in the QED proof justifies the use of TypeOK in step <1>2. Stephan On 29 Mar 2023, at 19:27, 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/0F84EA38-DD0A-4E77-8D38-F88632900AD8%40gmail.com. |

**References**:**Re: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Resources for learning TLA+ proofs** - Next by Date:
**[tlaplus] Experience report: teaching TLA+ proofs to ChatGPT** - Previous by thread:
**RE: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.** - Next by thread:
**[tlaplus] Experience report: teaching TLA+ proofs to ChatGPT** - Index(es):