mirror of
https://gitlab.cs.fau.de/ik15ydit/latexandmore.git
synced 2024-11-22 11:49:32 +01:00
Konfluenz fertig
This commit is contained in:
parent
43da8a85f1
commit
11552bd5af
@ -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.
|
||||
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user