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.