### LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INSTANCE

a brief explanation of substitution instances
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

Let *p* and *q* be terms or formulas (there is no difference in ACL2).
Then we say *p* is an *instance* or *substitution instance*
of *q* if and only if *p* can be obtained from *q* by uniformly
replacing the variables of *q* by terms. Sometimes we call *p* the
*target* and *q*
the *pattern* because by choosing appropriate replacements we can make
the pattern *match* many different targets.

For example, the following *target* is an instance of the given *pattern*:

*target*: (APP (APP (REV A) (REV B)) (REV C))
*pattern*: (APP (APP x y ) (REV z))

The replacement or *substitution* used in this match of the pattern to the
target is:

*variable in pattern* *replacement term*
x (REV A)
y (REV B)
z C

Such substitutions are usually written this way in ACL2:
((x (REV A))
(y (REV B))
(z C)).

Please use your browser's **Back Button** to return to the page that mentioned
``instance.''