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

rlvarl – list of bound variables

## Calling Sequence

rlvarl \((\,\varphi\,)\)

## Arguments

\(\varphi\) | — | first-order formula |

## Returns

\(\{L_f,\ L_b\}\) | — | \(\{\)list of variables, list of variables\(\}\) |

## Description

Returns a pair of two lists \(L_f\) and \(L_b\), which are the sets of all variables that have a free or bound occurrence in \(\varphi\), respectively. Both \(L_f\) and \(L_b\) are sorted according to the Reduce kernel order.

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

Unless the formula is prenex it is possible to have \(L_f \cap L_b \neq \emptyset.\)

## Example

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

## See Also

- rlbvarl — list of bound variables
- rlfvarl — list of free variables
- rlqvarl — list of quantified variables