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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 28 Nov 2023 19:47:57 +0100*References*: <0cda95d7-7d8a-4ce3-b8b4-b4f761e363fdn@googlegroups.com>

You are exploring mostly uncharted territory here, and I encourage you to file this as an issue on GitHub so that it won't get lost. Logically, your proof should only rely on a state-level assumption, i.e. you should be able to prove ASSUME terminate = TRUE PROVE (ENABLED <<NextDown>>_cvars => ENABLED <<CNext>>_cvars) which implies your actual proposition. But I see why you find it unwieldy that the proof fails with temporal-level hypotheses. 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/FC9E59E1-949E-48AE-9E8D-09947BD07A98%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1***From:*Ramon Snir

- Prev by Date:
**[tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1** - Next by Date:
**Re: [tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1** - Previous by thread:
**[tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1** - Next by thread:
**Re: [tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1** - Index(es):