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

*From*: ns <nedsri1988@xxxxxxxxx>*Date*: Fri, 28 May 2021 20:51:09 -0700 (PDT)*Ironport-hdrordr*: A9a23:4aJL4q4nynvCpYYK1gPXwNPXdLJyesId70hD6qkXc3xom62j9vxG885w6faZskdyZJhCo7690de7MBDhHPdOiOF7AV7IZmXbUQWTQb2KobGM/wHd

hello, the Specifying Systems book says that a regular existentially quantified variable functions as a constant. And from the definition this does seem to be the case

\sigma |= (\E x: F) == \E x: (\sigma |= F)

where \sigma is a trace. However, if I have

[] (\E x: F)

its now possible for each state of \sigma to have a different value of x and satisfy this formula. But this now seems closer to a temporal existential. So would it be equivalent to

\EE x: [] F

?

thanks

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/c52798d7-3a1f-4ebd-9025-2a1afa8b3b46n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Q about the existential quantifier***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+** - Next by Date:
**Re: [tlaplus] Q about the existential quantifier** - Previous by thread:
**Re: [tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+** - Next by thread:
**Re: [tlaplus] Q about the existential quantifier** - Index(es):