Go backward to
General Invariance Proofs
Go up to
Top
Go forward to
Eventuality Properties
More About Invariance Proofs
Use one invariance property to prove another.
Know
Phi
=>
always
T
.
Prove
Phi
=>
always
P
.
Application of rule INV2.
|-
always
I
=>
(
always
[
A
]
_{f}
<=>
always
[
A
and
I
and
I'
]
_{f}
)
Phi
<=>
Init
_{Phi}
and
always
[
A
and
T
and
T'
]
_{<x, y>}
and
WF
_{<x, y>}
(
A
_{1}
)
and
WF
_{<x, y>}
(
A
_{2}
)
Can substitute
A
and
T
and
T'
instead of
A
for
A
in INV1.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998