 The axioms are all formulas of the following forms, where in the last two schemas the subformula \(A(t)\) is the result of substituting an occurrence of the term \(t\) for every free occurrence of \(x\) in \(A(x),\) and no variable free in \(t\) becomes bound in \(A(t)\) as a result of the substitution.