8 files changed, 218 insertions, 4 deletions

diff --git a/gup/pdf.gup b/gup/pdf.gup
index 9b6749e..5a4588b 100755
--- a/gup/pdf.gup
+++ b/gup/pdf.gup
@@ -3,4 +3,4 @@
 gup -u ${2%.pdf}.md
 
 pandoc -t latex -o $2 -V "geometry=margin=2cm" -V "fontfamily=libertine" ${2%.pdf}.md >&2
-touch $2
+[[ -e $2 ]] && touch $2
diff --git a/shell.nix b/shell.nix
index 3da569e..81aca9d 100644
--- a/shell.nix
+++ b/shell.nix
@@ -3,8 +3,7 @@
 
 pkgs.stdenv.mkDerivation rec {
   name = "uni-env";
-  buildInputs = [ pkgs.haskellPackages.pandoc
-                  pkgs.gup
+  buildInputs = [ pkgs.gup
                   pkgs.jdk
                   pkgs.zip
                   pkgs.strace
@@ -12,8 +11,11 @@ pkgs.stdenv.mkDerivation rec {
                   (pkgs.callPackage ./mars.nix {})
                   pkgs.sqlite
                   (pkgs.haskellPackages.ghcWithPackages (p:
-                    with p; [ yesod yesod-bin
+                    with p; [ yesod yesod-bin pandoc
                             ]))
+                  (pkgs.texlive.combine {
+                    inherit (pkgs.texlive) scheme-small libertine tipa cm-super context bussproofs mweights fontaxes;
+                  })
                 ];
   shellHook = ''
     export PROMPT_INFO="${name}"
diff --git a/ws2015/EiP/blaetter/03/H3-1.md b/ws2015/EiP/blaetter/03/H3-1.md
new file mode 100644
index 0000000..bb3d2ca
--- /dev/null
+++ b/ws2015/EiP/blaetter/03/H3-1.md
@@ -0,0 +1,39 @@
+---
+header-includes:
+        - \usepackage{bussproofs}
+        - \renewcommand{\implies}{\rightarrow}
+        - \EnableBpAbbreviations
+---
+# Hoare-Tripel II
+
+d)
+
+\begin{prooftree}
+\AXC{$\forall \phi \ldotp \phi \implies \phi$}
+\UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n < m)$}
+\RightLabel{Umformung}
+\UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n \leq m - 1)$}
+\RightLabel{Umformung}
+\UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n + 1 \leq m)$}
+\RightLabel{Zuweisung}
+\UIC{$ \{ 0 < n + 1 \land n < m \} $ \texttt{n = n + 1} $ \{ 0 < n \land n \leq m \} $}
+\end{prooftree}
+
+e) Nimm als Gegenbeispiel:
+
+~~~
+a = -1
+b = 0
+~~~
+
+f) Seit $\phi$ die Nachfolgerfunktion auf $\mathbb{N}$.
+
+\begin{prooftree}
+\AXC{$\forall n \in \mathbb{N} \ldotp \phi(n) > n$}
+\UIC{$1 > 0$}
+\UIC{$((x + 1) + y > x + y)$}
+\UIC{$(z = x + y) \implies ((x + 1) + y > z)$}
+\UIC{$ \{ z = x + y \} $ \texttt{ x = x + 1} $ \{ x + y > z \} $}
+\UIC{$ \{ z = x + y \land z \equiv 0 \mod 2 \} $ \texttt{x = x + 1} $ \{ x + y > z \} $ \quad $ \{ z = x + y \land z \equiv 1 \mod 2 \} $ \texttt{x = x + 1} $ \{ x + y > z \} $}
+\UIC{$ \{ z = x + y \} $ \texttt{if (z \% 2 == 0) x = x + 1; else y = y + 1;} $ \{ x + y > z \} $}
+\end{prooftree}
diff --git a/ws2015/EiP/blaetter/03/H3-2.md b/ws2015/EiP/blaetter/03/H3-2.md
new file mode 100644
index 0000000..62d8fc2
--- /dev/null
+++ b/ws2015/EiP/blaetter/03/H3-2.md
@@ -0,0 +1,84 @@
+---
+header-includes:
+        - \usepackage{bussproofs}
+        - \renewcommand{\implies}{\rightarrow}
+        - \EnableBpAbbreviations
+---
+# Hoare-Logik: While-Schleife II
+
+| Schleifendurchlauf | \texttt{n} | \texttt{a} | \texttt{b} | \texttt{c} |
+|--------------------+------------+------------+------------+------------|
+|                  0 |          5 |          0 |          0 |          1 |
+|                  1 |          5 |          1 |          1 |          7 |
+|                  2 |          5 |          8 |          2 |         19 |
+|                  3 |          5 |         27 |          3 |         37 |
+|                  4 |          5 |         64 |          4 |         61 |
+|                  5 |          5 |        125 |          5 |         91 |
+
+Wir bezeichnen mit $P'$:
+
+~~~
+a = a + c
+b = b + 1
+c = c + 6*b
+~~~
+
+Wir bezeichnen mit $J$:
+
+~~~
+a = 0
+b = 0
+c = 1
+~~~
+
+und setzen $J'$ derart, dass $\{\} J \{J'\}$ gültig ist.
+
+Wir bezeichnen zudem mit $\bar P$:
+
+~~~
+while (b != n) {
+  a = a + c
+  b = b + 1
+  c = c + 6*b
+}
+~~~
+
+Es sei zudem $I = (c = (b + 1)^3 - b^3)$.
+
+\begin{prooftree}
+\AXC{$ 1 = (0 + 1)^3 - 0 $}
+\UIC{$ (a, b, c) = (0, 0, 1) \implies c = ( b + 1 )^3 - b^3$}
+\UIC{$J' \implies I$}
+\end{prooftree}
+
+\begin{prooftree}
+\AXC{$0 = 0$}
+\RightLabel{Algebraische Umformung}
+\UIC{$(b + 1)^3 - b^3 + 6 \cdot (b + 1) = (b + 2)^3 - (b + 1)^3$}
+\UIC{$c = ( b + 1 )^3 - b^3 \implies c + 6 \cdot (b + 1) = (b + 2)^3 - (b + 1)^3$}
+\UIC{$\{c = ( b + 1 )^3 - b^3 \land b \neq n \}$ $P'$ $\{ c = (b + 1)^3 - b^3 \}$}
+\UIC{$\{ I \land b \}$ $P'$ $ \{ I \} $}
+\end{prooftree}
+
+\begin{prooftree}
+\AXC{$J' \implies I$}
+\AXC{$\{I \land b\}$ $P'$ $\{ I \}$}
+\AXC{$I \land b = n \implies a = n^3$}
+\TIC{$ \{ n > 0 \land J' \} $ $ \bar P $ $ \{ a = n^3 \} $}
+\end{prooftree}
+
+Es bleibt zu zeigen, dass $a(n) = n^3$.
+Es gilt wegen $P'$ und $J$:
+\begin{align*}
+c(0) &= 1 \\
+c(k) &= c(k - 1) + 6 \cdot k \\
+     &= 1 + \sum_{i = 0}^{k} 6i \\
+a(0) &= 0 \\
+a(k) &= a(k - 1) + c(k - 1) \\
+         &= a(k - 1) + 1 + \sum_{i = 0}^{k - 1} 6i \\
+         &= \sum_{j = 0}^{k} \left ( 1 + \sum_{i = 0}^{j - 1} 6i \right ) \\
+         &= k + \sum_{j = 0}^{k} \sum_{i = 0}^{j - 1} 6i \\
+         &= k + \sum_{j = 0}^{k} \left ( 3j (j - 1) \right ) \\
+         &= k + \left ( k^3 - k \right ) \\
+         &= k^3
+\end{align*}
diff --git a/ws2015/EiP/blaetter/03/H3-3.md b/ws2015/EiP/blaetter/03/H3-3.md
new file mode 100644
index 0000000..ca9fbd8
--- /dev/null
+++ b/ws2015/EiP/blaetter/03/H3-3.md
@@ -0,0 +1,33 @@
+# Code Verständnis
+
+| Zeile | Zuweisung |
+|-------+-----------|
+|   010 | x = 42    |
+|   030 | y = 36    |
+|   070 | z = 1     |
+|   080 | z = 2     |
+|   090 | z = 3     |
+|   100 | y = 39    |
+|   120 | z = 6     |
+|   070 | z = 1     |
+|   080 | z = 2     |
+|   090 | z = 3     |
+|   100 | y = 42    |
+|   120 | z = 6     |
+|   230 | x = 53    |
+|   240 | z = 0     |
+|   250 | x = 57    |
+|   260 | y = 36    |
+|   270 | z = 1     |
+|   240 | z = 1     |
+|   250 | x = 61    |
+|   260 | y = 37    |
+|   270 | z = 2     |
+|   240 | z = 2     |
+|   250 | x = 65    |
+|   260 | y = 39    |
+|   270 | z = 3     |
+|   240 | z = 3     |
+|   250 | x = 69    |
+|   260 | y = 42    |
+|   270 | z = 4     |
diff --git a/ws2015/EiP/blaetter/03/manifest b/ws2015/EiP/blaetter/03/manifest
new file mode 100644
index 0000000..ff79ea4
--- /dev/null
+++ b/ws2015/EiP/blaetter/03/manifest
@@ -0,0 +1,3 @@
+H3-1.pdf
+H3-2.pdf
+H3-3.pdf
\ No newline at end of file
diff --git a/ws2015/betriebssysteme/blaetter/04/abgabe.md b/ws2015/betriebssysteme/blaetter/04/abgabe.md
new file mode 100644
index 0000000..94578c5
--- /dev/null
+++ b/ws2015/betriebssysteme/blaetter/04/abgabe.md
@@ -0,0 +1,38 @@
+# 5-Zustands-Prozessmodell
+
+a)
+        i) Übergang von *blocked* zu *running* wird nur via *ready* realisiert, da der Scheduler bereits periodisch Prozesse aus *ready* aufweckt.
+                Zusätzlich auch noch den jeweiligen Prozess aufzuwecken wäre schlicht unnötig.
+        ii) Fordert ein Prozess E/A-Resourcen an, so wird er nach *blocked* verschoben bis die jeweilige E/A-Operation per Unterbrechung bekannt macht, dass der Vorgang abgeschlossen ist.
+        iii) Ein Prozess, der nicht läuft, kann keine E/A-Resource anfordern.  
+b)
+        (i) *new* → *ready*
+                ~ Ein Nutzer hat seine Shell angewiesen `Hello World!` auszugeben, diese forkt um später `/bin/echo` aufzurufen.
+                        
+                *ready* → *running*
+                ~ Der Shell-Prozess ruft `wait` auf den soeben gespawnten Prozess auf und wird daher *blocked*.
+                Der Scheduler entscheidet nun zum Kindprozess zu wechseln.
+
+            *running* → *ready*
+                ~ `/bin/echo` hat nicht innerhalb der switching-Frequenz des Schedulers terminiert.
+                Der Scheduler verschiebt `/bin/echo` in *ready* und wechselt zu einem anderen Prozess.
+
+                *running* → *blocked*
+                ~ `/bin/echo` ist dynamisch gelinkt und möchte eine library von der Festplatte lesen.
+                Es setzt einen Syscall ab und wartet auf das Ergebnis.
+
+            *blocked* → *ready*
+                ~ Die Festplatte fängt an einen Stream von bytes zu schicken.
+                Der Scheduler fängt die Unterbrechung ab und verschiebt `/bin/echo` nach *ready*
+
+            *running* → *exit*
+            ~ `/bin/echo` terminiert.
+        (ii) *new*. Prozesse werden im reinen batch-betrieb nicht dynamisch erzeugt.
+
+# Prozesse
+
+a) Kontext
+b) Uniprogramming
+c) 13.3 min
+d) `fork`
+e) Scheduler
diff --git a/ws2015/datenbanksysteme/blaetter/04/abgabe.md b/ws2015/datenbanksysteme/blaetter/04/abgabe.md
new file mode 100644
index 0000000..708a249
--- /dev/null
+++ b/ws2015/datenbanksysteme/blaetter/04/abgabe.md
@@ -0,0 +1,15 @@
+---
+header-includes:
+        - \usepackage{amsmath}
+        - \usepackage{amssymb}
+---
+
+# Natural Join
+
+Zu $\land$.
+
+# Anfragen in relationaler Algebra
+
+a) $\pi_{\texttt{P.pname}}(\sigma_{\texttt{P.ort} = \text{Berlin}}(\texttt{P}))$
+b) $\pi_{\texttt{T.tnr}} \left ( \sigma_{\texttt{L.lname} = \text{Meier}} \left ( \texttt{L} \bowtie \texttt{LTP} \texttt{T} \right ) \right )$
+c) $\pi_{\texttt{T.tname}}(\sigma_{\texttt{P.ort} = \text{Berlin}}(\texttt{P} \bowtie \texttt{LTP} \bowtie \texttt{T}))$