 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.