 Subterm

A subterm of a first-order term is a term appearing at a node of its syntactic tree, including the whole term. Recursively, a variable or constant has only itself as a subterm; the subterms of $f(t_1,\dots ,t_n)$ are the full term together with every subterm of every $t_i$. A proper subterm excludes the full term.

For $t=f(g(x),g(x))$, the distinct subterms are $t$, $g(x)$ and $x$. The subterm $g(x)$ occurs twice, so a subterm value and a subterm occurrence are different notions. Replacing a particular occurrence requires its position in the tree, not only its text.

The subterm relation organizes structural induction, recursive evaluation and term rewriting. Every proper subterm has smaller syntactic size in the usual finite term grammar, so recursive definitions can terminate by descending through the tree. A substring of printed notation is not automatically a subterm: the tree structure determines which expressions are complete terms.