Go backward to Adding LivenessGo up to TopGo forward to Fairness |

`always`[`A`]is TLA formula._{f}*not*`always`[*not*`A`]_{f}*<=>*`eventually`*not*[*not*`A`]_{f}*<=>*`eventually`*not*(*not*`A`*or**f'=f*)*<=>*`eventually`(`A`*and**f'**notequal**f*)- <
`A`>_{f}*<=>*`A`*and**f'**notequal**f* - <
`A`>is TLA formula._{f}

- Reformulation of
`Phi`:`Phi`*<=>*`Init`_{Phi}*and*`always``A`_<*x, y*>

*and*`always``eventually`<`A`>_<_{1}*x, y*>*and*`always``eventually`<`A`>_<_{2}*x, y*>

Author: Wolfgang Schreiner

Last Modification: May 14, 1998