---
# System prepended metadata

title: Lemat pomocniczy

---

tags: `jp21`

# Lemat pomocniczy
## 17 października 2021

**Założenie**: Niech $t, t'$ będą termami, że $t \rightarrow^* t'$.
**Teza**:
$$
(t = t') \vee (\exists s. t \rightarrow_1 s \wedge s \rightarrow^* t')
$$
**Dowód**:
Indukcja względem drzewa wyprowadzenia $t \rightarrow^* t'$:
1. Wyprowadzenie ma w korzeniu $\dfrac{}{t \rightarrow^* t}$:
    Mamy $t = t'$, więc zachodzi lewa strona alternatywy w tezie.
2. Wyprowadzenie ma w korzeniu $\dfrac{t \rightarrow_1 t'}{t \rightarrow^* t'}$:
    Pokażemy, że zachodzi prawa strona alternatywy w tezie.
    Niech $s := t'$ ($s$ to ten z tezy), wtedy pozostaje udowodnić: $t \rightarrow_1 t' \wedge t' \rightarrow^* t'$.
    Pierwsze dostajemy z drzewa wyprowadzenia, drugie ze zwrotności $\rightarrow^*$.
3. Wyprowadzenie ma w korzeniu $\dfrac{t \rightarrow^* t''\quad t'' \rightarrow^* t'}{t \rightarrow^* t'}$:
  Z zał. ind dla $t \rightarrow^* t''$ mamy dwie możliwości:
- Zachodzi $t = t''$, w konsekwencji $t \rightarrow^* t'$. Korzystamy z założenia ind. dla drugiej przesłanki w drzewie, która brzmi $t \rightarrow^* t'$ (bo $t = t''$), mamy znowu dwie możliwości:
    - Zachodzi $t = t'$, zatem zachodzi lewa alternatywa w tezie,
    - $\exists s. t \rightarrow_1 s \wedge s \rightarrow^* t'$, wtedy zachodzi prawa alternatywa tezy
- $\exists s. t \rightarrow_1 s \wedge s \rightarrow^* t''$. Pokażemy, że zachodzi prawa strona alternatywy w tezie (z takim samym $s$).
    Pozostaje zatem pokazać $t \rightarrow_1 s$ i $s \rightarrow^* t'$:
    - $t \rightarrow_1 s$ mamy z rozważanego przypadku,
    - wiemy, że $s \rightarrow^* t''$ i $t'' \rightarrow^* t'$, zatem z trzeciej reguły dla $\rightarrow^*$ wiemy, że $t'' \rightarrow^* t'$, cbdu.
  
 Rozważyliśmy wszystkie możliwe przypadki.
 
 $\blacksquare$