Proof of Simple Properties About Terms, Position of Subterms and Replacement of Subterms
Item 2. If $p \in Pos(s)$ and $q \in Pos(t)$:
2.1 $(s[t]_{p})|_{pq} = t|_{q}$.
We prove by induction on the length of $p$:
Case $p = \epsilon$:
$(s[t]_{\epsilon})|_{\epsilon q} = t|_{\epsilon q} = t|_{q}$.
Case $p = ip'$:
$(s[t]_{ip'})|_{ip'q} = f(s_1, \ldots, s_i[t]_{p'}, \ldots, s_n)|_{ip'q} = (s_{i}[t]_{p'})|_{p'q}$. By induction hypothesis, $(s_{i}[t]_{p'})|_{p'q} = t|_{q}$.
2.2 $(s[t]_{p})[r]_{pq} = s[t[r]_{q}]_{p}$.
We prove by induction on the length of $p$:
Case $p = \epsilon$:
Notice that $(s[t]_{\epsilon})[r]_{\epsilon q} = t[r]_{q}$ and also that: $s[t[r]_{q}]_{\epsilon} = t[r]_{q}$.
Case $p = ip'$:
$(s[t]_{ip'})[r]_{ip'q} = f(s_1, \ldots, s_{i}[t]_{p'}, \ldots, s_n)[r]_{ip'q} = f(s_1, \ldots, (s_{i}[t]_{p'})[r]_{p'q}, \ldots, s_n)$. By induction hypothesis,
$$(s_{i}[t]_{p'})[r]_{p'q} = s_i[t[r]_{q}]_{p'}$$
and hence $f(s_1, \ldots, (s_{i}[t]_{p'})[r]_{p'q}, \ldots, s_n) = f(s_1, \ldots, s_i[t[r]_{q}]_{p'}, \ldots, s_n) = s[t[r]_{q}]_{ip'}$.
Item 3. If $pq \in Pos(s)$, then :
3.1 $(s[t]_{pq})|_{p} = (s|_{p})[t]_{q}$.
We prove by induction on the length of $p$:
Case $p = \epsilon$:
notice that $(s[t]_{\epsilon q})|_{\epsilon} = s[t]_{q}$ and also that $(s|_{\epsilon})[t]_{q} = s[t]_{q}$.
Case $p = ip'$:
$(s[t]_{ip'q})|_{ip'} = f(s_1, \ldots, s_{i}[t]_{p'q}, \ldots, s_n)|_{ip'} = (s_{i}[t]_{p'q})|_{p'}$. By induction hypothesis:
$$(s_{i}[t]_{p'q})|_{p'} = (s_{i}|_{p'})[t]_{q}$$
But $(s|_{ip'})[t]_{q} = (s_{i}|_{p'})[t]_{q}$ and thus the result holds.
3.2 $(s[t]_{pq})[r]_{p} = s[r]_{p}$.
We prove by induction on the length of $p$:
Case $p = \epsilon$:
$(s[t]_{\epsilon q})[r]_{\epsilon} = r = s[r]_{\epsilon}$.
Case $p = ip'$:
$(s[t]_{ip'q})[r]_{ip'} = f(s_1, \ldots, s_{i}[t]_{p'q}, \ldots, s_n)[r]_{ip'q} = f(s_1, \ldots, (s_{i}[t]_{p'q})[r]_{p'}, \ldots, s_n)$. By induction hypothesis:
$$(s_{i}[t]_{p'q})[r]_{p'} = s_{i}[r]_{p'} $$
and therefore we have $f(s_1, \ldots, (s_{i}[t]_{p'q})[r]_{p'}, \ldots, s_n) = f(s_1, \ldots, s_{i}[r]_{p'}, \ldots, s_n) = s[r]_{ip'}$.
Item 4. If $p$ and $q$ are parallel positions in $s$ (i.e. $p || q$), then
4.1 $(s[t]_{p})|_{q} = s|_{q}$
We prove by induction on the length of $p$:
Case $p = \epsilon$: This case can't happen, as $p$ and $q$ would not be parallel positions.
Case $ p  = ip'$:
We now prove this by induction on the length of $q$.
If $q = \epsilon$:

This can't happen, as $p$ and $q$ would not be parallel positions.

If $q = jq'$:

There are two possibilities, according to whether $i = j$ or not.
Case $i = j$:

$(s[t]_{ip'})|_{iq'} = f(s_1, \ldots, s_{i}[t]_{p'}, \ldots, s_{n})|_{iq'} = (s_{i}[t]_{p'})|_{q'}$. We have that $p'$ and $q'$ are parallel positions and thus, by induction hypothesis:
$$(s_{i}[t]_{p'})|_{q'} = s_{i}|_{q'}.$$
Since we also have $s|_{iq'} = s_{i}|_{q'}$ the result holds.

Case $i \neq j$:

Let's suppose without loss of generality that $i &gt; j$. Then:
$$(s[t]_{ip'})|_{jq'} = f(s_1, \ldots, s_{j}, \ldots, s_{i}[t]_{p'}, \ldots, s_{n})|_{jq'} = s_{j}|_{q'}.$$
Since we also have $s|_{jq'} = s_{j}|_{q'}$ the result holds.


4.2 $(s[t]_{p})[r]_{q} = (s[r]_{q})[t]_{p}$:
Case $p = \epsilon$: This case can't happen, as $p$ and $q$ would not be parallel positions.
Case $ p  = ip'$:
We now prove this by induction on the length of $q$.
If $q = \epsilon$:

This can't happen, as $p$ and $q$ would not be parallel positions.

If $q = jq'$:

There are two possibilities, according to whether $i = j$ or not.
Case $i = j$:

$(s[t]_{ip'})[r]_{iq'} = f(s_1, \ldots, s_{i}[t]_{p'}, \ldots, s_n)[r]_{iq'} = 
f(s_1, \ldots, (s_{i}[t]_{p'})[r]_{q'}, \ldots, s_n)$.
We have that $p'$ and $q'$ are parallel positions and thus, by induction hypothesis:
$$ (s_{i}[t]_{p'})[r]_{q'} = (s_{i}[r]_{q'})[t]_{p'} $$
and hence $$f(s_1, \ldots, (s_{i}[t]_{p'})[r]_{q'}, \ldots, s_n) = f(s_1, \ldots, (s_{i}[r]_{q'})[t]_{p'} , \ldots, s_n)= f(s_1, \ldots, s_{i}[r]_{q'}, \ldots, s_n)[t]_{ip'} = (s[r]_{q})[t]_{p}.$$

Case $i \neq j$:

Let's suppose without loss of generality that $i &gt; j$. Then:
$$(s[t]_{ip'})[r]_{jq'} = f(s_1, \ldots, s_{j}, \ldots, s_{i}[t]_{p'}, \ldots, s_n)[r]_{jq'} = f(s_1, \ldots, s_{j}[r]_{q'}, \ldots, s_{i}[t]_{p'}, \ldots, s_n) = f(s_1, \ldots, s_{j}[r]_{q'}, \ldots, s_{i}, \ldots, s_n)[t]_{ip'} = (s[r]_{jq'})[t]_{ip'}.$$