Go backward to FairnessGo up to TopGo forward to Examining Formula Phi |

- Machine-closed
- Pair (
`Init`*and*`always`[`A`],_{f}*F*) is machine-closed*<=>*`Init`*and*`always`[`A`]_{f}*and**F*does not add additional safety properties. - If
*F*is conjunciton of conditions WF(_{f}`A`) and/or SF(_{f}`A`), where each <`A`>implies_{f}`A`, then`Init`*and*`always`[`A`]_{v}*and**F*is machine-closed.

- Pair (
- Fairness requirements:
- Rewrite
`always``eventually`<`A`>_<_{1}*x, y*>*and*`always``eventually`<`A`>_<_{2}*x, y*> as fairness conditons. `Enabled`<`A`>_<_{1}*x, y*> =`Enabled`<`A`>_<_{2}*x, y*> =**true**- WF_<
*x, y*>(`A`) =_{1}`always``eventually`<`A`>_<_{1}*x, y*>

WF_<*x, y*>(`A`) =_{2}`always``eventually`<`A`>_<_{2}*x, y*> `Phi`*<=>*`Init`_{Phi}*and*`always``A`_<*x, y*>

*and*WF_<*x, y*>(`A`)_{1}*and*WF_<*x, y*>(`A`)_{2}

- Rewrite

Author: Wolfgang Schreiner

Last Modification: May 14, 1998