If formula "x := 5" is activated in a computation involving a quantifier that binds variable "x", then the bound variable "x" is replaced by 5, resulting in "VAR$[5]".
This seems to happen in the computation of the quantifier, hence it can only be experienced if the quantifier can actually be computed.
If formula "x := 5" is activated in a computation involving a quantifier that binds variable "x", then the bound variable "x" is replaced by 5, resulting in "VAR$[5]". This seems to happen in the computation of the quantifier, hence it can only be experienced if the quantifier can actually be computed.