From 6dad43a678ac89e411244153cf45d8491ac68d1f Mon Sep 17 00:00:00 2001 From: Sheppy Date: Thu, 8 Oct 2015 21:44:34 +0200 Subject: [PATCH] Bisimulation small changes --- Vorlesungen/ThProg/Koinduktion_reduktion.tex | 11 +++++++++++ Vorlesungen/ThProg/Makefile | 17 ++++++++++------- 2 files changed, 21 insertions(+), 7 deletions(-) diff --git a/Vorlesungen/ThProg/Koinduktion_reduktion.tex b/Vorlesungen/ThProg/Koinduktion_reduktion.tex index 6aeeb24..d075f20 100644 --- a/Vorlesungen/ThProg/Koinduktion_reduktion.tex +++ b/Vorlesungen/ThProg/Koinduktion_reduktion.tex @@ -88,6 +88,17 @@ discardSample(flat\;0) = \underbrace{flat\;0}_{wieder\;rechte\;Seite} \] und fertig!\\\\ +\section*{Sonstiges:} + Eine Relation $\mathrm{R}\;\subset\;A^{\omega}\;$x$\;A^{\omega}$ heisst Bisimulation, wenn f\"ur + alle $(s,t)$ $\in\; \mathrm{R}$ gilt: \\ + \noindent\hspace{1cm} hd s = hd t\\ + \noindent\hspace{1cm} (tl\;s)\;R\;(tl\;t)\\\\\\\\ + + Wenn R eine Bisimulation ist, dann gilt $\mathrm{R}\;\subseteq\;id$ , d.h. + \[ + sRt \Rightarrow s = t + \] + f\"ur alle s,t $\in\;A^\omega$\\\\ \begin{tiny} \copyright\ Joint-Troll-Expert-Group (JTEG) 2015 \end{tiny} diff --git a/Vorlesungen/ThProg/Makefile b/Vorlesungen/ThProg/Makefile index 6039d24..6100d25 100644 --- a/Vorlesungen/ThProg/Makefile +++ b/Vorlesungen/ThProg/Makefile @@ -1,20 +1,23 @@ all: Konfluenz.pdf Koinduktion_reduktion.pdf Strukturelle_Induktion.pdf Polynomordnung.pdf SystemF.pdf PumpingLemma.pdf -continuous: $(PDF).continuous +continuous: $(PDF).continuous -clean: cleanup all +clean: cleanup rmpdf all + +rmpdf: + @-rm -f *.pdf cleanup: - -rm -f *.aux *.fdb_latexmk *.fls *.log *.pdf + @-rm -f *.aux *.fdb_latexmk *.fls *.log single: all - -pdftk Polynomordnung.pdf Konfluenz.pdf SystemF.pdf Koinduktion_reduktion.pdf Strukturelle_Induktion.pdf PumpingLemma.pdf cat output ThProgCheatsheet.pdf + @-pdftk Polynomordnung.pdf Konfluenz.pdf SystemF.pdf Koinduktion_reduktion.pdf Strukturelle_Induktion.pdf PumpingLemma.pdf cat output ThProgCheatsheet.pdf %.continuous: %.pdf - latexmk -quiet -jobname=$(@:%.continuous=%) -pvc -pdf $(@:%.continuous=%).tex + @latexmk -quiet -jobname=$(@:%.continuous=%) -pvc -pdf $(@:%.continuous=%).tex %.pdf: %.tex - latexmk -quiet -jobname=$(@:%.pdf=%) -pdf -halt-on-error $< 1>/dev/null + @latexmk -quiet -jobname=$(@:%.pdf=%) -pdf -halt-on-error $< 1>/dev/null -.PHONY: all continuous cleanup single +.PHONY: all continuous cleanup single clean rmpdf