### 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)).
```