Formal definition of string-to-term substitution Forgive me if this question seems elementary. Let L be a nonempty alphabet. We have an intuitive notion of substituting words for letters in a word. For example, substituting 'cd' for 'b' in the word 'bab' results in 'cdacd'. And, in the word 'aad', the substitution would result in 'aad'. We also have a notion of simultaneous substitution. For example, substituting  'bb' for 'a' and simultaneously 'aa' for 'b' in the word 'ab' results in 'bbaa'. Now I can set up the question. How is simultaneous substitution formally defined? More precisely, if some set of letters S is mapped to a set of words W, how is the simultaneous substitution of S to W defined for all words over L? I have looked on the internet, but haven't found a formal definition.

Let $f$ be the given function from some set $S$ of letters to a set $W$ of words.  The "substitute according to $f$" function $g$ from words to words can be defined by recursion on the length of the input words as follows:
$g$ maps the empty word to itself.
If $w$ is $u^\frown x$, where $u$ is a word and $x$ is a letter in $S$ (and ${}^\frown$ means concatenation), then $g(w)=g(u)^\frown f(x)$.
If $w$ is $u^\frown x$, where $u$ is a word and $x$ is a letter not in $S$, then $g(w)=g(u)^\frown x$.
