# Redlog Documentation Center

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});