From d2d4cfd51b9e5f47c98bd84406d20a9fe01f5485 Mon Sep 17 00:00:00 2001 From: Sheppy Date: Thu, 8 Oct 2015 15:15:34 +0200 Subject: [PATCH] fixes --- Vorlesungen/ThProg/Konfluenz.tex | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) 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!)}