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 CSuch 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.''
