Terms and Boolean terms are defined as before. The free variables of terms and guards are defined inductively, as in first-order logic. Notice that a bounded quantifier implicitly contains an atomic declaration.
As usual, every guard g is equivalent to a guard g' where no variable is both bound and free and where different quantifier occurrences bind different variables. To reduce g to g' , iterate the following transformation: Select an innermost quantifier q whose variable v occurs outside the scope of q and then replace v with a fresh variable in the scope of q .