Go backward to Temporal FormulasGo up to TopGo forward to Validity and Provability |

- 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*]]

- <
- 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*]]

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

Author: Wolfgang Schreiner

Last Modification: May 14, 1998