From e7c959dc3320dfef7138f7b0741877fe2854a005 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Tue, 15 Mar 2016 09:33:33 +0100
Subject: Fix task 6 2.21

---
 task6.tex | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

(limited to 'task6.tex')

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.
-- 
cgit v1.2.3

