| | | A.2.4 Quantified Formulas |
FORALL(I1:T1, I2:T2,
..., In:Tn): E
EXISTS(I1:T1, I2:T2,
..., In:Tn): E
These expressions represent universal and existential quantification, respectively. They are composed of identifiers I1 of type T1, I2 of type T2, ..., In of type Tn and a value E of type BOOLEAN (in which I1, I2, ..., In may freely occur) and have themselves type BOOLEAN.
If quantified expressions occur in the context of another expression, they must be put into parentheses, as e.g. the EXISTS formula in
FORALL(x:NAT): x > 0 => (EXISTS(y:NAT): y+1=x)
For multiple parameters with the same type, the parameter type needs to be declared only once, thus it is for example legal to write
FORALL(x,y:NAT, z:INT): x+y >= 0*z
| | | A.2.4 Quantified Formulas |