关于术语的简单特性证明，子线的位置和替换子

Question

我正在通过阅读Baader / Nipkow的书来学习重写：“术语重写和所有这些”。

我想证明关于术语的引理，地点的位置和更换子。符号如下：

$ s | _ {p} $ 表示 $ s $ 的子项 $ p $ 。
$ s [t] _ {p} $ 表示从 $ s $ s $ s $ 的术语通过替换子项在position $ p $ by $ t $ 。

我要证明的引理是：

lemma 3.1.4 让 $ s，t，r $ 是术语和 $ p，q $ 在正整数上串。

1. 如果 $ pq \ in pos（s）$ ，则 $ s | _ {pq}= （s | _ {p}）| _ {q} $ 。

2. 如果 $ p \在pos（s）$ 和 $ q \中，在pos（t）$ ，然后

   2.1 $（s [t] _ {p}）| _ {pq}= t | _ {q} $

   2.2 $（s [t] _ {p}）[r] _ {pq}= s [t [r] _ {q} _ {p} $ < / span>

3. 如果 $ pq \ in pos（s）$ ，则

   3.1 $（s [t] _ {pq}）| _ {p}=（s | _ {p}）[t] _ {q} $

   3.2 $（s [t] _ {pq}）[r] _ {p}= s [r] _ {p} $ 。

4. 如果 $ p $ 和 $ q $ 是 $ s $ （即 $ p || q $ ），然后

   4.1 $（s [t] _ {p}）| _ {q}= s | _ {q} $

   4.2 $（s [t] _ {p}）[r] _ {q}=（s [r] _ {q}）[t] _ {p} $

本书为第一个项目提供了证明：

作为一个例子，我们通过诱导诱导 $ p $ $ s | _ {pq }=（s | _ {p}）| _ {q} $ 为所有 $ pq \的保存在pos（s）$ 中。

对于 $ p=epsilon $ ，我们有 $ pq= q $ ，因此< SPAN Class=“Math-Container”> $ S | _ {PQ}= s | _ {q} $ 。此外， $ p=epsilon $ 暗示 $ s | _ {p}= s $ ，哪个显示 $ s | _ {q}=（s | _ {p}）| _ {q} $ 。

现在假设 $ p= ip' $ 。因为 $ ip'q \中的pos（s）$ ，我们知道 $ s $ 是的form $ s= f（s_1，\ ldots，s_n）$ 使用 $ i \ leq n $ 。按定义， $ s | _ {pq}= s | _ {ip'q}= s_ {i} | _ {p'q} $ ，归纳 $ s_ {i} | _ {p'q}=（s_ {i} | _ {p'}）| _ {q} $ 。同样，根据定义，我们获得 $ s_ {i} | _ {p'}= s | _ {ip'}= s | _ {p} $ ，哪个完成归纳步骤的证明。

我想证明其他物品也是如此。我把我的尝试写着答案，但当然，我欢迎其他解决方案或反馈。提前致谢。

Answer 1

项目2.如果 $ p \ in pos（s）$ 和 $ q \在pos中（ t）$ ：

2.1 $（s [t] _ {p}）| _ {pq}= t | _ {q} $ 。
我们在<跨度类=“math-container”> $ p $ ：

中的长度上证明了诱导

案例 $ p=epsilon $ ：
$（s [t] _ {\ epsilon}）| _ {\ epsilon q}= t | _ {\ epsilon q}= t | _ {q} $ 。

案例 $ 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} $ 。通过归纳假设， $（s_ {i} [t] _ {p'}）| _ {p'q}= t | _ {q} $ 。< / p>

