# Redlog Documentation Center

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

rlfvarl – list of free variables

## Calling Sequence

rlfvarl $$(\,\varphi\,)$$

## Arguments

 $$\varphi$$ — first-order formula

## Returns

 $$L$$ — list of variables

## Description

Returns the set of all variables that have a free occurrence in $$\varphi$$ as a list. $$L$$ is sorted according to the Reduce kernel order.

An occurrence of a variable is an occurrence inside an atomic formula. A free occurrence is an occurrence outside the scope of a corresponding quantifier. Note that by this definition, variables that are quantified but do not appear in any atomic formulas do not occur at all.

## Example

 rlfvarl(ex({w, x, y, z}, v=0 and x=0 and y=0) and w=0 and y=0);