Go backward to
The Basic Rules of TLA
Go up to
Top
Additional Rules
WF2.
<
A
and
A
>
f
=>
<
A
>
g
P
and
P'
and
<
A
and
A
>
f
and
Enabled
<
A
>
g
=>
A
P
and
Enabled
<
A
>
g
=>
Enabled
<
A
>
f
always
[
A
and
not
A
]
f
and
WF
f
(
A
)
and
always
F
and
eventually
always
Enabled
<
A
>
g
=>
eventually
always
P
always
[
A
]
f
and
WF
f
(
A
)
and
always
F
=>
WF
g
(
A
)
SF1.
P
and
[
A
]
f
=>
(
P'
or
Q'
)
P
and
<
A
and
A
>
f
=>
Q'
always
P
and
always
[
A
]
f
and
always
F
=>
eventually
Enabled
<
A
>
f
always
[
A
]
f
and
SF
f
(
A
)
and
always
F
=>
(
P
|->
Q
)
SF2.
<
A
and
A
>
f
=>
<
A
>
g
P
and
P'
and
<
A
and
A
>
f
=>
A
P
and
Enabled
<
A
>
g
=>
Enabled
<
A
>
f
always
[
A
and
not
A
]
f
and
SF
f
(
A
)
and
always
F
and
always
eventually
Enabled
<
A
>
g
=>
eventually
always
P
always
[
A
]
f
and
SF
f
(
A
)
and
always
F
=>
SF
g
(
A
)
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998