This new documentation in under construction. For functions
not covered yet, please use the
old documentation.
rlex – existential closure
Calling Sequence
rlex \((\,\varphi\,)\)
rlex \((\,\varphi\,,\ L\,)\)
Arguments
| \(\varphi\) | — | first-order formula |
| \(L\) | — | list of variables |
Returns
| \(\varphi′\) | — | first-order formula |
Description
Existentially quantify all variables with free occurrences inside \(\varphi\). The optional argument \(L\) is an exception list, i.e., variables in \(L\) remain unquantified.
For positively specifying a list of variables to be quantified use the existential quantifier ex with the corresponding list as its first argument.
Examples
rlex(a=0 and b=0 and all(a, ex({c, d}, c > a and a > b and b > d), {b});
See Also