Go backward to
The Fairness Requirement
Go up to
Top
Go forward to
Proof of Fairness
Proving
Psi
Implements
Phi
Prove
Psi
=>
Phi
Init
_{Psi}
=>
Init
_{Phi}
always
[
A
]
_{w}
=>
always
[
A
]
_{<x,y>}
Psi
=>
WF
_{<x,y>}
(
A
_{1}
)
and
WF
_{<x,y>}
(
A
_{2}
)
Proof of Step Simulation:
[
A
]
_{w}
=>
[
A
]
_{<x,y>}
[
A
]
_{w}
<=>
alpha
_{1}
or
...
or
gamma
_{2}
or
(
w'
=
w
)
beta
_{1}
=>
A
_{1}
beta
_{2}
=>
A
_{2}
(<
x
,
y
>' = <
x
,
y
>) for all others.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998