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