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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 14 Jul 2020 14:25:12 +0200*References*: <fd2059df-06ce-475a-89d3-3acf3781c665n@googlegroups.com>

Hello, this is not provable unless you assume that the values y[i] are numbers (for i \in DOMAIN y). For example, we don't know if {} + 1 = {} or not. You should be able to prove THEOREM ASSUME y \in [DOMAIN y -> Nat], inc PROVE \A i \in DOMAIN y : y'[i] # y[i] In typical reasoning about specifications, one includes a typing invariant that provides such information. 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/213FC0B5-D2FC-4A59-A703-5D38C5AE615C%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] Requesting help with TLAPM proof***From:*Swee Warman

- Prev by Date:
**[tlaplus] Requesting help with TLAPM proof** - Next by Date:
**Re: [tlaplus] Requesting help with TLAPM proof** - Previous by thread:
**[tlaplus] Requesting help with TLAPM proof** - Next by thread:
**Re: [tlaplus] Requesting help with TLAPM proof** - Index(es):