Go up to TopGo forward to Invariance Properties |

- Program
*P*:**var natural***x*,*y*= 0**do**

<**true**->*x*:=*x+1*>

[]

<**true**->*y*:=*y+1*>**od**

- TLA Formula
`Phi`:`Init`_{Phi}*<=>**(x=0)**and**(y=0)*`A`_{1}*<=>**(x' = x+1)**and**(y' = y)*`A`_{2}*<=>**(y' = y+1)**and**(x' = x)*`A`*<=>*`A`_{1}*or*`A`_{2}`Phi`*<=>*`Init`_{Phi}*and*`always`[`A`]_{<x, y>}

*and*WF(_{<x, y>}`A`)_{1}*and*WF(_{<x, y>}`A`)_{2}

- Program
*P*has property*F*:`Phi`*=>**F*

Author: Wolfgang Schreiner

Last Modification: May 14, 1998