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