diff --git a/info4/kapitel-11/PCP.ipynb b/info4/kapitel-11/PCP.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..9e632f34b1974f31753983ca38a9950373c9d2d0
--- /dev/null
+++ b/info4/kapitel-11/PCP.ipynb
@@ -0,0 +1,2856 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# PCP - Das Postsche Korrespondenzproblem\n",
+ " \n",
+ "Sei $\\Sigma$ ein Alphabet.\n",
+ "\n",
+ "\n",
+ "Das __Postsche Korrespondenzproblem__ (über $\\Sigma$)\n",
+ " ist definiert durch\n",
+ "\n",
+ "$PCP_{\\Sigma}$ = $\\{ ((x_1, y_1), \\ldots , (x_k, y_k)) |$\n",
+ "so dass $k \\in ℕ$ und $x_i, y_i \\in \\Sigma^{+}$ für $1 \\leq i \\leq k$}\n",
+ "und es gibt $i_1, i_2, \\ldots , i_n \\in \\{1, \\ldots , k\\}$,\n",
+ "so dass $x_{i_1} x_{i_2} \\cdots x_{i_n} = y_{i_1} y_{i_2} \\cdots\n",
+ " y_{i_n}$\n",
+ "$\\}$.\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Diese Maschine modelliert das PCP Problem von Folie 35. Die einzelnen Lösungschritte (hinzufügen eines Indexes $i_j$) werden mit der Operation ```Schritt``` ausgeführt.\n",
+ "Diese Maschine verhindert offensichtlich nutzlose Schritte, wo niemals eine Lösung gefunden werden kann, da der Anfang von x und y sich unterscheiden.\n",
+ "Sobald man eine Lösung gefunden hat ist die B Operation ```Lösung``` ausführbar."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 85,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: PostCorrespondence_MC"
+ ]
+ },
+ "execution_count": 85,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE PostCorrespondence_MC\n",
+ "/* Version wo die Schritt Operation nur sinnvolle Erweiterungen zulässt */\n",
+ "CONSTANTS K, Σ\n",
+ "PROPERTIES\n",
+ " Σ = {0,1} ∧\n",
+ " K = [ [1]↦[1,0], [0,1]↦[1], [0,1,0] ↦ [1,0,0] ] /* Problem von Folie 35 */\n",
+ "VARIABLES x,y\n",
+ "INVARIANT\n",
+ " x ∈ seq(Σ) ∧ y∈seq(Σ)\n",
+ "INITIALISATION x,y := <>,<>\n",
+ "OPERATIONS\n",
+ " Schritt(i,ix,iy) = PRE i∈dom(K) ∧ K(i)=ix↦iy\n",
+ " ∧ same_prefix(x^ix,y^iy) \n",
+ " /* kann man die beiden neuen Wörter überhaupt noch gleich machen ? */\n",
+ " THEN\n",
+ " x := x ^ ix || \n",
+ " y := y ^ iy\n",
+ " END;\n",
+ " Lösung = SELECT x=y ∧ x ≠ [] THEN skip END\n",
+ "DEFINITIONS\n",
+ " GOAL == (x=y ∧ x≠<>);\n",
+ " ANIMATION_FUNCTION == {1}×x ∪ {2}×y ; \n",
+ " ANIMATION_FUNCTION_DEFAULT == {(1,(0,2)),(2,(0,3))} ∪ {1,2}×λi.(i∈dom(x)∪dom(y)|6);\n",
+ " ANIMATION_IMG0 == \"images/sm_0.gif\";\n",
+ " ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+ " ANIMATION_IMG2 == \"images/sm_X.gif\";\n",
+ " ANIMATION_IMG3 == \"images/sm_Y.gif\";\n",
+ " ANIMATION_IMG6 == \"images/sm_empty_box.gif\";\n",
+ " SET_PREF_PP_SEQUENCES == TRUE;\n",
+ " same_prefix(a,b) == LET ms BE ms=min({size(a),size(b)}) IN\n",
+ " a /|\\ ms = b /|\\ ms END\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 86,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 86,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 87,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 87,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 88,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 88,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 89,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_MC\n",
+ "Sets: (none)\n",
+ "Constants: K, Σ\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(1,[1],[1,0])"
+ ]
+ },
+ "execution_count": 89,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Es wird nur Schritt mit $i=1$ angeboten, da sonst sich x und y am Anfang unterscheiden und wir nie mehr eine Lösung finden könnten."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 90,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(1,[1],[1,0])"
+ ]
+ },
+ "execution_count": 90,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 91,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 91,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 92,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_MC\n",
+ "Sets: (none)\n",
+ "Constants: K, Σ\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(2,[0,1],[1])\n",
+ "Schritt(3,[0,1,0],[1,0,0])"
+ ]
+ },
+ "execution_count": 92,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Hier gibt es zwei Möglichkeiten: wir können Index 2 oder 3 wählen"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 93,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(2,[0,1],[1])"
+ ]
+ },
+ "execution_count": 93,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 94,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 94,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 95,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Lösung()"
+ ]
+ },
+ "execution_count": 95,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Lösung"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wir haben eine Lösung gefunden.\n",
+ "Um die Lösung von den Folien nachzuspielen gehen wir noch einmal züruck."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 96,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "* -1: Root state\n",
+ "* 0: `SETUP_CONSTANTS()`\n",
+ "* 1: `INITIALISATION()`\n",
+ "* 2: `Schritt(1,[1],[1,0])`\n",
+ "* 3: `Schritt(2,[0,1],[1])`\n",
+ "* 4: `Lösung()` **(current)**"
+ ],
+ "text/plain": [
+ "-1: Root state\n",
+ "0: SETUP_CONSTANTS()\n",
+ "1: INITIALISATION()\n",
+ "2: Schritt(1,[1],[1,0])\n",
+ "3: Schritt(2,[0,1],[1])\n",
+ "4: Lösung() (current)"
+ ]
+ },
+ "execution_count": 96,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":trace"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 97,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed to state with index 2"
+ ]
+ },
+ "execution_count": 97,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":goto 2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 98,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 98,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 99,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(3,[0,1,0],[1,0,0])"
+ ]
+ },
+ "execution_count": 99,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 100,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 100,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 101,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(3,[0,1,0],[1,0,0])"
+ ]
+ },
+ "execution_count": 101,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 102,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 102,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 103,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(2,[0,1],[1])"
+ ]
+ },
+ "execution_count": 103,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 104,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 104,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 105,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Lösung()"
+ ]
+ },
+ "execution_count": 105,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Lösung"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 106,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "* -1: Root state\n",
+ "* 0: `SETUP_CONSTANTS()`\n",
+ "* 1: `INITIALISATION()`\n",
+ "* 2: `Schritt(1,[1],[1,0])`\n",
+ "* 3: `Schritt(3,[0,1,0],[1,0,0])`\n",
+ "* 4: `Schritt(3,[0,1,0],[1,0,0])`\n",
+ "* 5: `Schritt(2,[0,1],[1])`\n",
+ "* 6: `Lösung()` **(current)**"
+ ],
+ "text/plain": [
+ "-1: Root state\n",
+ "0: SETUP_CONSTANTS()\n",
+ "1: INITIALISATION()\n",
+ "2: Schritt(1,[1],[1,0])\n",
+ "3: Schritt(3,[0,1,0],[1,0,0])\n",
+ "4: Schritt(3,[0,1,0],[1,0,0])\n",
+ "5: Schritt(2,[0,1],[1])\n",
+ "6: Lösung() (current)"
+ ]
+ },
+ "execution_count": 106,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":trace"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Sie können das B Modell oben mit anderen Werten für K ausprobieren:\n",
+ "- K = [ [0,1]↦[1], [0,1,0]↦[1,0,0], [1]↦[1,0] ] Problem von Folie 36 */\n",
+ "- K = [ [1]↦[1,0,1], [1,0]↦[0,0], [0,1,1]↦[1,1] ] \n",
+ "- K = [ [0,0,1]↦[0], [0,1]↦[0,1,1], [0,1]↦[1,0,1], [1,0] ↦ [0,0,1] ], Problem von Folie 32; kleinse Lösung hat 66 Elemente\n",
+ "\n",
+ "Hier erst einmal Illustration der Lösung von Folie 36.\n",
+ "Folgende Maschine hat keinen vordefinierten Wert von K; man muss diesen der :constants Anweisung übergeben."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 107,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: PostCorrespondence_MC"
+ ]
+ },
+ "execution_count": 107,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE PostCorrespondence_MC\n",
+ "/* Version wo die Schritt Operation nur sinnvolle Erweiterungen zulässt */\n",
+ "CONSTANTS K, Σ\n",
+ "PROPERTIES\n",
+ " Σ = {0,1} ∧\n",
+ " K ∈ seq(seq(Σ)×seq(Σ))\n",
+ "VARIABLES x,y\n",
+ "INVARIANT\n",
+ " x ∈ seq(Σ) ∧ y∈seq(Σ)\n",
+ "INITIALISATION x,y := <>,<>\n",
+ "OPERATIONS\n",
+ " Schritt(i,ix,iy) = PRE i∈dom(K) ∧ K(i)=ix↦iy\n",
+ " ∧ same_prefix(x^ix,y^iy) \n",
+ " /* kann man die beiden neuen Wörter überhaupt noch gleich machen ? */\n",
+ " THEN\n",
+ " x := x ^ ix || \n",
+ " y := y ^ iy\n",
+ " END;\n",
+ " Lösung = SELECT x=y ∧ x ≠ [] THEN skip END\n",
+ "DEFINITIONS\n",
+ " GOAL == (x=y ∧ x≠<>);\n",
+ " ANIMATION_FUNCTION == {1} × x ∪ {2} × y ; \n",
+ " ANIMATION_FUNCTION_DEFAULT == {(1,(0,2)),(2,(0,3))} ∪ {1,2}×λi.(i∈dom(x)∪dom(y)|6);\n",
+ " ANIMATION_IMG0 == \"images/sm_0.gif\";\n",
+ " ANIMATION_IMG1 == \"images/sm_1.gif\";\n",
+ " ANIMATION_IMG2 == \"images/sm_X.gif\";\n",
+ " ANIMATION_IMG3 == \"images/sm_Y.gif\";\n",
+ " ANIMATION_IMG6 == \"images/sm_empty_box.gif\";\n",
+ " SET_PREF_PP_SEQUENCES == TRUE;\n",
+ " same_prefix(a,b) == LET ms BE ms=min({size(a),size(b)}) IN\n",
+ " a /|\\ ms = b /|\\ ms END\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 108,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 108,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants K = [ [0,1]↦[1], [0,1,0]↦[1,0,0], [1]↦[1,0] ]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 109,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 109,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 110,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(3,[1],[1,0])"
+ ]
+ },
+ "execution_count": 110,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 111,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 111,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 112,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(2,[0,1,0],[1,0,0])"
+ ]
+ },
+ "execution_count": 112,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 113,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 113,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 114,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(2,[0,1,0],[1,0,0])"
+ ]
+ },
+ "execution_count": 114,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 115,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 115,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 116,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(1,[0,1],[1])"
+ ]
+ },
+ "execution_count": 116,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 117,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 117,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wir haben eine Lösung gefunden."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 118,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed to state with index -1"
+ ]
+ },
+ "execution_count": 118,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":goto -1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 119,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 11: $setup_constants()"
+ ]
+ },
+ "execution_count": 119,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants K = [ [0,0,1]↦[0], [0,1]↦[0,1,1], [0,1]↦[1,0,1], [1,0] ↦ [0,0,1] ]"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 120,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 12: $initialise_machine()"
+ ]
+ },
+ "execution_count": 120,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 121,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_MC\n",
+ "Sets: (none)\n",
+ "Constants: K, Σ\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(1,[0,0,1],[0])\n",
+ "Schritt(2,[0,1],[0,1,1])"
+ ]
+ },
+ "execution_count": 121,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 122,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(2,[0,1],[0,1,1])"
+ ]
+ },
+ "execution_count": 122,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 123,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(4,[1,0],[0,0,1])"
+ ]
+ },
+ "execution_count": 123,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=4"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 124,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/sm_X.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"6\" src=\"images/sm_empty_box.gif\"/></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/sm_Y.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/sm_0.gif\"/></td>\n",
+ "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/sm_1.gif\"/></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 124,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "jetzt fehlen nur noch 64 Schritte bis zu einer Lösung.\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Kodierung des Halteproblems als MPCP Problem\n",
+ "\n",
+ "Folgende B Maschine kodiert das Halteproblem einer Turingmaschine als MPCP Problem.\n",
+ "Der erste Schritt zu einer Lösung wird in der Initialisierung kodiert; dort wir erzwungen, dass wir das erste Paar aus dem Skript $(\\#,\\# z_0 w)$ benutzen.\n",
+ "Die Turing Maschine hat 3 Zustände: z0,z1,z2.\n",
+ "z2 ist der Endzustand.\n",
+ "z0 akzeptiert a and wechselt bei einem b zu z1, z1 akzeptiert b's und geht zu z2 bei einem Blank. \n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 125,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: PostCorrespondence_Turing_MC"
+ ]
+ },
+ "execution_count": 125,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE PostCorrespondence_Turing_MC\n",
+ "/* The Turing machine has 3 states: z0,z1,z2; z2 is Final\n",
+ " z0 accepts a and goes to z1 via b; z1 accepts b and goes to z2 via Blank \n",
+ "*/\n",
+ "SETS\n",
+ " Σ={a,b,Blank,z0,z1,z2,Hash}\n",
+ "CONSTANTS K\n",
+ "PROPERTIES\n",
+ " K = [ [a]↦[a], [b]↦[b], [Hash] ↦ [Hash] /* Copy Regeln */\n",
+ " ,\n",
+ " [z0,a] ↦ [a,z0], [z0,b] ↦ [b,z1],\n",
+ " [z1,b] ↦ [b,z1], [z1,Hash] ↦ [z2,Hash] /* Transitionen der TM */\n",
+ " ,\n",
+ " [a,z2] ↦ [z2], [b,z2] ↦ [z2] /* Löschregeln für Endzustände */\n",
+ " ,\n",
+ " [z2,Hash,Hash] |-> [Hash] /* Abschlussregeln für Endzustände */\n",
+ " ]\n",
+ "VARIABLES x,y\n",
+ "INVARIANT\n",
+ " x∈seq(Σ) ∧ y∈seq(Σ)\n",
+ "INITIALISATION x,y := [Hash],[Hash,z0,a,b,Hash] /* Start configuration */\n",
+ "OPERATIONS\n",
+ " Schritt(i,ix,iy) = PRE i∈dom(K) ∧ K(i)=ix↦iy\n",
+ " ∧ same_prefix(x^ix,y^iy) \n",
+ " /* kann man die beiden neuen Wörter überhaupt noch gleich machen ? */\n",
+ " THEN\n",
+ " x := x ^ ix || \n",
+ " y := y ^ iy\n",
+ " END;\n",
+ " Lösung = SELECT x=y ∧ x ≠ [] THEN skip END\n",
+ "DEFINITIONS\n",
+ " GOAL == (x=y ∧ x≠<>);\n",
+ " ANIMATION_FUNCTION == {1}*x \\/ {2} * y ; \n",
+ " ANIMATION_FUNCTION_DEFAULT == {(1,0,\"x\"),(2,0,\"y\")};\n",
+ " SET_PREF_MAX_OPERATIONS == 20;\n",
+ " SET_PREF_PP_SEQUENCES == TRUE;\n",
+ " same_prefix(a,b) == LET ms BE ms=min({size(a),size(b)}) IN\n",
+ " a /|\\ ms = b /|\\ ms END\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 126,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 126,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 127,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 127,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 128,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 128,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 129,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(4,[z0,a],[a,z0])"
+ ]
+ },
+ "execution_count": 129,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 130,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(4,[z0,a],[a,z0])"
+ ]
+ },
+ "execution_count": 130,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=4"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 131,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 131,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wir haben jetzt die Zuständsänderung ausgeführt; der neue Zustand befindet sich in der y-Reihe. Hier ist der neue Zustand gleich dem alten Zustand.\n",
+ "Jetzt müssen noch die Kopierregeln angewendet werden um den unveränderten Bandinhalt zu kopieren."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 132,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(2,[b],[b])"
+ ]
+ },
+ "execution_count": 132,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 133,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(2,[b],[b])"
+ ]
+ },
+ "execution_count": 133,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 134,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(3,[Hash],[Hash])"
+ ]
+ },
+ "execution_count": 134,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 135,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(3,[Hash],[Hash])"
+ ]
+ },
+ "execution_count": 135,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 136,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 136,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 137,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(1,[a],[a])"
+ ]
+ },
+ "execution_count": 137,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Jetzt muss noch der Bandinhalt links vom Schreibkopf kopiert werden:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 138,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(1,[a],[a])"
+ ]
+ },
+ "execution_count": 138,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 139,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 139,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 140,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(5,[z0,b],[b,z1])"
+ ]
+ },
+ "execution_count": 140,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 141,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(5,[z0,b],[b,z1])"
+ ]
+ },
+ "execution_count": 141,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 142,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 142,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Jetzt haben wir den Zustand gewechselt; wir müssen wieder kopieren."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 143,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(3,[Hash],[Hash])"
+ ]
+ },
+ "execution_count": 143,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 144,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(1,[a],[a])"
+ ]
+ },
+ "execution_count": 144,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 145,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 145,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 146,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(2,[b],[b])"
+ ]
+ },
+ "execution_count": 146,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 147,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 147,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 148,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(7,[z1,Hash],[z2,Hash])"
+ ]
+ },
+ "execution_count": 148,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 149,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(7,[z1,Hash],[z2,Hash])"
+ ]
+ },
+ "execution_count": 149,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=7"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 150,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 150,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Jetzt haben wir in den Endzustand z2 gewechselt. Bald greifen die Löschregeln um eine Lösung zu produzieren."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 151,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(1,[a],[a])"
+ ]
+ },
+ "execution_count": 151,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 152,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(1,[a],[a])"
+ ]
+ },
+ "execution_count": 152,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 153,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 153,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 154,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(2,[b],[b])\n",
+ "Schritt(9,[b,z2],[z2])"
+ ]
+ },
+ "execution_count": 154,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Jetzt greift die Löschregel 9."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 155,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(9,[b,z2],[z2])"
+ ]
+ },
+ "execution_count": 155,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=9"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 156,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 156,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 157,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(3,[Hash],[Hash])"
+ ]
+ },
+ "execution_count": 157,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 158,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(3,[Hash],[Hash])"
+ ]
+ },
+ "execution_count": 158,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 159,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 159,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 160,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(1,[a],[a])\n",
+ "Schritt(8,[a,z2],[z2])"
+ ]
+ },
+ "execution_count": 160,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wir können wieder ein Symbol löschen."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 161,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(8,[a,z2],[z2])"
+ ]
+ },
+ "execution_count": 161,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=8"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 162,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 162,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 163,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(3,[Hash],[Hash])"
+ ]
+ },
+ "execution_count": 163,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 164,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 164,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 165,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PostCorrespondence_Turing_MC\n",
+ "Sets: Σ\n",
+ "Constants: K\n",
+ "Variables: x, y\n",
+ "Operations: \n",
+ "Schritt(10,[z2,Hash,Hash],[Hash])"
+ ]
+ },
+ "execution_count": 165,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Jetzt greift die Abschlussregel um endlich eine Lösung zu finden."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 166,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Schritt(10,[z2,Hash,Hash],[Hash])"
+ ]
+ },
+ "execution_count": 166,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Schritt i=10"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 167,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">x</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">y</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z0</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z1</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">b</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">a</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">z2</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "<td style=\"padding:10px\">Hash</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 167,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 168,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Lösung()"
+ ]
+ },
+ "execution_count": 168,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Lösung"
+ ]
+ },
+ {
+ "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": 2
+}
diff --git a/info4/kapitel-11/images/sm_0.gif b/info4/kapitel-11/images/sm_0.gif
new file mode 100644
index 0000000000000000000000000000000000000000..b439a1ff3c60e196637e9e0b6ce4a9826a39bcb2
Binary files /dev/null and b/info4/kapitel-11/images/sm_0.gif differ
diff --git a/info4/kapitel-11/images/sm_1.gif b/info4/kapitel-11/images/sm_1.gif
new file mode 100644
index 0000000000000000000000000000000000000000..d8e44e8a29b28259369b23cd168a4a7693f6b55a
Binary files /dev/null and b/info4/kapitel-11/images/sm_1.gif differ
diff --git a/info4/kapitel-11/images/sm_Square_red.gif b/info4/kapitel-11/images/sm_Square_red.gif
new file mode 100644
index 0000000000000000000000000000000000000000..208b25d35a9aa5f6020b9f85bd6d43f25b900014
Binary files /dev/null and b/info4/kapitel-11/images/sm_Square_red.gif differ
diff --git a/info4/kapitel-11/images/sm_X.gif b/info4/kapitel-11/images/sm_X.gif
new file mode 100644
index 0000000000000000000000000000000000000000..7751d5cf41d6acee52e078b0f27dc2fb70640067
Binary files /dev/null and b/info4/kapitel-11/images/sm_X.gif differ
diff --git a/info4/kapitel-11/images/sm_Y.gif b/info4/kapitel-11/images/sm_Y.gif
new file mode 100644
index 0000000000000000000000000000000000000000..7a721090e9c8153df9980ee7a87705fce82f3154
Binary files /dev/null and b/info4/kapitel-11/images/sm_Y.gif differ
diff --git a/info4/kapitel-11/images/sm_bullet_box.gif b/info4/kapitel-11/images/sm_bullet_box.gif
new file mode 100644
index 0000000000000000000000000000000000000000..0ecac36325545ab3ca4b258c03c545348b587ce2
Binary files /dev/null and b/info4/kapitel-11/images/sm_bullet_box.gif differ
diff --git a/info4/kapitel-11/images/sm_empty_box.gif b/info4/kapitel-11/images/sm_empty_box.gif
new file mode 100644
index 0000000000000000000000000000000000000000..0f33c780ae8e000a17f340b75a3b90f5450f6c9c
Binary files /dev/null and b/info4/kapitel-11/images/sm_empty_box.gif differ