diff --git a/Vorlesungen/ThProg/Konfluenz.tex b/Vorlesungen/ThProg/Konfluenz.tex index 367d3fa..3dd82f9 100644 --- a/Vorlesungen/ThProg/Konfluenz.tex +++ b/Vorlesungen/ThProg/Konfluenz.tex @@ -48,16 +48,17 @@ \[ mgu = [\;y \mapsto u\,,\;z \mapsto (\,u;\Uparrow\;w\,)\;] \] - \textbf{und die mit dem MGU substituierte Seite $l_1$:} + \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.1) = x\;\Uparrow \, ( \, u \; \Downarrow \; u\,) + l_1\sigma (1) = x\;\Uparrow \, ( \, u \; \Downarrow \; u\,) \hspace{1cm}&\hspace{8mm} - l_1\sigma (1.2) = x\;\Uparrow \, ( \, u \; \Uparrow \,(v\;\;\Downarrow\;v\,) \\\\ - + \underbrace{l_1\sigma (1) = x\;\Uparrow \, ( \, u \; \Uparrow \,\underbrace{(v\;\;\Downarrow\;v\,)}_{z'}}_{Regel\;(1)} \\\\ + l_1\sigma (1) = x\;\Uparrow \, ( \, u \; \Downarrow \; u\,) + \hspace{1cm}&==\hspace{10mm} + l_1\sigma (1) = x\;\Uparrow \, ( \, u \; \Downarrow \; u\,) \\ \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. + \textbf{Analog mit (2)(2) und allen anderen kritischen Paaren (wobei (1)(2) und (2)(1) hier triviale kritische Paare w\"aren!)}