Constant atomic terms and non-variable operators must be declared before being used in a theory. We will see below that it is permitted and sometimes important to declare variable operators. It is neither necessary nor possible to declare free or bound variables.
Equational axioms can be introduced by a simple command exhibited below in the first example. There are more complex commands discussed below for introducing constants and operators by definition.