Go backward to The Next-State RelationGo up to TopGo forward to Proving Psi Implements Phi |

`Psi`shall implement`Phi`.*x*and*y*must be incremented infinitely often.- Infinitely many
`A`and_{1}`A`steps must occur._{2}

- Assume only
`A`steps occur._{2} - Does WF
(_{w}`A`) rule out this?_{1}`Enabled``alpha`_{1}*<=>*(`pc`= "a")_{1}*and*(0 <`sem`).`alpha`is enabled and disabled infinitely often._{1}- <
`A`>_{1}is disabled infinitely often._{w} - WF
(_{w}`A`) still holds for this behavior!_{1}

- Does SF
(_{w}`A`) rule out this?_{1}- Either <
`A`>_{1}is eventually disabled forever, or infinitely many <_{w}`A`>_{1}steps occur._{w} - <
`A`>_{1}is enabled infinitely often._{w} - SF
(_{w}`A`) does not hold for this behavior!_{1}

- Either <

*Need strong fairness condition!*

Author: Wolfgang Schreiner

Last Modification: May 14, 1998