|
|
|---|
|
|
|
|---|
The condition in which all the function names are distinct.
The
Here we capture this uniqueness property for functions; the uniqueness property for variables is captured in unique-variables. We formalize this property via ACL2 functions on statements, blocks, etc. that take as arguments the function names encountered so far, check that the names of the functions introduced by the statement (or block etc.) are not among those, and update the set of encountered function names with the names of the introduced functions. Thus, the set of function 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 functions.