Go backward to Quantification over Flexible Variables
Go up to Top
Go forward to Refinement Mappings
Quantification in TLA
- Syntax:
- <general formula> <STLA formula>
| exists <flexible variable>: <general
formula>
| exists <rigid variable>: <general
formula>
| <general formula>and <general formula>
| not <general formula>
- Semantics:
- sigma[[exists : ]] exists rho, tau in St:
(sigma= rho) and (rho = tau)
and tau[[F]]
- sigma[[exists c: ]] exists c
in Val: sigma[[]]
- Proof rules:
- E1.
- E2.
,
not free in .
- F1.
- F2.
,
c not free in .
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine