diff --git a/info4/kapitel-2/Der Satz von Myhill und Nerode.ipynb b/info4/kapitel-2/Der Satz von Myhill und Nerode.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..02e621953c89fab1646af6a4685d82831242d8bc
--- /dev/null
+++ b/info4/kapitel-2/Der Satz von Myhill und Nerode.ipynb
@@ -0,0 +1,283 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Der Satz von Myhill und Nerode"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: EquivalenceRelation"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE EquivalenceRelation\n",
+ "/* Ein Modell der Myhill-Nerode Äquivalenzrelation R_L,\n",
+ " der entsprechenden Äquivalenzklassen und dem Index der Sprache.*/\n",
+ "SETS\n",
+ " Alphabet = {a,b,c}\n",
+ "CONSTANTS L, RL, maxsize, All, Classes, index\n",
+ "DEFINITIONS\n",
+ " class(x) == {y | x↦y : RL} ;\n",
+ " ANIMATION_FUNCTION1 == {r,c,i |r=1 ∧ c∈ dom(word) ∧ i=word(c)};\n",
+ " ANIMATION_FUNCTION2 == {r,c,i |r=2 ∧ c=1 ∧ i=z};\n",
+ " ANIMATION_FUNCTION3 == {(1, 0, \"Wort:\"), (2, 0, \"Äquivalenzklasse:\")};\n",
+ " \n",
+ "PROPERTIES\n",
+ " L ⊆ seq(Alphabet) ∧\n",
+ " \n",
+ " // All = {z | z∈seq(Alphabet) ∧ size(z)<=maxsz} & /* beschränkt auf endliche Folgen */\n",
+ " All = UNION(ii).(ii:0..maxsize| (1..ii) --> Alphabet) ∧\n",
+ "\n",
+ " RL = ({x,y| x∈All ∧ y∈All ∧ ∀z.(z∈All ⇒ ( x^z ∈ L ⇔ y^z ∈ L))}) ∧\n",
+ "\n",
+ " L = {[a],[b],[a,a],[b,b],[a,a,c],[b,b,c],[c,c,c]} ∧ maxsize = 3 ∧\n",
+ "\n",
+ " Classes = ran( %x.(x∈All|class(x))) ∧ /* Menge der Äquivalenzklassen {class(x)|x∈All} */\n",
+ " index = card( Classes ) \n",
+ "\n",
+ "ASSERTIONS\n",
+ " /* Test ob wir eine Äquivalenzrelation haben: */\n",
+ " ∀x.(x∈All ⇒ x↦x ∈ RL); /* Reflexivität */\n",
+ " ∀(x,y).(x↦y ∈ RL ⇒ y↦x ∈ RL); /* Symetrie */\n",
+ " ∀(x,y,z).(x↦y ∈ RL ∧ y↦z ∈ RL ⇒ x↦z ∈ RL); /* Transitivität */\n",
+ "\n",
+ " /* Einige Beispiele : */\n",
+ " [a,a] ↦ [b,b] ∈ RL;\n",
+ " [a,a] ↦ [c,c] ∉ RL;\n",
+ " [b,b,c] ↦ [c,c,c] ∈ RL;\n",
+ " class([a,a]) = {[a,a],[b,b]};\n",
+ " class([c,c,c]) = {[a,a,c],[b,b,c],[c,c,c]}\n",
+ "\n",
+ "/* Der durch die Äquivalenzklassen induzierte DFA: */\n",
+ "VARIABLES z, word\n",
+ "INVARIANT z ⊆ All ∧ word ∈ seq(Alphabet)\n",
+ "INITIALISATION z := class([]); word := []\n",
+ "OPERATIONS\n",
+ " Delta(terminal) = PRE terminal∈Alphabet THEN\n",
+ " ANY x WHERE x∈z ∧ ∀x2.(x2∈z ⇒ size(x2)≥size(x)) THEN\n",
+ " z := class(x^[terminal]);\n",
+ " word := word^[terminal]\n",
+ " END\n",
+ " END;\n",
+ " Final = SELECT z ∩ L ≠ {} THEN skip END\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Durch die Äquivalenzklassen wird ein Minimalautomat induziert.\n",
+ "Die Menge der Zustände ist gleich der Menge der Äquivalenzklassen.\n",
+ "Und nach dem Einlesen eines Wortes $w∈Σ^*$ landet man in dem Zustand, der der Äquivalenzklasse von $w$ bezüglich $R_L$ entspricht."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: EquivalenceRelation\n",
+ "Sets: Alphabet\n",
+ "Constants: L, RL, maxsize, All, Classes, index\n",
+ "Variables: z, word\n",
+ "Operations: \n",
+ "Delta(a)\n",
+ "Delta(b)\n",
+ "Delta(c)"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Delta(a)"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Delta terminal=a"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Delta(a)"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Delta terminal=a"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">Wort:</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">Äquivalenzklasse:</td>\n",
+ "<td style=\"padding:10px\">{{(1|->a),(2|->a)},{(1|->b),(2|->b)}}</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$8$"
+ ],
+ "text/plain": [
+ "8"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "index"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Da der $Index(L)=8<\\infty$ ist die gegebene Sprache regulär."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 4
+}