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

Question

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.

Answer 1

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