|
|
|---|
|
|
|
|---|
Notion of second-order theorem.
A second-order theorem is an ACL2 theorem
that
The second-order theorem is universally quantified
over the function variables that it depends on.
These function variables may be replaced by functions of matching arities,
obtaining a new theorem that is an
Including in the name of a second-order theorem, between square brackets (in any order), the function variables that the theorem depends on, as in the examples in the SOFT documentation pages, makes the dependency more explicit when referencing the theorem. This naming convention may arise naturally when the name of the theorem includes names of second-order functions that follow the naming convention described in second-order-functions, or it may be explicitly followed when choosing the name of the theorem. However, SOFT does not enforce this naming convention.