# Redlog Documentation Center

This new documentation in under construction. For functions not covered yet, please use the old documentation.

rlall – universal closure

## Calling Sequence

rlall $$(\,\varphi\,)$$
rlall $$(\,\varphi\,,\ L\,)$$

## Arguments

 $$\varphi$$ — first-order formula $$L$$ — list of variables

## Returns

 $$\varphi′$$ — first-order formula

## Description

Universally 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 universal quantifier all with the corresponding list as its first argument.

## Examples

 rlall(a=0 or b=0 or all(a, ex({c, d}, c > a and a > b and b > d), {b});