that condition is necessary for proving
(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.
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.