|
|
|---|
|
|
|
|---|
The condition in which all the variable names are distinct.
The
Here we capture this uniqueness property for variables; the uniqueness property for functions is captured in unique-functions. We formalize this property via ACL2 functions on statements, blocks, etc. that take as arguments the variable names encountered so far, check that the names of the variables introduced by the statement (or block etc.) are not among those, and update the set of encountered variable names with the names of the introduced variables. Thus, the set of variable names encountered so far is threaded through. We do not need to define any ACL2 functions on expressions, in order to capture this property, because expressions do not introduce new variables.