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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 15 Apr 2020 17:11:02 +0200*References*: <a70545cd-37a0-430a-aad5-bc303a0f33e0@googlegroups.com>

1. Your algorithm is written in PlusCal, which appears as a comment to TLA+. You first need to generate the TLA+ specification (File -> Translate PlusCal Algorithm in the Toolbox). 2. Your theorem should then be stated as a consequence of the specification in the form THEOREM diagseq == Spec => (diag = tdiag) Its proof will look like "BY DEF Spec, Init". Note that your assertion only talks about the initial state. Regards, Stephan
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/3F9142EF-641E-4A04-8650-DFE1CAC46592%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Proving a Matrix Transpose***From:*christina . a . burge

**Re: [tlaplus] Proving a Matrix Transpose***From:*christina . a . burge

**References**:**[tlaplus] Proving a Matrix Transpose***From:*christina . a . burge

- Prev by Date:
**[tlaplus] Proving a Matrix Transpose** - Next by Date:
**Re: [tlaplus] Proving a Matrix Transpose** - Previous by thread:
**[tlaplus] Proving a Matrix Transpose** - Next by thread:
**Re: [tlaplus] Proving a Matrix Transpose** - Index(es):