{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\newcommand{\\Inter}{\\bigcap\\nolimits}\\newcommand{\\bfalse}{\\mathord\\bot}\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}\\newcommand{\\binter}{\\mathbin{\\mkern1mu\\cap\\mkern1mu}}\\newcommand{\\dprod}{\\mathbin\\otimes}\\newcommand{\\usucc}{\\mathop{\\mathrm{succ}}\\nolimits}\\newcommand{\\trel}{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>}}\\newcommand{\\strel}{\\mathbin{<\\mkern-6mu<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}\\newcommand{\\Bool}{\\mathord{\\mathrm{BOOL}}}\\newcommand{\\rel}{\\mathbin{<\\mkern-10mu-\\mkern-10mu>}}\\newcommand{\\pprod}{\\mathbin\\mid}\\newcommand{\\id}{\\mathop{\\mathrm{id}}\\nolimits}\\newcommand{\\cprod}{\\mathbin\\times}\\newcommand{\\ran}{\\mathop{\\mathrm{ran}}\\nolimits}\\newcommand{\\nat}{\\mathord{\\mathbb N}}\\newcommand{\\pown}{\\mathop{\\mathbb P_1}\\nolimits}\\newcommand{\\finite}{\\mathop{\\mathrm{finite}}\\nolimits}\\newcommand{\\inter}{\\mathop{\\mathrm{inter}}\\nolimits}\\newcommand{\\prjone}{\\mathop{\\mathrm{prj}_1}\\nolimits}\\newcommand{\\defi}{\\mathrel{≙}}\\newcommand{\\ranres}{\\mathbin▷}\\newcommand{\\prjtwo}{\\mathop{\\mathrm{prj}_2}\\nolimits}\\newcommand{\\upred}{\\mathop{\\mathrm{pred}}\\nolimits}\\newcommand{\\fcomp}{\\mathbin;}\\newcommand{\\tbij}{\\mathbin⤖}\\newcommand{\\pfun}{\\mathbin↦}\\newcommand{\\tfun}{\\mathbin→}\\newcommand{\\card}{\\mathop{\\mathrm{card}}\\nolimits}\\newcommand{\\pinj}{\\mathbin⤔}\\newcommand{\\dom}{\\mathop{\\mathrm{dom}}\\nolimits}\\newcommand{\\bool}{\\mathop{\\mathrm{bool}}\\nolimits}\\newcommand{\\tinj}{\\mathbin↣}\\newcommand{\\domsub}{\\mathbin⩤}\\newcommand{\\Union}{\\bigcup\\nolimits}\\newcommand{\\limp}{\\mathbin\\Rightarrow}\\newcommand{\\ransub}{\\mathbin⩥}\\newcommand{\\psur}{\\mathbin⤅}\\newcommand{\\pow}{\\mathop{\\mathbb P\\hbox{}}\\nolimits}\\newcommand{\\bcmsuch}{\\mathrel{:\\mkern1mu\\mid}}\\newcommand{\\natn}{\\mathord{\\mathbb N_1}}\\newcommand{\\expn}{\\mathbin{\\widehat{\\mkern1em}}}\\newcommand{\\upto}{\\mathbin{.\\mkern1mu.}}\\newcommand{\\bcomp}{\\circ}\\newcommand{\\bcmin}{\\mathrel{:\\mkern1mu\\in}}\\newcommand{\\ovl}{\\mathbin{<\\mkern-11mu+}}\\newcommand{\\intg}{\\mathord{\\mathbb Z}}\\newcommand{\\domres}{\\mathbin◁}\\newcommand{\\tsur}{\\mathbin↠}\\newcommand{\\btrue}{\\mathord\\top}\\newcommand{\\union}{\\mathop{\\mathrm{union}}\\nolimits}\\newcommand{\\bcmeq}{\\mathrel{:\\mkern1mu=}}\\newcommand{\\leqv}{\\mathbin\\Leftrightarrow}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\newcommand{\\bunion}{\\mathbin{\\mkern1mu\\cup\\mkern1mu}}\\newcommand{\\srel}{\\mathbin{<\\mkern-10mu-\\mkern-10mu>\\mkern-6mu>}}\\text{All bsymb.sty definitions have been loaded.}$"
      ],
      "text/plain": [
       "Your current environment uses plain text output; the bsymb.sty LaTeX commands will not be loaded."
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":bsymb"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Application: Course Notes for Theoretical Computer Science (NFA)\n",
    "\n",
    "\n",
    "\n",
    "#### DEFINITION 2.9 (NFA)\n",
    "A non-deterministic finite automaton\n",
    "(NFA) is a  5-tuple $M = (\\Sigma, Z, \\delta , S, F)$, where\n",
    "\n",
    "* $\\Sigma$ is the alphabet,\n",
    "* $Z$ is a finite set of states with $\\Sigma \\cap Z = \\emptyset$,\n",
    "* $\\delta : Z \\times \\Sigma \\rightarrow POW(Z)$ is the transition function\n",
    "  ($\\pow(Z)$ is the powerset of $Z$, the set of all subsets of $Z$),\n",
    "* $S \\subseteq Z$ is the set of initial states,\n",
    "* $F \\subseteq Z$ is the set of final (accepting) states.\n",
    "\n",
    "\n",
    "#### DEFINITION 2.10 (Language of an NFA)\n",
    "\n",
    "Die erweiterte Überführungsfunktion $\\widehat{\\delta} :\n",
    "\\pow(Z) \\times \\Sigma^* \\rightarrow \\pow(Z)$ von $M$ ist\n",
    "induktiv definiert:\n",
    "* $\\widehat{\\delta}(Z', \\lambda) = Z'$\n",
    "* $\\widehat{\\delta}(Z', ax) = \\bigcup_{z \\in Z'} \\widehat{\\delta}(\\delta(z,a), x)$\n",
    "für alle $Z' \\subseteq Z$, $a \\in \\Sigma$ und $x \\in \\Sigma^*$.\n",
    "\n",
    "Die vom NFA $M$ akzeptierte Sprache ist definiert durch\n",
    "* L(M) = $\\{w \\in \\Sigma^* \\mid \\widehat{\\delta}(S,w) \\cap F \\neq \\emptyset\\}$\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Wie laden nun ein B Modell welches diese Definitionen beinhaltet.\n",
    "Wörter werden dabei in der B Sprache mit eckigen Klammern und Kommas geschrieben; aus 101 wird [1,0,1].\n",
    "Gewisse griechische Zeichen sind in der B Sprache als Schlüsselwörter reserviert, zB $\\lambda$.\n",
    "Auch kann man leider kein $\\hat{~}$ in Bezeichnern verwenden.\n",
    "Deshalb wird aus\n",
    "* $\\Sigma^*$ wird ```seq(Σ)```\n",
    "* $\\widehat{\\delta}$ wird ```δs```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: NFA_nach_DFA"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE NFA_nach_DFA\n",
    "SETS\n",
    "   Z = {z0,z1,z2,z3}\n",
    "ABSTRACT_CONSTANTS δs, L\n",
    "CONSTANTS Σ, S, F, δ\n",
    "PROPERTIES\n",
    " S ⊆ Z ∧ F ⊆ Z ∧ δ ∈ (Z×Σ) → ℙ(Z) ∧\n",
    "\n",
    " /* Definition der erweiterten Übergangsfunktion */\n",
    " δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(Z) ∧\n",
    " δs = λ(Z2,s).(Z2⊆Z ∧ s∈seq(Σ) | \n",
    "           IF s=[] THEN Z2\n",
    "           ELSE         ⋃(z).(z∈Z2|δs(δ(z,first(s)),tail(s))) END)\n",
    " ∧\n",
    " /* die vom Automaten generierte Sprache */\n",
    " L = {ω|ω∈seq(Σ) ∧ δs(S,ω) ∩ F ≠ ∅}\n",
    " ∧\n",
    " /* Nun ein Beispiel-Automat von Folie 24 (Info 4) */\n",
    " Σ = {0,1} ∧\n",
    " S = {z0} ∧ F={z2} ∧\n",
    " δ = {     (z0,0)↦{z0}, (z0,1)↦{z0,z1},\n",
    "           (z1,0)↦{z2}, (z1,1)↦{z2},\n",
    "           (z2,0)↦{z3}, (z2,1)↦{z3},\n",
    "           (z3,0)↦{z3}, (z3,1)↦{z3} }\n",
    "END"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die Übergangsfunktion $\\delta$ gibt us für einen Zustand und ein Symbol die möglichen nächsten Zustande an:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{\\mathit{z0},\\mathit{z1}\\}$"
      ],
      "text/plain": [
       "{z0,z1}"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "δ(z0,1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As you can see, the automaton is non-deterministic as there are two successors for the state ```z0``` and the input symbol ```1```.\n",
    "\n",
    "We can examine the transition function of this automaton as a table:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "|prj11|prj12|prj2|\n",
       "|---|---|---|\n",
       "|$\\mathit{z0}$|$0$|$\\{\\mathit{z0}\\}$|\n",
       "|$\\mathit{z0}$|$1$|$\\{\\mathit{z0},\\mathit{z1}\\}$|\n",
       "|$\\mathit{z1}$|$0$|$\\{\\mathit{z2}\\}$|\n",
       "|$\\mathit{z1}$|$1$|$\\{\\mathit{z2}\\}$|\n",
       "|$\\mathit{z2}$|$0$|$\\{\\mathit{z3}\\}$|\n",
       "|$\\mathit{z2}$|$1$|$\\{\\mathit{z3}\\}$|\n",
       "|$\\mathit{z3}$|$0$|$\\{\\mathit{z3}\\}$|\n",
       "|$\\mathit{z3}$|$1$|$\\{\\mathit{z3}\\}$|\n"
      ],
      "text/plain": [
       "prj11\tprj12\tprj2\n",
       "z0\t0\t{z0}\n",
       "z0\t1\t{z0,z1}\n",
       "z1\t0\t{z2}\n",
       "z1\t1\t{z2}\n",
       "z2\t0\t{z3}\n",
       "z2\t1\t{z3}\n",
       "z3\t0\t{z3}\n",
       "z3\t1\t{z3}\n"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":table δ"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Alternatively, we can view it as graph:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
       " -->\n",
       "<!-- Title: state Pages: 1 -->\n",
       "<svg width=\"146pt\" height=\"472pt\"\n",
       " viewBox=\"0.00 0.00 146.00 472.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 468)\">\n",
       "<title>state</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-468 142,-468 142,4 -4,4\"/>\n",
       "<g id=\"clust1\" class=\"cluster\">\n",
       "<title>cluster_Z</title>\n",
       "<polygon fill=\"#d3d3d3\" stroke=\"#d3d3d3\" points=\"8,-8 8,-456 130,-456 130,-8 8,-8\"/>\n",
       "<text text-anchor=\"middle\" x=\"69\" y=\"-442.4\" font-family=\"Times,serif\" font-size=\"12.00\" fill=\"#000000\">Z</text>\n",
       "</g>\n",
       "<!-- z0 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>z0</title>\n",
       "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-427 16,-427 16,-391 70,-391 70,-427\"/>\n",
       "<text text-anchor=\"middle\" x=\"43\" y=\"-405.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z0</text>\n",
       "</g>\n",
       "<!-- z0&#45;&gt;z0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>z0&#45;&gt;z0</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M70.2408,-412.3717C80.0239,-412.4442 88,-411.3203 88,-409 88,-407.5861 85.0382,-406.6164 80.5105,-406.091\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"80.3882,-402.582 70.2408,-405.6283 80.0731,-409.5749 80.3882,-402.582\"/>\n",
       "<text text-anchor=\"middle\" x=\"92\" y=\"-405.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- z0&#45;&gt;z0 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>z0&#45;&gt;z0</title>\n",
       "<path fill=\"none\" stroke=\"#a0522d\" d=\"M70.1975,-415.1551C88.3402,-416.8876 106,-414.8359 106,-409 106,-404.2583 94.3418,-402.0148 80.2386,-402.2695\"/>\n",
       "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"79.9809,-398.7784 70.1975,-402.8449 80.3814,-405.7669 79.9809,-398.7784\"/>\n",
       "<text text-anchor=\"middle\" x=\"110\" y=\"-405.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- z1 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>z1</title>\n",
       "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-302 16,-302 16,-266 70,-266 70,-302\"/>\n",
       "<text text-anchor=\"middle\" x=\"43\" y=\"-280.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z1</text>\n",
       "</g>\n",
       "<!-- z0&#45;&gt;z1 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>z0&#45;&gt;z1</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M43,-390.8239C43,-370.2723 43,-336.5472 43,-312.4893\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"46.5001,-312.198 43,-302.198 39.5001,-312.198 46.5001,-312.198\"/>\n",
       "<text text-anchor=\"middle\" x=\"47\" y=\"-342.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- z2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>z2</title>\n",
       "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-177 16,-177 16,-141 70,-141 70,-177\"/>\n",
       "<text text-anchor=\"middle\" x=\"43\" y=\"-155.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z2</text>\n",
       "</g>\n",
       "<!-- z1&#45;&gt;z2 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>z1&#45;&gt;z2</title>\n",
       "<path fill=\"none\" stroke=\"#a0522d\" d=\"M43,-265.8239C43,-245.2723 43,-211.5472 43,-187.4893\"/>\n",
       "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"46.5001,-187.198 43,-177.198 39.5001,-187.198 46.5001,-187.198\"/>\n",
       "<text text-anchor=\"middle\" x=\"47\" y=\"-217.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- z3 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>z3</title>\n",
       "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-52 16,-52 16,-16 70,-16 70,-52\"/>\n",
       "<text text-anchor=\"middle\" x=\"43\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">z3</text>\n",
       "</g>\n",
       "<!-- z3&#45;&gt;z3 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>z3&#45;&gt;z3</title>\n",
       "<path fill=\"none\" stroke=\"#a0522d\" d=\"M70.2408,-40.7434C80.0239,-40.8884 88,-38.6406 88,-34 88,-31.1721 85.0382,-29.2328 80.5105,-28.182\"/>\n",
       "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"80.5146,-24.6683 70.2408,-27.2566 79.8863,-31.64 80.5146,-24.6683\"/>\n",
       "<text text-anchor=\"middle\" x=\"92\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- z2&#45;&gt;z3 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>z2&#45;&gt;z3</title>\n",
       "<path fill=\"none\" stroke=\"#a0522d\" d=\"M43,-140.8239C43,-120.2723 43,-86.5472 43,-62.4893\"/>\n",
       "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"46.5001,-62.198 43,-52.198 39.5001,-62.198 46.5001,-62.198\"/>\n",
       "<text text-anchor=\"middle\" x=\"47\" y=\"-92.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:Z & y:δ(x, 0)})]>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":dot expr_as_graph (\"0\",{x,y| x∈Z & y:δ(x,0)},\n",
    "                    \"1\",{x,y| x∈S & y∈δ(x,1)})"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die Funktion $\\widehat{\\delta}$ berechnet die möglichen Zustände nach dem Abarbeiten eines Wortes. Zum Beispiel, kann sich der Automat nach dem Abarbeiten des Präfixes 111 in folgenden Zuständen befinden:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$"
      ],
      "text/plain": [
       "{z0,z1,z2,z3}"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "δs(S,[1,1,1])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Der Automat akzeptiert zum Beispiel das Wort 111 und das Wort 101 nicht, da:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{\\mathit{z2}\\}$"
      ],
      "text/plain": [
       "{z2}"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "δs(S,[1,1,1]) ∩ F"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Folgende Wörter der Länge 3 werden vom Automaten akzeptiert:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "|x|y|z|\n",
       "|---|---|---|\n",
       "|$0$|$1$|$0$|\n",
       "|$0$|$1$|$1$|\n",
       "|$1$|$1$|$0$|\n",
       "|$1$|$1$|$1$|\n"
      ],
      "text/plain": [
       "x\ty\tz\n",
       "0\t1\t0\n",
       "0\t1\t1\n",
       "1\t1\t0\n",
       "1\t1\t1\n"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":table {x,y,z| [x,y,z]∈L}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "and the following words of length 3 are not accepted:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "|x|y|z|\n",
       "|---|---|---|\n",
       "|$0$|$0$|$0$|\n",
       "|$0$|$0$|$1$|\n",
       "|$1$|$0$|$0$|\n",
       "|$1$|$0$|$1$|\n"
      ],
      "text/plain": [
       "x\ty\tz\n",
       "0\t0\t0\n",
       "0\t0\t1\n",
       "1\t0\t0\n",
       "1\t0\t1\n"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":table {x,y,z| {x,y,z} ⊆ Σ & ¬([x,y,z]∈L)}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Es stellt sich die Frage, ob NFAs mächtiger sind als DFAs. Die \n",
    "Antwort lautet: Nein.\n",
    "\n",
    "## Theorem (Rabin und Scott)\n",
    "Jede von einem NFA akzeptierte Sprache kann auch von einem DFA akzeptiert\n",
    "werden.\n",
    "\n",
    "### Beweis\n",
    "Sei $M = (\\Sigma, Z, \\delta , S, E)$ ein NFA. \n",
    "Konstruiere einen zu\n",
    "  $M$ äquivalenten DFA \n",
    "  $M' = (\\Sigma, \\pow(Z), \\delta' ,z_0', F)$ wie folgt:\n",
    "* Zustandsmenge von $M'$: die Potenzmenge $\\pow(Z)$ von $Z$,\n",
    "* $\\delta'(Z' , a) = \\widehat{\\delta}(Z',a)$ für alle $Z' \\subseteq Z$ und $a \\in \\Sigma$,\n",
    "* $z_0'=S$,\n",
    "* $F = \\{ Z' \\subseteq Z \\mid Z' \\cap E \\neq \\emptyset\\}$.\n",
    "Offenbar sind M' und M äquivalent, denn für alle ...\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Für den oben geladen Automaten können wir diese Konstruktion illustrieren.\n",
    "Die Potenzmenge der Zustände ist:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\{\\emptyset,\\{\\mathit{z0}\\},\\{\\mathit{z0},\\mathit{z1}\\},\\{\\mathit{z0},\\mathit{z2}\\},\\{\\mathit{z0},\\mathit{z3}\\},\\{\\mathit{z1}\\},\\{\\mathit{z0},\\mathit{z1},\\mathit{z2}\\},\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\},\\{\\mathit{z1},\\mathit{z2}\\},\\{\\mathit{z1},\\mathit{z3}\\},\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z2}\\},\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z1},\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z2},\\mathit{z3}\\},\\{\\mathit{z3}\\}\\}$"
      ],
      "text/plain": [
       "{∅,{z0},{z0,z1},{z0,z2},{z0,z3},{z1},{z0,z1,z2},{z0,z1,z3},{z1,z2},{z1,z3},{z0,z1,z2,z3},{z2},{z0,z2,z3},{z1,z2,z3},{z2,z3},{z3}}"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ℙ(Z)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Tabellarisch können wir $\\widehat{\\delta}$ für $\\pow(Z)$ wie folgt ausrechnen:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "|x|a|y|\n",
       "|---|---|---|\n",
       "|$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$|$0$|$\\emptyset$|\n",
       "|$\\emptyset$|$1$|$\\emptyset$|\n",
       "|$\\{\\mathit{z0}\\}$|$0$|$\\{\\mathit{z0}\\}$|\n",
       "|$\\{\\mathit{z0}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z1}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z2}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z1}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z2}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z2}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z1}\\}$|$0$|$\\{\\mathit{z2}\\}$|\n",
       "|$\\{\\mathit{z1}\\}$|$1$|$\\{\\mathit{z2}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z1},\\mathit{z2}\\}$|$0$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z1},\\mathit{z2}\\}$|$1$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z1},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z1},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z2}\\}$|$0$|$\\{\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z2}\\}$|$1$|$\\{\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z0},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z0},\\mathit{z2},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z0},\\mathit{z1},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z2},\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z2},\\mathit{z3}\\}$|$0$|$\\{\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z2},\\mathit{z3}\\}$|$1$|$\\{\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z3}\\}$|$0$|$\\{\\mathit{z3}\\}$|\n",
       "|$\\{\\mathit{z3}\\}$|$1$|$\\{\\mathit{z3}\\}$|\n"
      ],
      "text/plain": [
       "x\ta\ty\n",
       "{}\t0\t{}\n",
       "{}\t1\t{}\n",
       "{z0}\t0\t{z0}\n",
       "{z0}\t1\t{z0,z1}\n",
       "{z0,z1}\t0\t{z0,z2}\n",
       "{z0,z1}\t1\t{z0,z1,z2}\n",
       "{z0,z2}\t0\t{z0,z3}\n",
       "{z0,z2}\t1\t{z0,z1,z3}\n",
       "{z0,z3}\t0\t{z0,z3}\n",
       "{z0,z3}\t1\t{z0,z1,z3}\n",
       "{z1}\t0\t{z2}\n",
       "{z1}\t1\t{z2}\n",
       "{z0,z1,z2}\t0\t{z0,z2,z3}\n",
       "{z0,z1,z2}\t1\t{z0,z1,z2,z3}\n",
       "{z0,z1,z3}\t0\t{z0,z2,z3}\n",
       "{z0,z1,z3}\t1\t{z0,z1,z2,z3}\n",
       "{z1,z2}\t0\t{z2,z3}\n",
       "{z1,z2}\t1\t{z2,z3}\n",
       "{z1,z3}\t0\t{z2,z3}\n",
       "{z1,z3}\t1\t{z2,z3}\n",
       "{z0,z1,z2,z3}\t0\t{z0,z2,z3}\n",
       "{z0,z1,z2,z3}\t1\t{z0,z1,z2,z3}\n",
       "{z2}\t0\t{z3}\n",
       "{z2}\t1\t{z3}\n",
       "{z0,z2,z3}\t0\t{z0,z3}\n",
       "{z0,z2,z3}\t1\t{z0,z1,z3}\n",
       "{z1,z2,z3}\t0\t{z2,z3}\n",
       "{z1,z2,z3}\t1\t{z2,z3}\n",
       "{z2,z3}\t0\t{z3}\n",
       "{z2,z3}\t1\t{z3}\n",
       "{z3}\t0\t{z3}\n",
       "{z3}\t1\t{z3}\n"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":table {x,a,y| a∈Σ & x∈ℙ(Z) & y=δs(x,[a])}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Graphisch lässt sich der Automat wie folgt darstellen; die Start und Endzustände sind noch nicht schön markiert."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":pref DOT_DECOMPOSE_NODES=FALSE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
       " -->\n",
       "<!-- Title: state Pages: 1 -->\n",
       "<svg width=\"662pt\" height=\"566pt\"\n",
       " viewBox=\"0.00 0.00 662.00 566.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 562)\">\n",
       "<title>state</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-562 658,-562 658,4 -4,4\"/>\n",
       "<!-- \\{z2,z3\\} -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>\\{z2,z3\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"226,-471 166,-471 166,-435 226,-435 226,-471\"/>\n",
       "<text text-anchor=\"middle\" x=\"196\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z2,z3}</text>\n",
       "</g>\n",
       "<!-- \\{z2,z3\\}&#45;&gt;\\{z2,z3\\} -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>\\{z2,z3\\}&#45;&gt;\\{z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M226.4673,-460.8731C236.248,-460.7923 244,-458.168 244,-453 244,-449.8508 241.1214,-447.6461 236.6593,-446.3859\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"236.8209,-442.8794 226.4673,-445.1269 235.9627,-449.8266 236.8209,-442.8794\"/>\n",
       "<text text-anchor=\"middle\" x=\"254.5\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
       "</g>\n",
       "<!-- \\{z3\\} -->\n",
       "<g id=\"node10\" class=\"node\">\n",
       "<title>\\{z3\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"185,-384 131,-384 131,-348 185,-348 185,-384\"/>\n",
       "<text text-anchor=\"middle\" x=\"158\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z3}</text>\n",
       "</g>\n",
       "<!-- \\{z2,z3\\}&#45;&gt;\\{z3\\} -->\n",
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>\\{z2,z3\\}&#45;&gt;\\{z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M174.1924,-434.6451C169.3745,-429.4531 164.8587,-423.4437 162,-417 158.8801,-409.9675 157.4136,-401.8548 156.8388,-394.1981\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"160.3368,-394.0739 156.5362,-384.1842 153.34,-394.2854 160.3368,-394.0739\"/>\n",
       "<text text-anchor=\"middle\" x=\"166\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z2,z3\\}&#45;&gt;\\{z3\\} -->\n",
       "<g id=\"edge27\" class=\"edge\">\n",
       "<title>\\{z2,z3\\}&#45;&gt;\\{z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M188.1264,-434.9735C182.8784,-422.9585 175.8819,-406.9401 169.9523,-393.3646\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"173.0737,-391.7664 165.8635,-384.0034 166.6589,-394.5683 173.0737,-391.7664\"/>\n",
       "<text text-anchor=\"middle\" x=\"184\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z1,z2,z3\\} -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>\\{z1,z2,z3\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"149.5,-558 72.5,-558 72.5,-522 149.5,-522 149.5,-558\"/>\n",
       "<text text-anchor=\"middle\" x=\"111\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1,z2,z3}</text>\n",
       "</g>\n",
       "<!-- \\{z1,z2,z3\\}&#45;&gt;\\{z2,z3\\} -->\n",
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>\\{z1,z2,z3\\}&#45;&gt;\\{z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M111.9305,-521.819C113.3101,-511.2556 116.546,-498.2486 124,-489 132.3732,-478.611 144.5156,-470.9638 156.4511,-465.4583\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"158.0369,-468.5886 165.9028,-461.4908 155.3275,-462.1342 158.0369,-468.5886\"/>\n",
       "<text text-anchor=\"middle\" x=\"128\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z1,z2,z3\\}&#45;&gt;\\{z2,z3\\} -->\n",
       "<g id=\"edge28\" class=\"edge\">\n",
       "<title>\\{z1,z2,z3\\}&#45;&gt;\\{z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M128.6121,-521.9735C140.9208,-509.3752 157.5297,-492.3755 171.1785,-478.4055\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"173.9256,-480.6021 178.4105,-471.0034 168.9186,-475.7103 173.9256,-480.6021\"/>\n",
       "<text text-anchor=\"middle\" x=\"163\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z1,z2,z3\\}&#45;&gt;\\{z1,z2,z3\\} -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>\\{z1,z2,z3\\}&#45;&gt;\\{z1,z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M149.5552,-547.8058C159.7662,-547.3597 167.5,-544.7578 167.5,-540 167.5,-537.0264 164.479,-534.8949 159.7203,-533.6055\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"159.9415,-530.1027 149.5552,-532.1942 158.9788,-537.0362 159.9415,-530.1027\"/>\n",
       "<text text-anchor=\"middle\" x=\"178\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
       "</g>\n",
       "<!-- \\{z0,z2,z3\\} -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>\\{z0,z2,z3\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"349.5,-297 272.5,-297 272.5,-261 349.5,-261 349.5,-297\"/>\n",
       "<text text-anchor=\"middle\" x=\"311\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z2,z3}</text>\n",
       "</g>\n",
       "<!-- \\{z0,z2,z3\\}&#45;&gt;\\{z0,z2,z3\\} -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>\\{z0,z2,z3\\}&#45;&gt;\\{z0,z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M349.5552,-286.8058C359.7662,-286.3597 367.5,-283.7578 367.5,-279 367.5,-276.0264 364.479,-273.8949 359.7203,-272.6055\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"359.9415,-269.1027 349.5552,-271.1942 358.9788,-276.0362 359.9415,-269.1027\"/>\n",
       "<text text-anchor=\"middle\" x=\"378\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z3\\} -->\n",
       "<g id=\"node11\" class=\"node\">\n",
       "<title>\\{z0,z1,z3\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"393.5,-123 316.5,-123 316.5,-87 393.5,-87 393.5,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"355\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1,z3}</text>\n",
       "</g>\n",
       "<!-- \\{z0,z2,z3\\}&#45;&gt;\\{z0,z1,z3\\} -->\n",
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>\\{z0,z2,z3\\}&#45;&gt;\\{z0,z1,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M311.8901,-260.86C313.2776,-239.6836 316.7192,-203.7656 325,-174 328.9228,-159.8994 335.1587,-144.9239 340.9314,-132.5406\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"344.2285,-133.7603 345.4087,-123.2314 337.9202,-130.7263 344.2285,-133.7603\"/>\n",
       "<text text-anchor=\"middle\" x=\"329\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z0,z3\\} -->\n",
       "<g id=\"node14\" class=\"node\">\n",
       "<title>\\{z0,z3\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"487,-210 427,-210 427,-174 487,-174 487,-210\"/>\n",
       "<text text-anchor=\"middle\" x=\"457\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z3}</text>\n",
       "</g>\n",
       "<!-- \\{z0,z2,z3\\}&#45;&gt;\\{z0,z3\\} -->\n",
       "<g id=\"edge29\" class=\"edge\">\n",
       "<title>\\{z0,z2,z3\\}&#45;&gt;\\{z0,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M341.2513,-260.9735C363.47,-247.7336 393.8464,-229.6326 417.9059,-215.2958\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"419.9886,-218.1291 426.7875,-210.0034 416.4053,-212.1157 419.9886,-218.1291\"/>\n",
       "<text text-anchor=\"middle\" x=\"396\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z2\\} -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>\\{z2\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"92,-471 38,-471 38,-435 92,-435 92,-471\"/>\n",
       "<text text-anchor=\"middle\" x=\"65\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z2}</text>\n",
       "</g>\n",
       "<!-- \\{z2\\}&#45;&gt;\\{z2\\} -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>\\{z2\\}&#45;&gt;\\{z2\\}</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M92.2408,-460.8673C102.0239,-461.0365 110,-458.4141 110,-453 110,-449.7008 107.0382,-447.4382 102.5105,-446.2123\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"102.5519,-442.6975 92.2408,-445.1327 101.82,-449.6591 102.5519,-442.6975\"/>\n",
       "<text text-anchor=\"middle\" x=\"120.5\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
       "</g>\n",
       "<!-- \\{z2\\}&#45;&gt;\\{z3\\} -->\n",
       "<g id=\"edge14\" class=\"edge\">\n",
       "<title>\\{z2\\}&#45;&gt;\\{z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M70.7229,-434.7868C74.7704,-424.2121 81.0778,-411.2043 90,-402 98.8615,-392.8583 110.5505,-385.5335 121.7332,-379.9399\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"123.3523,-383.0468 130.9344,-375.6466 120.3924,-376.7033 123.3523,-383.0468\"/>\n",
       "<text text-anchor=\"middle\" x=\"94\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z2\\}&#45;&gt;\\{z3\\} -->\n",
       "<g id=\"edge30\" class=\"edge\">\n",
       "<title>\\{z2\\}&#45;&gt;\\{z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M84.2697,-434.9735C97.8615,-422.2586 116.2459,-405.0603 131.2563,-391.0183\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"133.8433,-393.3909 138.755,-384.0034 129.0612,-388.279 133.8433,-393.3909\"/>\n",
       "<text text-anchor=\"middle\" x=\"122\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z2,z3\\} -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>\\{z0,z1,z2,z3\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"311.5,-36 218.5,-36 218.5,0 311.5,0 311.5,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"265\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1,z2,z3}</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z2,z3\\}&#45;&gt;\\{z0,z2,z3\\} -->\n",
       "<g id=\"edge31\" class=\"edge\">\n",
       "<title>\\{z0,z1,z2,z3\\}&#45;&gt;\\{z0,z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M268.2311,-36.3327C276.1454,-81.2381 296.5441,-196.9783 306.0223,-250.7568\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"302.5827,-251.4063 307.7654,-260.647 309.4765,-250.1912 302.5827,-251.4063\"/>\n",
       "<text text-anchor=\"middle\" x=\"294\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z2,z3\\}&#45;&gt;\\{z0,z1,z2,z3\\} -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>\\{z0,z1,z2,z3\\}&#45;&gt;\\{z0,z1,z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M311.6737,-21.8315C321.988,-21.4715 329.5,-20.1943 329.5,-18 329.5,-16.6285 326.5656,-15.6153 321.8467,-14.9604\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"321.9152,-11.4553 311.6737,-14.1685 321.3718,-18.4341 321.9152,-11.4553\"/>\n",
       "<text text-anchor=\"middle\" x=\"340\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z2,z3\\}&#45;&gt;\\{z0,z1,z2,z3\\} -->\n",
       "<g id=\"edge15\" class=\"edge\">\n",
       "<title>\\{z0,z1,z2,z3\\}&#45;&gt;\\{z0,z1,z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M311.6325,-25.7669C332.4024,-26.4542 350.5,-23.8652 350.5,-18 350.5,-13.1429 338.0889,-10.5326 322.0269,-10.1691\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"321.6107,-6.6715 311.6325,-10.2331 321.6539,-13.6714 321.6107,-6.6715\"/>\n",
       "<text text-anchor=\"middle\" x=\"354.5\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z1,z2\\} -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>\\{z1,z2\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"267,-558 207,-558 207,-522 267,-522 267,-558\"/>\n",
       "<text text-anchor=\"middle\" x=\"237\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1,z2}</text>\n",
       "</g>\n",
       "<!-- \\{z1,z2\\}&#45;&gt;\\{z2,z3\\} -->\n",
       "<g id=\"edge17\" class=\"edge\">\n",
       "<title>\\{z1,z2\\}&#45;&gt;\\{z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M212.1632,-521.6958C206.9289,-516.5786 202.0676,-510.5913 199,-504 195.7581,-497.0343 194.3667,-488.9431 193.9447,-481.2858\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"197.4445,-481.239 193.8872,-471.2593 190.4447,-481.2792 197.4445,-481.239\"/>\n",
       "<text text-anchor=\"middle\" x=\"203\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z1,z2\\}&#45;&gt;\\{z2,z3\\} -->\n",
       "<g id=\"edge33\" class=\"edge\">\n",
       "<title>\\{z1,z2\\}&#45;&gt;\\{z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M228.5048,-521.9735C222.8425,-509.9585 215.2936,-493.9401 208.8959,-480.3646\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"211.9134,-478.5571 204.4843,-471.0034 205.5813,-481.5413 211.9134,-478.5571\"/>\n",
       "<text text-anchor=\"middle\" x=\"223\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z1,z2\\}&#45;&gt;\\{z1,z2\\} -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>\\{z1,z2\\}&#45;&gt;\\{z1,z2\\}</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M267.4673,-547.8731C277.248,-547.7923 285,-545.168 285,-540 285,-536.8508 282.1214,-534.6461 277.6593,-533.3859\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"277.8209,-529.8794 267.4673,-532.1269 276.9627,-536.8266 277.8209,-529.8794\"/>\n",
       "<text text-anchor=\"middle\" x=\"295.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z2\\} -->\n",
       "<g id=\"node7\" class=\"node\">\n",
       "<title>\\{z0,z1,z2\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"349.5,-384 272.5,-384 272.5,-348 349.5,-348 349.5,-384\"/>\n",
       "<text text-anchor=\"middle\" x=\"311\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1,z2}</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z2\\}&#45;&gt;\\{z0,z2,z3\\} -->\n",
       "<g id=\"edge35\" class=\"edge\">\n",
       "<title>\\{z0,z1,z2\\}&#45;&gt;\\{z0,z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M311,-347.9735C311,-336.1918 311,-320.5607 311,-307.1581\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"314.5001,-307.0033 311,-297.0034 307.5001,-307.0034 314.5001,-307.0033\"/>\n",
       "<text text-anchor=\"middle\" x=\"315\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z2\\}&#45;&gt;\\{z0,z1,z2,z3\\} -->\n",
       "<g id=\"edge19\" class=\"edge\">\n",
       "<title>\\{z0,z1,z2\\}&#45;&gt;\\{z0,z1,z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M276.834,-347.9744C253.5781,-332.9816 227,-309.2335 227,-279 227,-279 227,-279 227,-105 227,-83.4445 236.9173,-61.2074 246.6192,-44.6107\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"249.6526,-46.3596 251.9226,-36.0108 243.6945,-42.6853 249.6526,-46.3596\"/>\n",
       "<text text-anchor=\"middle\" x=\"231\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z2\\}&#45;&gt;\\{z0,z1,z2\\} -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>\\{z0,z1,z2\\}&#45;&gt;\\{z0,z1,z2\\}</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M349.5552,-373.8058C359.7662,-373.3597 367.5,-370.7578 367.5,-366 367.5,-363.0264 364.479,-360.8949 359.7203,-359.6055\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"359.9415,-356.1027 349.5552,-358.1942 358.9788,-363.0362 359.9415,-356.1027\"/>\n",
       "<text text-anchor=\"middle\" x=\"378\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
       "</g>\n",
       "<!-- \\{z0,z2\\} -->\n",
       "<g id=\"node8\" class=\"node\">\n",
       "<title>\\{z0,z2\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"467,-297 407,-297 407,-261 467,-261 467,-297\"/>\n",
       "<text text-anchor=\"middle\" x=\"437\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z2}</text>\n",
       "</g>\n",
       "<!-- \\{z0,z2\\}&#45;&gt;\\{z0,z2\\} -->\n",
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>\\{z0,z2\\}&#45;&gt;\\{z0,z2\\}</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M467.4673,-286.8731C477.248,-286.7923 485,-284.168 485,-279 485,-275.8508 482.1214,-273.6461 477.6593,-272.3859\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"477.8209,-268.8794 467.4673,-271.1269 476.9627,-275.8266 477.8209,-268.8794\"/>\n",
       "<text text-anchor=\"middle\" x=\"495.5\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">end</text>\n",
       "</g>\n",
       "<!-- \\{z0,z2\\}&#45;&gt;\\{z0,z1,z3\\} -->\n",
       "<g id=\"edge22\" class=\"edge\">\n",
       "<title>\\{z0,z2\\}&#45;&gt;\\{z0,z1,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M428.3795,-260.7078C413.9466,-230.0818 384.8161,-168.2682 367.9228,-132.4216\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"370.934,-130.6009 363.505,-123.0471 364.6019,-133.585 370.934,-130.6009\"/>\n",
       "<text text-anchor=\"middle\" x=\"408\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z0,z2\\}&#45;&gt;\\{z0,z3\\} -->\n",
       "<g id=\"edge38\" class=\"edge\">\n",
       "<title>\\{z0,z2\\}&#45;&gt;\\{z0,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M441.144,-260.9735C443.8793,-249.0751 447.5171,-233.2508 450.6182,-219.7606\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"454.0318,-220.5333 452.8613,-210.0034 447.2098,-218.965 454.0318,-220.5333\"/>\n",
       "<text text-anchor=\"middle\" x=\"452\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z0\\} -->\n",
       "<g id=\"node9\" class=\"node\">\n",
       "<title>\\{z0\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"461,-558 407,-558 407,-522 461,-522 461,-558\"/>\n",
       "<text text-anchor=\"middle\" x=\"434\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0}</text>\n",
       "</g>\n",
       "<!-- \\{z0\\}&#45;&gt;\\{z0\\} -->\n",
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>\\{z0\\}&#45;&gt;\\{z0\\}</title>\n",
       "<path fill=\"none\" stroke=\"#a0522d\" d=\"M461.2408,-543.9337C471.0239,-544.0182 479,-542.707 479,-540 479,-538.3504 476.0382,-537.2191 471.5105,-536.6062\"/>\n",
       "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"471.4107,-533.0962 461.2408,-536.0663 471.0432,-540.0865 471.4107,-533.0962\"/>\n",
       "<text text-anchor=\"middle\" x=\"491.5\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">start</text>\n",
       "</g>\n",
       "<!-- \\{z0\\}&#45;&gt;\\{z0\\} -->\n",
       "<g id=\"edge40\" class=\"edge\">\n",
       "<title>\\{z0\\}&#45;&gt;\\{z0\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M461.36,-546.9863C482.1371,-549.3424 504,-547.0137 504,-540 504,-534.137 488.7224,-531.5478 471.5725,-532.2324\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"471.0638,-528.761 461.36,-533.0137 471.5979,-535.7406 471.0638,-528.761\"/>\n",
       "<text text-anchor=\"middle\" x=\"508\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1\\} -->\n",
       "<g id=\"node15\" class=\"node\">\n",
       "<title>\\{z0,z1\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"464,-471 404,-471 404,-435 464,-435 464,-471\"/>\n",
       "<text text-anchor=\"middle\" x=\"434\" y=\"-449.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z0,z1}</text>\n",
       "</g>\n",
       "<!-- \\{z0\\}&#45;&gt;\\{z0,z1\\} -->\n",
       "<g id=\"edge24\" class=\"edge\">\n",
       "<title>\\{z0\\}&#45;&gt;\\{z0,z1\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M434,-521.9735C434,-510.1918 434,-494.5607 434,-481.1581\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"437.5001,-481.0033 434,-471.0034 430.5001,-481.0034 437.5001,-481.0033\"/>\n",
       "<text text-anchor=\"middle\" x=\"438\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z3\\}&#45;&gt;\\{z3\\} -->\n",
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>\\{z3\\}&#45;&gt;\\{z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M185.2408,-369.9337C195.0239,-370.0182 203,-368.707 203,-366 203,-364.3504 200.0382,-363.2191 195.5105,-362.6062\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"195.4107,-359.0962 185.2408,-362.0663 195.0432,-366.0865 195.4107,-359.0962\"/>\n",
       "<text text-anchor=\"middle\" x=\"207\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z3\\}&#45;&gt;\\{z3\\} -->\n",
       "<g id=\"edge26\" class=\"edge\">\n",
       "<title>\\{z3\\}&#45;&gt;\\{z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M185.1975,-373.1809C203.3402,-375.2022 221,-372.8086 221,-366 221,-360.468 209.3418,-357.8506 195.2386,-358.1477\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"194.9417,-354.6597 185.1975,-358.8191 195.4088,-361.6441 194.9417,-354.6597\"/>\n",
       "<text text-anchor=\"middle\" x=\"225\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z3\\}&#45;&gt;\\{z0,z2,z3\\} -->\n",
       "<g id=\"edge34\" class=\"edge\">\n",
       "<title>\\{z0,z1,z3\\}&#45;&gt;\\{z0,z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M353.1903,-123.2704C350.1723,-150.0824 343.0098,-201.4126 329,-243 328.0589,-245.7937 326.9391,-248.6443 325.7251,-251.4571\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"322.4489,-250.1992 321.3575,-260.7377 328.7826,-253.18 322.4489,-250.1992\"/>\n",
       "<text text-anchor=\"middle\" x=\"350\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1,z3\\}&#45;&gt;\\{z0,z1,z2,z3\\} -->\n",
       "<g id=\"edge18\" class=\"edge\">\n",
       "<title>\\{z0,z1,z3\\}&#45;&gt;\\{z0,z1,z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M336.3519,-86.9735C323.1985,-74.2586 305.4072,-57.0603 290.881,-43.0183\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"293.2467,-40.4371 283.6242,-36.0034 288.3815,-45.4701 293.2467,-40.4371\"/>\n",
       "<text text-anchor=\"middle\" x=\"320\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z1,z3\\} -->\n",
       "<g id=\"node12\" class=\"node\">\n",
       "<title>\\{z1,z3\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"384,-558 324,-558 324,-522 384,-522 384,-558\"/>\n",
       "<text text-anchor=\"middle\" x=\"354\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1,z3}</text>\n",
       "</g>\n",
       "<!-- \\{z1,z3\\}&#45;&gt;\\{z2,z3\\} -->\n",
       "<g id=\"edge16\" class=\"edge\">\n",
       "<title>\\{z1,z3\\}&#45;&gt;\\{z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M323.9095,-523.4312C298.7311,-509.5671 262.6249,-489.6859 235.1903,-474.5795\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"236.6952,-471.4126 226.2471,-469.6551 233.3187,-477.5445 236.6952,-471.4126\"/>\n",
       "<text text-anchor=\"middle\" x=\"289\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z1,z3\\}&#45;&gt;\\{z2,z3\\} -->\n",
       "<g id=\"edge32\" class=\"edge\">\n",
       "<title>\\{z1,z3\\}&#45;&gt;\\{z2,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M337.4415,-521.9971C326.7521,-511.2333 312.0684,-497.9537 297,-489 278.0574,-477.7442 255.0393,-469.2008 235.7642,-463.2678\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"236.649,-459.8798 226.0671,-460.4027 234.6655,-466.5929 236.649,-459.8798\"/>\n",
       "<text text-anchor=\"middle\" x=\"322\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z1\\} -->\n",
       "<g id=\"node13\" class=\"node\">\n",
       "<title>\\{z1\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"54,-558 0,-558 0,-522 54,-522 54,-558\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{z1}</text>\n",
       "</g>\n",
       "<!-- \\{z1\\}&#45;&gt;\\{z2\\} -->\n",
       "<g id=\"edge20\" class=\"edge\">\n",
       "<title>\\{z1\\}&#45;&gt;\\{z2\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M27.0007,-521.8438C27.6026,-511.7804 29.3707,-499.2653 34,-489 35.4686,-485.7435 37.3276,-482.5584 39.4029,-479.5137\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"42.3516,-481.4212 45.6797,-471.3626 36.8054,-477.1503 42.3516,-481.4212\"/>\n",
       "<text text-anchor=\"middle\" x=\"38\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z1\\}&#45;&gt;\\{z2\\} -->\n",
       "<g id=\"edge36\" class=\"edge\">\n",
       "<title>\\{z1\\}&#45;&gt;\\{z2\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M34.8736,-521.9735C40.1216,-509.9585 47.1181,-493.9401 53.0477,-480.3646\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"56.3411,-481.5683 57.1365,-471.0034 49.9263,-478.7664 56.3411,-481.5683\"/>\n",
       "<text text-anchor=\"middle\" x=\"53\" y=\"-492.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z0,z3\\}&#45;&gt;\\{z0,z1,z3\\} -->\n",
       "<g id=\"edge21\" class=\"edge\">\n",
       "<title>\\{z0,z3\\}&#45;&gt;\\{z0,z1,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M444.3424,-173.6871C436.6232,-163.3329 426.1232,-150.5829 415,-141 409.8677,-136.5784 404.1243,-132.3749 398.2795,-128.5043\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"400.0264,-125.468 389.7031,-123.0849 396.2871,-131.3856 400.0264,-125.468\"/>\n",
       "<text text-anchor=\"middle\" x=\"433\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z0,z3\\}&#45;&gt;\\{z0,z3\\} -->\n",
       "<g id=\"edge37\" class=\"edge\">\n",
       "<title>\\{z0,z3\\}&#45;&gt;\\{z0,z3\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M487.4673,-199.8731C497.248,-199.7923 505,-197.168 505,-192 505,-188.8508 502.1214,-186.6461 497.6593,-185.3859\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"497.8209,-181.8794 487.4673,-184.1269 496.9627,-188.8266 497.8209,-181.8794\"/>\n",
       "<text text-anchor=\"middle\" x=\"509\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1\\}&#45;&gt;\\{z0,z1,z2\\} -->\n",
       "<g id=\"edge23\" class=\"edge\">\n",
       "<title>\\{z0,z1\\}&#45;&gt;\\{z0,z1,z2\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M408.5143,-434.9735C390.0432,-421.9086 364.8799,-404.1102 344.7418,-389.8662\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"346.6383,-386.9206 336.453,-384.0034 342.5961,-392.6355 346.6383,-386.9206\"/>\n",
       "<text text-anchor=\"middle\" x=\"383\" y=\"-405.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{z0,z1\\}&#45;&gt;\\{z0,z2\\} -->\n",
       "<g id=\"edge39\" class=\"edge\">\n",
       "<title>\\{z0,z1\\}&#45;&gt;\\{z0,z2\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M434.3154,-434.7078C434.8389,-404.3436 435.891,-343.3226 436.5113,-307.3464\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"440.0158,-307.106 436.6888,-297.0471 433.0169,-306.9852 440.0158,-307.106\"/>\n",
       "<text text-anchor=\"middle\" x=\"439\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "<!-- \\{\\} -->\n",
       "<g id=\"node16\" class=\"node\">\n",
       "<title>\\{\\}</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"602,-558 548,-558 548,-522 602,-522 602,-558\"/>\n",
       "<text text-anchor=\"middle\" x=\"575\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{}</text>\n",
       "</g>\n",
       "<!-- \\{\\}&#45;&gt;\\{\\} -->\n",
       "<g id=\"edge25\" class=\"edge\">\n",
       "<title>\\{\\}&#45;&gt;\\{\\}</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M602.2408,-543.9337C612.0239,-544.0182 620,-542.707 620,-540 620,-538.3504 617.0382,-537.2191 612.5105,-536.6062\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"612.4107,-533.0962 602.2408,-536.0663 612.0432,-540.0865 612.4107,-533.0962\"/>\n",
       "<text text-anchor=\"middle\" x=\"624\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- \\{\\}&#45;&gt;\\{\\} -->\n",
       "<g id=\"edge41\" class=\"edge\">\n",
       "<title>\\{\\}&#45;&gt;\\{\\}</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M602.1975,-547.1809C620.3402,-549.2022 638,-546.8086 638,-540 638,-534.468 626.3418,-531.8506 612.2386,-532.1477\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"611.9417,-528.6597 602.1975,-532.8191 612.4088,-535.6441 611.9417,-528.6597\"/>\n",
       "<text text-anchor=\"middle\" x=\"642\" y=\"-536.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">0</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<Dot visualization: expr_as_graph [(\"0\",{x,y|x:POW(Z) & δs(x, [0])=y})]>"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":dot expr_as_graph (\"0\",{x,y| x∈ℙ(Z) & δs(x,[0]) = y},\n",
    "                    \"1\",{x,y| x∈ℙ(Z) & δs(x,[1]) = y},\n",
    "                    \"start\", {x,y|x=y & x={z0}},\n",
    "                    \"end\", {x,y|x=y & x∩F ≠ ∅})"
   ]
  },
  {
   "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
}