2.2 $（s [t] _ {p}）[r] _ {pq}= s [t [r] _ {q}] _ {p $ 。
我们在<跨度类=“math-container”> $ p $ ：

中的长度上证明了诱导

案例 $ p=epsilon $ ：
请注意， $（s [t] _ \ epsilon}）[r] _ {\ epsilon q}= t [r] _ {q} $ 以及： $ s [t [r] _ {q}= t [r] _ {q} $ 。

案例 $ 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）$ 。通过归因， $$（s_ {i} [t] _ {p'}）[r] _ {p'q}= s_i [t [r] _ {q} _ {p '} $$ 因此 $ 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'} $ 。

项目3.如果 $ pq \在pos中，则为：

3.1 $（s [t] _ {pq}）| _ {p}=（s | _ {p}）[t] _ {q} $ 。
我们在<跨度类=“math-container”> $ p $ ：

中的长度上证明了诱导

案例 $ p=epsilon $ ：
请注意， $（s [t] _ \ epsilon q}）| _ {\ epsilon}= s [t] _ {q} $ 以及 $（s | _ {\ epsilon}）[t] _ {q}= s [t] _ {q} $ 。

案例 $ 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'} $ 。通过诱导假设：

$$（s_ {i} [t] _ {p'q}）| _ {p'}=（s_ {i} | _ {p'}）[ t] _ {q} $$

但 $（s | _ {ip'}）[t] _ {q}=（s_ {i} | _ {p'}）[t] _ {q $ ，因此结果保持。

3.2 $（s [t] _ {pq}）[r] _ {p}= s [r] _ {p} $ 。
我们在<跨度类=“math-container”> $ p $ ：

中的长度上证明了诱导

案例 $ p=epsilon $ ：
$（s [t] _ \ epsilon q}）[r] _ {\ epsilon}= r= s [r] _ {\ epsilon} $ 。< / p>

案例 $ 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）$ 。通过诱导假设：

$$（s_ {i} [t] _ {p'q}）[r] _ {p'}= s_ {i} [r] _ {p' $$

因此，我们有 $ 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'} $ 。

项目4.如果 $ p $ 和 $ q $ 是<跨越类=“math-container”> $ s $ （即 $ p || q $ ），然后

4.1 $（s [t] _ {p}）| _ {q}= s | _ {q} $ < BR> 我们在<跨度类=“math-container”> $ p $ ：

中的长度上证明了诱导

案例 $ p=epsilon $ ：这种情况不能发生，如 $ p $ 和 $ q $ 不会是并行位置。

案例 $ p= ip'$ ：
我们现在通过在 $ q $ 的长度上来证明这一点。

如果 $ q= epsilon $ ：

这不可能发生，如 $ p $ 和 $ q $ 不会是并行位置。

如果 $ q= jq' $ ：

有两种可能性，根据 $ i= j $ 或不是。

case $ i= j $ ：

强>

$（s [t] _ {ip'}）| _ {iq'}= f（s_1，\ ldots，s_ {i} [t] _ {p' }，\ ldots，s_ {n}）| _ {iq'}=（s_ {i} [t] _ {p'}）| _ {q'} $ 。我们有 $ p'$ 和 $ q'$ 是并行位置，因此，通过归纳假设： $$（s_ {i} [t] _ {p'}）| _ {q'}= s_ {i} | _ {q'}。$$ 由于我们也有 $ s | _ {iq'}= s_ {i} | _ {q'} | _ {q'} $ 结果保存。

案例 $ i \ neq j $ ：

让我们假设没有一般性的损失 $ i> j $ 。然后：
$$（s [t] _ {ip'}）| _ {jq'}= f（s_1，\ ldots，s_ {j}，\ ldots，s_ {i} [ t] _ {p'}，\ ldots，s_ {n}）| _ {jq'}= s_ {j} | _ {q'}。$$ 由于我们也有 $ s | _ {jq'}= s_ {j} | _ {j} | _ {q'} | _ {q'} $ 结果保存。

4.2 $（s [t] _ {p}）[r] _ {q}=（s [r] _ {q}）[t] _ {P} $ ：

案例 $ p=epsilon $ ：这种情况不能发生，如 $ p $ 和 $ q $ 不会是并行位置。

案例 $ p= ip'$ ：
我们现在通过在 $ q $ 的长度上来证明这一点。

如果 $ q= epsilon $ ：

这不可能发生，如 $ p $ 和 $ q $ 不会是并行位置。

如果 $ q= jq' $ ：

有两种可能性，根据 $ i= j $ 或不是。

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）$ 。
我们有 $ p'$ 和 $ q'$ 是并行位置，因此，通过归纳假设： $$（s_ {i} [t] _ {p'}）[r] _ {q'}=（s_ {i} [r] _ {q'}）[ t] _ {p'} $$ 因此 $$ 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}。$$

案例 $ i \ neq j $ ：

让我们假设没有一般性的损失 $ i> j $ 。然后：
$$（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'}。$$