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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 25 Apr 2024 17:46:19 +0200*References*: <9811f409-94b8-42d4-b56b-2ff4b2739886n@googlegroups.com> <7D444807-747B-40F6-9AD9-EB3A203EADA3@gmail.com> <8bd4439d-7f5d-4e5d-b935-7c4d8b71b4ban@googlegroups.com>

The proof appearing at the beginning of appendix B of the paper you point to is checked by TLAPS, cf. also [1] that has 10 different versions of the proof that are all checked by TLAPS. The proof in Cantor10.tla is even more succinct than the one appearing in the paper. 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/AD9E4C7A-449E-435E-85AA-CEF15683D726%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] TLA and TLAPIS***From:*marta zhango

**References**:**[tlaplus] TLA and TLAPIS***From:*marta zhango

**Re: [tlaplus] TLA and TLAPIS***From:*Stephan Merz

**Re: [tlaplus] TLA and TLAPIS***From:*marta zhango

- Prev by Date:
**Re: [tlaplus] TLA and TLAPIS** - Next by Date:
**Re: [tlaplus] TLA and TLAPIS** - Previous by thread:
**Re: [tlaplus] TLA and TLAPIS** - Next by thread:
**Re: [tlaplus] TLA and TLAPIS** - Index(es):