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

Fixes in Bisimullation

Browse Source
This commit is contained in:
Sheppy 2015-10-09 13:17:16 +02:00
parent b6b6c527cf
commit 5ff1f0ab28
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Vorlesungen/ThProg/Koinduktion_reduktion.tex
View File

@ -71,7 +71,8 @@
\[ currentSample(\,sampler(square\:0\:1)(square\:x\:0)) = 0 \] \[ currentSample(\,sampler(square\:0\:1)(square\:x\:0)) = 0 \]
$\rightarrow$ wenn hier am Ende kein Term rauskommt, dann koennen wir einfach die \textbf{rechte Seite bei der normalen Funktion} einsetzen und selbige aufloesen: $\rightarrow$ wenn hier am Ende kein Term rauskommt, dann koennen wir einfach die \textbf{rechte Seite bei der normalen Funktion} einsetzen und selbige aufloesen:
\[ currentSample(flat\;0) = 0 \] \[ currentSample(flat\;0) = 0 \]
$\rightarrow$ sehr gut, die rechten Seiten sind gleich wir sind hier also fertig\\ \\ $\rightarrow$ sehr gut, die rechten Seiten sind gleich wir sind hier also fertig\\\\
\textbf{\underline{WICHTIG} Jetzt das selbe noch mit discardSample()!}\\\\
\textbf{zweite Bedingung:} \textbf{zweite Bedingung:}
\begin{align*} \begin{align*}
discardSample(sampler&(square\;1\;0)(square\;0\;x)) \\ discardSample(sampler&(square\;1\;0)(square\;0\;x)) \\
@ -82,15 +83,15 @@
\textbf{Schritt 3:}\\ \textbf{Schritt 3:}\\
\[R' = R \;\cup\;\{\underbrace{ \[R' = R \;\cup\;\{\underbrace{
sampler(discardSample (square\;1\;0))(discardSample(square\;0\;x)) sampler(discardSample (square\;1\;0))(discardSample(square\;0\;x))
}_{aufgeloeste\;2.\;Bedingung},square\;x\;0\:|\:x\in Int\}\] }_{aufgeloeste\;2.\;Bedingung},discardSample(square\;x\;0\,)\:|\:x\in Int\}\]
wir muessen jetzt zeigen: wir muessen jetzt zeigen:
\[ \[
currentSample(\underbrace{sampler(square\:1\:0)(square\:0\:x)}_{hier\;=\;0}) = \underbrace{currentSample(flat\;0)}_{hier\;=\;0} \underbrace{currentSample(sampler(square\:1\:0)(square\:0\:x)}_{currentSample(\,x\;0\,)}) = \underbrace{currentSample(square\;0\,x)}_{selbes\;wie\;rechts}
\] \]
passt also, jetzt wie oben auch zweite Funktion: passt also, jetzt wie oben auch zweite Funktion:
\[ \[
discardSample(sampler(square\:1\:0)(square\:0\:x)) = \underbrace{sampler(square\:1\:0)(square\:0\:x)}_{wieder\;linke\;Seite\;in\;R'}\]\[ discardSample(sampler(square\:1\:0)(square\:0\:x)) = \underbrace{sampler(square\:1\:0)(square\:0\:x)}_{wieder\;linke\;Seite\;in\;R'}\]\[
discardSample(flat\;0) = \underbrace{flat\;0}_{wieder\;rechte\;Seite} discardSample(\,square\;x\;0\,) = \underbrace{discardSample(\,square\;0\;x\,)}_{wieder\;rechte\;Seite}
\] \]
und fertig!\\\\ und fertig!\\\\
\section*{Sonstiges:} \section*{Sonstiges:}