# Proof of Simple Properties About Terms, Position of Subterms and Replacement of Subterms

I am studying term rewriting by reading Baader/Nipkow's book: "Term Rewriting and All That".

I want to prove a lemma about terms, position of subterms and replacement of subterms. The notation is as follows:

$$s|_{p}$$ denotes the subterm of $$s$$ at position $$p$$.
$$s[t]_{p}$$ denotes the term obtained from $$s$$ by replacing the subterm at position $$p$$ by $$t$$.

The lemma I want to prove is:

Lemma 3.1.4 Let $$s, t, r$$ be terms and $$p, q$$ be strings over the positive integers.

1. If $$pq \in Pos(s)$$, then $$s|_{pq} = (s|_{p})|_{q}$$.

2. If $$p \in Pos(s)$$ and $$q \in Pos(t)$$, then

2.1 $$(s[t]_{p})|_{pq} = t|_{q}$$

2.2 $$(s[t]_{p})[r]_{pq} = s[t[r]_{q}]_{p}$$

3. If $$pq \in Pos(s)$$, then

3.1 $$(s[t]_{pq})|_{p} = (s|_{p})[t]_{q}$$

3.2 $$(s[t]_{pq})[r]_{p} = s[r]_{p}$$.

4. If $$p$$ and $$q$$ are parallel positions in $$s$$ (i.e. $$p || q$$), then

4.1 $$(s[t]_{p})|_{q} = s|_{q}$$

4.2 $$(s[t]_{p})[r]_{q} = (s[r]_{q})[t]_{p}$$

The book provides proof for the first item:

As an example, we show, by induction on the length of $$p$$ that $$s|_{pq} = (s|_{p})|_{q}$$ holds for all $$pq \in Pos(s)$$.

For $$p = \epsilon$$, we have $$pq = q$$, and thus $$s|_{pq} = s|_{q}$$. In addition, $$p = \epsilon$$ implies $$s|_{p} = s$$, which shows $$s|_{q} = (s|_{p})|_{q}$$.

Now assume that $$p = ip'$$. Because $$ip'q \in Pos(S)$$, we know that $$s$$ is of the form $$s = f(s_1, \ldots, s_n)$$ with $$i \leq n$$. By definition, $$s|_{pq} = s|_{ip'q} = s_{i}|_{p'q}$$, and by induction $$s_{i}|_{p'q} = (s_{i}|_{p'})|_{q}$$. Again, by definition, we obtain $$s_{i}|_{p'} = s|_{ip'} = s|_{p}$$, which finishes the proof of the induction step.

I want to prove that the other items are also true. I wrote my attempt as an answer, but of course, I welcome other solutions or feedback. Thanks in advance.

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 > 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 > 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'}.$$