I am familiarizing myself with the TLA. On the 7th page following definition of the "always" (also pronounced as "box") is given:
Right after the formal definition, informal explanation in plain English says following:
I am bothered with sentence:
The formula $<s_0, ...>[|F|]$ asserts that $F$ is true at time $0$ of this behavior, and $<s_n, ...>[|F|]$ asserts that it is true at time $n$.
According to the definition [|F|] deals with subbehaviors. That's what $\forall n \in \mathbb{Nat}: <s_n, s_{n+1}, s_{n+2}, ...>$ stands for - it defines the subbehavior of the original behavior $<s_0, s_1, s_2, ..., s_{n}, ...>$. According to my understanding, it does not deal with exact state $s_n$ at the moment $n$; hence, to my understanding, informal English description is not quite correct and it should have been phrased in the different way:
The formula $<s_0, s_1, s_2, ...>[|F|]$ asserts that $F$ is true starting from the state at time 0 and infinetely long onward, and $<s_n, s_{n+1}, s_{n+2}, ...>[|F|]$ asserts that it is true starting from the state at the time $n$ and infinetely long onward.
Am I right? If not, what am I missing?