From 43da8a85f1801ceb6e00dca4ed685ce322eb3137 Mon Sep 17 00:00:00 2001
From: Sheppy <jupiterfisch@web.de>
Date: Thu, 8 Oct 2015 14:17:26 +0200
Subject: [PATCH] started Konfluenz fixed missing negation in pumping lemma

---
 Vorlesungen/ThProg/Konfluenz.tex    | 46 +++++++++++++++++++++--------
 Vorlesungen/ThProg/PumpingLemma.tex |  2 +-
 2 files changed, 34 insertions(+), 14 deletions(-)

diff --git a/Vorlesungen/ThProg/Konfluenz.tex b/Vorlesungen/ThProg/Konfluenz.tex
index 58f0f1c..8205275 100644
--- a/Vorlesungen/ThProg/Konfluenz.tex
+++ b/Vorlesungen/ThProg/Konfluenz.tex
@@ -2,6 +2,7 @@
 	\usepackage{amsmath}
 	\usepackage{nccmath}
 	\DeclareMathSizes{10}{10}{10}{10}
+	\newcommand{\xhspace}[0]{\noindent\hspace*{5mm}}
 	\setlength{\parindent}{0pt}
 	\title{Konfluenz}
 	\date{ }
@@ -11,7 +12,24 @@
 			Ein stark normalisierendes und lokal Konfluentes Termersetzungssystem (TES) ist konfluent.
 		\subsection*{Critical Pair Lemma:}
 			Ein TES ist lokal konfluent, wenn alle kritischen Paare zusammenf\"uhrbar sind.
-		\section{Matching Table:}
+			
+		\section*{Allgemeines Vorgehen:}
+		Alle Regeln m\"ussen gegen alle anderen gematched werden um lokale Konfluenz zu 
+		zeigen, f\"ur das Gegenteil reicht also logischerweise \textbf{ein} nicht- 
+		zusammenf\"urbares Paar.\\\\
+		
+		\textbf{F\"ur Regelpaar (x)(y):}\\
+		$\rightarrow$ $l_1$ = linke Seite von x\\
+		$\rightarrow$ $l_2$ = linke Seite von y (falls gleiche Variablennamen selbige umbennen)\\
+		$\rightarrow$ $l_1$ so substituieren, dass Regel y angewendet werden kann (aka MGU finden)\\
+		$\rightarrow$ $l_1$ sollte der MGU = $l_2$ sein $\rightarrow$ triviales Paar\\
+		$\rightarrow$ beide Regeln 1x anwenden und sehen ob man die entstehenden Terme wieder zusammen bringen kann 
+		\textit{(durch Anwendung beliebiger Regeln des TES)}\\\\
+		
+		Triviale Paare muessen nicht gezeigt werden. Ein Paar kann bereits nach Anwendung beider Regeln wieder gleich sein
+		(z.B. $\neg\neg\neg x$ ). So ein Paar ist automatisch zusammenf\"uhrbar, aber dennoch der Definition nach
+		\textbf{\underline{kein}} triviales Paar.
+		\section*{Beispiel Lokale Konfluenz zeigen:}
 			Formeln:
 			\begin{align}
 				x \Uparrow ( y \Uparrow z) & \rightarrow_{0}
@@ -20,18 +38,20 @@
 				x \Downarrow ( x \Downarrow y ) & \rightarrow_0
 					\; x \Downarrow y
 			\end{align}
-			- alle Regeln m\"ussen gegen alle anderen gematched werden 
-			daher f\"ur \"ubersichtlichkeit:\\ \\
-			\begin{tabular}{l c r}
-				  & 1 & 2 \\
-				1 & ? & ? \\
-				2 & ? & ? \\
-			\end{tabular}		
-		
-		
-		
-		
-		
+			
+		\textbf{(1)(1)}
+			\begin{align*}
+				l_1 &= x \Uparrow ( y \Uparrow z)  \\
+				l_2 &= u \Uparrow ( v \Uparrow w)  \\
+			\end{align*}
+		\textbf{damit:}
+			\[
+				mgu = [\;y \mapsto u\,,\;z \mapsto (\,u;\Uparrow\;w\,)\;]
+			\]
+		\textbf{und die mit dem mgu substituierte Seite $l_1$:}
+			\[
+				l_1\omega = u \Uparrow 
+			\]
 		
 		
 		
diff --git a/Vorlesungen/ThProg/PumpingLemma.tex b/Vorlesungen/ThProg/PumpingLemma.tex
index acc4e56..fc9118f 100644
--- a/Vorlesungen/ThProg/PumpingLemma.tex
+++ b/Vorlesungen/ThProg/PumpingLemma.tex
@@ -14,7 +14,7 @@
 	%\maketitle
 	%----------------------------------%
 	Konkret geht es in diesem Beispiel um eine Sprache die alle ge\"offneten Klammern auch wieder schlie$\upbeta$en soll, oder allgemeiner, um eine Sprache die sich eine Anzahl merken muss.\\\\	
-	\textbf{'L' ist regul\"ar wenn:}
+	\textbf{'L' ist nicht regul\"ar wenn:}
 		\[		
 			\forall l \geq 1\;.\, \exists w \in L\;mit\; |w|\geq l
 		\]