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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 4 Apr 2020 14:42:20 +0200*References*: <50d348f8-4b04-43d6-98bd-5045540ca1d6@googlegroups.com>

Hello, (1) Spec => \EE p : SpecUP As a trivial example, consider defining PredSend(f) == FALSE With that definition, you can still show that (2) SpecUP => SS!Spec holds but you wouldn't be able to conclude Spec => SS!Spec because you don't have (1). This is explained in more detail in section 4.5. 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/10D23B2C-C1F1-419D-A3C1-CD16C78A75CD%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] on prophecy variables***From:*Alex Tim

**References**:**[tlaplus] on prophecy variables***From:*Alex Tim

- Prev by Date:
**[tlaplus] on prophecy variables** - Next by Date:
**Re: [tlaplus] on prophecy variables** - Previous by thread:
**[tlaplus] on prophecy variables** - Next by thread:
**Re: [tlaplus] on prophecy variables** - Index(es):