- Eventually (
`eventually`)- $F$ is eventually true.
`eventually`$F$ $<=>$*not*`always`*not*$F$.- <$s$
_{0}, $s$_{1}, ...>[[`eventually`$F$]] $<=>$

*exists*$n$ in**Nat**: <$s$_{n}, $s$_{n+1}, ...>[[$F$]]

- Infinitely Often (
`always``eventually`)- <$s$
_{0}, $s$_{1}, ...>[[`always``eventually`$F$]] $<=>$

*forall*$n$ in**Nat**:*exists*$m$ in**Nat**:

<$s$_{n+m}, $s$_{n+m+1}, ...>[[$F$]]

- <$s$
- Eventually Always (
`eventually``always`)- <$s$
_{0}, $s$_{1}, ...>[[`eventually``always`$F$]] $<=>$

*exists*$n$ in**Nat**:*forall*$m$ in**Nat**:

<$s$_{n+m}, $s$_{n+m+1}, ...>[[$F$]]

- <$s$
- Leads to ($|->$)
- $F$ $|->$ $G$ $<=>$
`always`($F$ $=>$`eventually`$G$) - Any time $F$ is true, $G$ is true then or at some later time.

- $F$ $|->$ $G$ $<=>$

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine $$