rlbvarl – list of bound variables

## Calling Sequence

rlbvarl \((\,\varphi\,)\)

## Arguments

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

## Returns

\(L\) | — | list of variables |

## Description

Returns the set of all variables that have a bound 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 *bound* occurrence is an occurrence within 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

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

## See Also