the process of converting a clause to a term
The ACL2 prover represents its goals and subgoals as clauses, e.g., lists of terms treated as disjunctions. The
individual elements of a clause are called literals. For example a
goal printed as
To termify a clause containing multiple literals, we convert the
clause to a unit clause using
Applying an induction scheme to a clause containing multiple literals can produce an exponential number of cases. This does not happen if the clause is a unit clause. So the ACL2 induction mechanism sometimes termifies its goal clause before applying the induction scheme to shift the case-analysis burden to the rest of the prover.