Go backward to Formal Specification (Contd)Go up to TopGo forward to Quantification over Flexible Variables |

*exists**x*:*F*- Flexible variable
*x*. - There exists values for
*x*such that*F*holds.

- Flexible variable
- Auxiliary definitions:
*s*=_{x}*t*: states*s*and*t*assign same values to all variables other than*x*.*s*=_{x}*t**<=>**forall*'*v*'*notequal*'*x*'*s*[[*v*]] =*t*[[*v*]]- <
*s*,_{0}*s*, ...> =_{1}<_{x}*t*,_{0}*t*, ...>_{1}*<=>**forall**n*in**Nat**:*s*=_{n}_{x}*t*_{n}

Author: Wolfgang Schreiner

Last Modification: May 14, 1998