Go backward to Formal Specification (Contd)
Go up to Top
Go forward to Quantification over Flexible Variables
Quantification over Flexible Variables
- exists :
- Flexible variable .
- There exists values for such that holds.
- Auxiliary definitions:
- = : states and assign same values to all variables
other than .
- = forall '' notequal '' [[]] =
[[]]
- <, , ...> = <, ,
...> forall in Nat: =
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine