Go backward to Eventuality PropertiesGo up to TopGo forward to Other Properties |

- 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`and_{1}`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