Subformula occurrence
= Subformula occurrence
A <subformula occurrence> specifies a particular position in the <syntax tree of a formula>. Two occurrences can contain the same <logical formula> while being different nodes. Replacement of one occurrence does not necessarily replace the others.