Go backward to Rigid Variables and QuantifiersGo up to TopGo forward to Simple Temporal Logic |

`Enabled``A`- True for
*s*iff it is possible to take an`A`step starting in*s*. *s*[[`Enabled``A`]]*<=>**exists**t*in**St**:*s*[[`A`]]*t*

- True for
- Syntactic definition
*v*all (flexible) variables in_{i}`A`.`Enabled``A`*<=>*

*exists*`c`, ...,_{1}`c`:_{n}`A`(`c`/_{1}*v'*, ...,_{1}`c`/_{n}*v'*)._{n}`Enabled`(*y*= (*x'*)+^{2}`n`) =

*exists*`c`:*y*=`c`+^{2}`n`

- If
`A`represents actomic operation,`Enabled``A`is true for those states in which it is possible to perform the operation.

Author: Wolfgang Schreiner

Last Modification: May 14, 1998