# Re: [tlaplus] Why is this an invalid TLA formula?

(Temporal) formulas are inductively defined as

- state predicates,
- [][A]_v and <> <<A>>_v for an action A and a state formula v,
- Boolean combinations of temporal formulas,
- []F and <>F for temporal formulas (and the derived forms F ~> G, WF_v(A), SF_v(A)),
- \E x : F, \A x : F, \EE v : F, \AA v : F,
- F -+-> G

It follows from the above that

[]<>( <<A>>_v \/ <<B>>_v )

is simply not a syntactically well-formed formula of TLA whereas

[]<> << A \/ B >>_v

is. If the first one were a formula, the two were semantically equivalent.

Hope this helps,
Stephan

> On 11 Jan 2017, at 13:32, George Singer <george....@xxxxxxxxx> wrote:
>
> At the top of page 95 of *Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers*, Lamport states that
>
> $$> \Box \Diamond ( \langle A \rangle_v \vee \langle B \rangle_v) >$$
>
> is not a valid TLA formula, even though its equivalent formulation
>
> $$> \Box \Diamond \langle A \vee B \rangle_v >$$
>
> *is* a valid TLA formula.
>
> **Question:** Why is the first formula invalid and the second formula valid?
>
> --
> 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+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.