Originally Posted by

**emakarov** First, I should note that I encountered the term "substitution" only when a variable occurring in a syntactic expression is replaced by another expression. For example, if E = x^2 = x + 1 and ϴ = [x ↦ 2 + 3] is substitution, then Eϴ = (2 + 3)^2 = (2 + 3) + 1. It is customary to denote substitutions by Greek letters and denote the result of the application by Eϴ or ϴ(E).

Let u range over elements of L and w range over subsets of L. We can identify the set of substitutions A with L x L, i.e., the set of pairs of elements of L, and B with the set of functions from L to L. If f ∊ B and w ⊆ L, it is customary to denote {f(u) | u ∊ w} by f[w].

So, let y ∊ Y and s ∊ S. Define y | s, or s(y), to be

{<a', f[w]> | <a, w> ∊ y, <<a, a'>, f> ∊ s} ∪

{<a, w> | <a, w> ∊ y, <<a, a'>, f> ∉ s for all a', f}.

The second set in the union corresponds to those pairs x whose first element is not subject to a substitution from y, if this is possible. To prove that y | s is well-defined one has to show that it is impossible that <a, w> ∊ y and <<a, a'>, f'> ∊ s, <<a, a''>, f''> ∊ s for a' ≠ a'' or f' ≠ f''.