Mirror/latexandmore
1
0
Fork 0
mirror of https://gitlab.cs.fau.de/ik15ydit/latexandmore.git synced 2024-11-25 21:25:02 +01:00
Code Issues Projects Releases Wiki Activity

fixes

Browse Source
This commit is contained in:
Sheppy 2015-10-08 15:15:34 +02:00
parent dc3ee72a39
commit d2d4cfd51b
1 changed files with 7 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
Vorlesungen/ThProg/Konfluenz.tex
View File

@ -48,16 +48,17 @@
\[ \[
mgu = [\;y \mapsto u\,,\;z \mapsto (\,u;\Uparrow\;w\,)\;] 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*} \begin{align*}
l_1\sigma = x \Uparrow (\,u\;&\Uparrow\,(\,v\Uparrow\;w\,))\\ \\ 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} \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*} \end{align*}
Newman's Lemma bedeutet in der Umkehrung, dass ein System bei dem mindestens ein Paar nicht zusammenf\"uhrbar ist, nicht konfluent ist.\\ \textbf{Analog mit (2)(2) und allen anderen kritischen Paaren (wobei (1)(2) und (2)(1) hier triviale kritische Paare w\"aren!)}
D.h. wir sind hier bereits fertig.