Fix task 6 2.21

1 files changed, 16 insertions, 6 deletions

diff --git a/task6.tex b/task6.tex
index 9693eb8..ef3a95d 100644
--- a/task6.tex
+++ b/task6.tex
@@ -56,12 +56,22 @@ Een toestand $s$ waarvoor de afleidingsrij van $\scomp{\sass{z}0}\whileLoop$ en
 \end{alignat*}
 
 \section*{Opdracht 2.21}
-Volgt dit niet direct uit $\rcompsos2$?
-%\begin{proof}
-%  In het geval dat $k=0$ is dit overduidelijk waar.
-%
-%  Stel dat voor $k\leq k_0$ geldt dat als $\transl{S_1}s\dimpl^ks'$, dan $\transl{\scomp{S_1}{S_2}}s\dimpl^k\transl{S_2}{s'}$ (\textbf{IH}).
-%\end{proof}
+\begin{proof}
+  In het geval dat $k=0$ is dit overduidelijk waar.
+
+  Stel dat voor $k\leq k_0$ geldt dat als $\transl{S_1}s\dimpl^ks'$, dan $\transl{\scomp{S_1}{S_2}}s\dimpl^k\transl{S_2}{s'}$ (inductiehypothese).
+
+  Stel verder dat $\transl{S_1}s \dimpl^{k+1} s''$. Dan hebben we een afleiding $\transl{S_1}s \dimpl \gamma \dimpl^k s''$ met $\gamma=\transl{S_1'}{s'}$. Dus $\transl{S_1}s \dimpl \transl{S_1'}{s'} \dimpl^k s''$.
+
+  Dan geldt volgens de inductiehypothese voor elke $S_2$ dat$\transl{\scomp{S_1'}{S_2}}{s'} \dimpl^k \transl{S_2}{s''}$.
+
+  Voor de afleiding van $\transl{\scomp{S_1}{S_2}}s$ moeten we dan $\rcompsos1$ toepassen, en dus krijgen we: $\transl{\scomp{S_1}{S_2}}s \dimpl \transl{\scomp{S_1'}{S_2}}{s'} \dimpl^k \transl{S_2}{s''}$.
+
+  Hieruit volgt dat $\transl{\scomp{S_1}{S_2}}s \dimpl^{k+1} \transl{S_2}{s''}$.
+
+  Uit het principe van volledige inductie volgt nu dat als $\transl{S_1}s \dimpl^k s'$, dan ook $\transl{\scomp{S_1}{S_2}}s \dimpl^k \transl{S_2}{s'}$, voor alle $S_1, S_2, s$ en $k\in\mathbb N$.
+
+\end{proof}
 
 \section*{Semantische equivalentie}
 De definitie van semantische equivalentie is beter met een conjunctie dan met een disjunctie. Anders zouden alle paren statements $S_1,S_2$ equivalent zijn terwijl er toestanden zijn waarbij de twee statements na een eindig aantal stappen in verschillende toestanden $\gamma\neq\gamma'$ terechtkomen, die beide terminaal zijn, omdat dan de tweede conditie in de definitie waar is.