From 11552bd5affd916c4fe40a5a173f8432927b1ee4 Mon Sep 17 00:00:00 2001 From: Sheppy Date: Thu, 8 Oct 2015 14:35:00 +0200 Subject: [PATCH] Konfluenz fertig --- Vorlesungen/ThProg/Konfluenz.tex | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/Vorlesungen/ThProg/Konfluenz.tex b/Vorlesungen/ThProg/Konfluenz.tex index 8205275..602e9c7 100644 --- a/Vorlesungen/ThProg/Konfluenz.tex +++ b/Vorlesungen/ThProg/Konfluenz.tex @@ -48,12 +48,16 @@ \[ mgu = [\;y \mapsto u\,,\;z \mapsto (\,u;\Uparrow\;w\,)\;] \] - \textbf{und die mit dem mgu substituierte Seite $l_1$:} - \[ - l_1\omega = u \Uparrow - \] - - + \textbf{und die mit dem MGU substituierte Seite $l_1$:} + \begin{align*} + l_1\sigma = x \Uparrow (\,u\;&\Uparrow\,(\,v\Uparrow\;w\,))\\ \\ + l_1\sigma (1) = x\;\Uparrow \, ( \, u \; \Downarrow \; u\,) + \hspace{1cm}&\hspace{8mm} + l_1\sigma (2) = x\;\Uparrow \, ( \, u \; \Uparrow \,(v\;\;\Downarrow\;v\,) \\\\ + Nicht\;zusam&menfuehrbar!\\ + \end{align*} + Newman's Lemma bedeutet in der Umkehrung, dass ein System bei dem mindestens ein Paar nicht zusammenf\"uhrbar ist, nicht konfluent ist.\\ + D.h. wir sind hier bereits fertig.