{
 "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",
    "\n",
    "Bei dem $MPCP_\\Sigma$ Problem verlangen wir, dass $i_1=1$.\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": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: PostCorrespondence_MC"
      ]
     },
     "execution_count": 1,
     "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": 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": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$[([1]\\mapsto [1,0]),([0,1]\\mapsto [1]),([0,1,0]\\mapsto [1,0,0])]$"
      ],
      "text/plain": [
       "[([1]↦[1,0]),([0,1]↦[1]),([0,1,0]↦[1,0,0])]"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "K"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "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": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "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": 6,
     "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": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(1,[1],[1,0])"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "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": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$[1]$"
      ],
      "text/plain": [
       "[1]"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$[1,0]$"
      ],
      "text/plain": [
       "[1,0]"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "y"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "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": 11,
     "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": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(2,[0,1],[1])"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "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": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Lösung()"
      ]
     },
     "execution_count": 14,
     "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": 15,
   "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": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":trace"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Changed to state with index 2"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":goto 2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "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": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(3,[0,1,0],[1,0,0])"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "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": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(3,[0,1,0],[1,0,0])"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "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": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(2,[0,1],[1])"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "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": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Lösung()"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Lösung"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "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": 25,
     "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; kleinste 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": 26,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: PostCorrespondence_MC"
      ]
     },
     "execution_count": 26,
     "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": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 27,
     "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": 28,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(3,[1],[1,0])"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "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": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(2,[0,1,0],[1,0,0])"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "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": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(2,[0,1,0],[1,0,0])"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "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": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(1,[0,1],[1])"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "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": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Wir haben eine Lösung gefunden."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Changed to state with index -1"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":goto -1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 11: $setup_constants()"
      ]
     },
     "execution_count": 38,
     "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": 39,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 12: $initialise_machine()"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "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": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(2,[0,1],[0,1,1])"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(4,[1,0],[0,0,1])"
      ]
     },
     "execution_count": 42,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=4"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "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": 43,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Jetzt fehlen nur noch 64 Schritte bis zu einer Lösung."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(3,[0,1],[1,0,1])"
      ]
     },
     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(4,[1,0],[0,0,1])"
      ]
     },
     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=4"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(4,[1,0],[0,0,1])"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=4"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(2,[0,1],[0,1,1])"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "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=\"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=\"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=\"6\" src=\"images/sm_empty_box.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",
       "<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",
       "<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",
       "<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",
       "<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",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "jetzt fehlen nur noch 60 Schritte bis zu der kürzesten Lösung.\n",
    "Die gesamte Lösung ist:\n",
    "\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(3,[0,1],[1,0,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(2,[0,1],[0,1,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(4,[1,0],[0,0,1])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(1,[0,0,1],[0])\n",
    "Schritt(3,[0,1],[1,0,1])\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 wird 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. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: PostCorrespondence_Turing_MC"
      ]
     },
     "execution_count": 49,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE PostCorrespondence_Turing_MC\n",
    "/* The Turing machine has 3 states: z0,z1,z2; z2 ist ein Endzustand\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": 50,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 50,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 51,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "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": 52,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "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": 53,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(4,[z0,a],[a,z0])"
      ]
     },
     "execution_count": 54,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=4"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "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": 55,
     "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": 56,
   "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": 56,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(2,[b],[b])"
      ]
     },
     "execution_count": 57,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "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": 58,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(3,[Hash],[Hash])"
      ]
     },
     "execution_count": 59,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "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": 60,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "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": 61,
     "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": 62,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(1,[a],[a])"
      ]
     },
     "execution_count": 62,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "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": 63,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "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": 64,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(5,[z0,b],[b,z1])"
      ]
     },
     "execution_count": 65,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=5"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "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": 66,
     "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": 67,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(3,[Hash],[Hash])"
      ]
     },
     "execution_count": 67,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(1,[a],[a])"
      ]
     },
     "execution_count": 68,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "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": 69,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(2,[b],[b])"
      ]
     },
     "execution_count": 70,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "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": 71,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "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": 72,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(7,[z1,Hash],[z2,Hash])"
      ]
     },
     "execution_count": 73,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=7"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "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": 74,
     "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": 75,
   "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": 75,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(1,[a],[a])"
      ]
     },
     "execution_count": 76,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 77,
   "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": 77,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 78,
   "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": 78,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Jetzt greift die Löschregel 9."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 79,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(9,[b,z2],[z2])"
      ]
     },
     "execution_count": 79,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=9"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 80,
   "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": 80,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 81,
   "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": 81,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 82,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(3,[Hash],[Hash])"
      ]
     },
     "execution_count": 82,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 83,
   "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": 83,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 84,
   "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": 84,
     "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": 85,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(8,[a,z2],[z2])"
      ]
     },
     "execution_count": 85,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=8"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 86,
   "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": 86,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 87,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(3,[Hash],[Hash])"
      ]
     },
     "execution_count": 87,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 88,
   "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": 88,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 89,
   "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": 89,
     "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": 90,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Schritt(10,[z2,Hash,Hash],[Hash])"
      ]
     },
     "execution_count": 90,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec Schritt i=10"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 91,
   "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": 91,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 92,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: Lösung()"
      ]
     },
     "execution_count": 92,
     "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
}