Go backward to
Eventuality Properties
Go up to
Top
Go forward to
Other Properties
Example
Prove WF1
P
<-
n
in
Nat
and
x
=
n
Q
<-
x
=
n
+1
A
<-
A
,
A
<-
A
1
,
f
<- <
x
,
y
>
Hypotheses:
(
n
in
Nat
and
x
=
n
)
and
[
A
]
<x, y>
=>
((
n
in
Nat
and
x'
=
n
)
or
(
x'
=
n
+1))
(
n
in
Nat
and
x
=
n
)
and
<
A
1
>
<x, y>
=>
(
x'
=
n
+1))
(
n
in
Nat
and
x
=
n
)
and
<
A
1
>
<x, y>
=>
Enabled
<
A
1
>
<x, y>
From definitions of
A
1
and
A
.
Conclusion:
always
[
A
]
<x, y>
and
WF
<x, y>
(
A
1
)
=>
((
n
in
Nat
and
x
=
n
)
|->
(
x
=
n
+1))
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998