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$