diff --git a/notebooks/models/NFA_to_DFA.ipynb b/notebooks/models/NFA_to_DFA.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..63bcc66fe48a5883b20a2e185b1139907201c3a1
--- /dev/null
+++ b/notebooks/models/NFA_to_DFA.ipynb
@@ -0,0 +1,1019 @@
+{
+ "cells": [
+ {
+ "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 $\\hat$ in Bezeichnern verwenden.\n",
+ "Deshalb wird aus\n",
+ "* $\\Sigma^*$ wird ```seq(Σ)```\n",
+ "* $\\widehat{\\delta}$ wird ```δs```"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NFA_nach_DFA"
+ ]
+ },
+ "execution_count": 3,
+ "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": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 5,
+ "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": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{z0},\\mathit{z1}\\}$"
+ ],
+ "text/plain": [
+ "{z0,z1}"
+ ]
+ },
+ "execution_count": 6,
+ "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": 7,
+ "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": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table δ"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Alternatively, we can view it as graph:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "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.28.0 (20110509.1545)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"144pt\" height=\"368pt\"\n",
+ " viewBox=\"0.00 0.00 144.00 368.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 364)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-364 141,-364 141,5 -4,5\"/>\n",
+ "<g id=\"graph2\" class=\"cluster\"><title>cluster_Z</title>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-352 128,-352 128,-8 8,-8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"68\" y=\"-337.2\" font-family=\"Times,serif\" font-size=\"12.00\">Z</text>\n",
+ "</g>\n",
+ "<!-- z0 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>z0</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-322 16,-322 16,-286 70,-286 70,-322\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-299.8\" font-family=\"Times,serif\" font-size=\"14.00\">z0</text>\n",
+ "</g>\n",
+ "<!-- z0->z0 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>z0->z0</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.2408,-308.121C80.0239,-308.21 88,-306.836 88,-304 88,-302.272 85.0382,-301.087 80.5105,-300.445\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.4181,-296.934 70.2408,-299.879 80.0332,-303.924 80.4181,-296.934\"/>\n",
+ "<text text-anchor=\"middle\" x=\"91.5\" y=\"-299.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- z0->z0 -->\n",
+ "<g id=\"edge12\" class=\"edge\"><title>z0->z0</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M70.1975,-319.251C88.3402,-323.544 106,-318.46 106,-304 106,-292.251 94.3418,-286.692 80.2386,-287.323\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"79.6061,-283.878 70.1975,-288.749 80.5903,-290.808 79.6061,-283.878\"/>\n",
+ "<text text-anchor=\"middle\" x=\"109.5\" y=\"-299.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- z1 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>z1</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-232 16,-232 16,-196 70,-196 70,-232\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-209.8\" font-family=\"Times,serif\" font-size=\"14.00\">z1</text>\n",
+ "</g>\n",
+ "<!-- z0->z1 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>z0->z1</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M43,-285.614C43,-273.24 43,-256.369 43,-242.22\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46.5001,-242.05 43,-232.05 39.5001,-242.05 46.5001,-242.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46.5\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- z2 -->\n",
+ "<g id=\"node7\" class=\"node\"><title>z2</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-142 16,-142 16,-106 70,-106 70,-142\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-119.8\" font-family=\"Times,serif\" font-size=\"14.00\">z2</text>\n",
+ "</g>\n",
+ "<!-- z1->z2 -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>z1->z2</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-195.614C43,-183.24 43,-166.369 43,-152.22\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5001,-152.05 43,-142.05 39.5001,-152.05 46.5001,-152.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46.5\" y=\"-164.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- z3 -->\n",
+ "<g id=\"node5\" class=\"node\"><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=\"-29.8\" font-family=\"Times,serif\" font-size=\"14.00\">z3</text>\n",
+ "</g>\n",
+ "<!-- z3->z3 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>z3->z3</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M70.2408,-42.2419C80.0239,-42.4192 88,-39.6719 88,-34 88,-30.5437 85.0382,-28.1734 80.5105,-26.8891\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"80.5639,-23.3739 70.2408,-25.7581 79.7975,-30.3318 80.5639,-23.3739\"/>\n",
+ "<text text-anchor=\"middle\" x=\"91.5\" y=\"-29.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- z2->z3 -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>z2->z3</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M43,-105.614C43,-93.2403 43,-76.3686 43,-62.2198\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"46.5001,-62.0504 43,-52.0504 39.5001,-62.0504 46.5001,-62.0504\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46.5\" y=\"-74.8\" font-family=\"Times,serif\" font-size=\"14.00\">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": 8,
+ "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": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$"
+ ],
+ "text/plain": [
+ "{z0,z1,z2,z3}"
+ ]
+ },
+ "execution_count": 9,
+ "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": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{z2}\\}$"
+ ],
+ "text/plain": [
+ "{z2}"
+ ]
+ },
+ "execution_count": 10,
+ "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": 11,
+ "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": 11,
+ "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": 12,
+ "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": 12,
+ "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": 13,
+ "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": 13,
+ "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": 14,
+ "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": 14,
+ "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": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref DOT_DECOMPOSE_NODES=FALSE"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "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.28.0 (20110509.1545)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"648pt\" height=\"584pt\"\n",
+ " viewBox=\"0.00 0.00 648.00 584.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 580)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-580 645,-580 645,5 -4,5\"/>\n",
+ "<!-- \\{z2,z3\\} -->\n",
+ "<g id=\"node1\" class=\"node\"><title>\\{z2,z3\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"230.524,-486 171.476,-486 171.476,-450 230.524,-450 230.524,-486\"/>\n",
+ "<text text-anchor=\"middle\" x=\"201\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z2,z3}</text>\n",
+ "</g>\n",
+ "<!-- \\{z2,z3\\}->\\{z2,z3\\} -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>\\{z2,z3\\}->\\{z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M230.375,-476.25C240.167,-476.25 248,-473.5 248,-468 248,-464.648 245.091,-462.318 240.603,-461.009\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"240.728,-457.498 230.375,-459.75 239.873,-464.445 240.728,-457.498\"/>\n",
+ "<text text-anchor=\"middle\" x=\"258.107\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
+ "</g>\n",
+ "<!-- \\{z3\\} -->\n",
+ "<g id=\"node19\" class=\"node\"><title>\\{z3\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"147,-396 93,-396 93,-360 147,-360 147,-396\"/>\n",
+ "<text text-anchor=\"middle\" x=\"120\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z3}</text>\n",
+ "</g>\n",
+ "<!-- \\{z2,z3\\}->\\{z3\\} -->\n",
+ "<g id=\"edge22\" class=\"edge\"><title>\\{z2,z3\\}->\\{z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M171.56,-453.384C161.851,-447.811 151.604,-440.623 144,-432 137.328,-424.433 132.209,-414.704 128.447,-405.651\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"131.695,-404.345 124.887,-396.227 125.146,-406.819 131.695,-404.345\"/>\n",
+ "<text text-anchor=\"middle\" x=\"147.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z2,z3\\}->\\{z3\\} -->\n",
+ "<g id=\"edge54\" class=\"edge\"><title>\\{z2,z3\\}->\\{z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M184.997,-449.614C172.938,-436.512 156.237,-418.368 142.784,-403.753\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"145.042,-401.038 135.694,-396.05 139.891,-405.778 145.042,-401.038\"/>\n",
+ "<text text-anchor=\"middle\" x=\"171.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z2,z3\\} -->\n",
+ "<g id=\"node3\" class=\"node\"><title>\\{z1,z2,z3\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"148.061,-576 71.9392,-576 71.9392,-540 148.061,-540 148.061,-576\"/>\n",
+ "<text text-anchor=\"middle\" x=\"110\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z2,z3}</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z2,z3\\}->\\{z2,z3\\} -->\n",
+ "<g id=\"edge24\" class=\"edge\"><title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M112.276,-539.994C114.566,-528.65 119.102,-514.033 128,-504 137.141,-493.694 149.984,-486.149 162.353,-480.761\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"163.66,-484.008 171.651,-477.052 161.066,-477.507 163.66,-484.008\"/>\n",
+ "<text text-anchor=\"middle\" x=\"131.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z2,z3\\}->\\{z2,z3\\} -->\n",
+ "<g id=\"edge56\" class=\"edge\"><title>\\{z1,z2,z3\\}->\\{z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M127.979,-539.614C141.652,-526.391 160.638,-508.032 175.822,-493.348\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"178.613,-495.518 183.368,-486.05 173.747,-490.486 178.613,-495.518\"/>\n",
+ "<text text-anchor=\"middle\" x=\"167.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z2,z3\\}->\\{z1,z2,z3\\} -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>\\{z1,z2,z3\\}->\\{z1,z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M148.214,-566.177C158.335,-565.71 166,-562.984 166,-558 166,-554.885 163.006,-552.652 158.289,-551.301\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"158.616,-547.812 148.214,-549.823 157.6,-554.737 158.616,-547.812\"/>\n",
+ "<text text-anchor=\"middle\" x=\"176.107\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z2,z3\\} -->\n",
+ "<g id=\"node5\" class=\"node\"><title>\\{z0,z2,z3\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"403.061,-306 326.939,-306 326.939,-270 403.061,-270 403.061,-306\"/>\n",
+ "<text text-anchor=\"middle\" x=\"365\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z2,z3}</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z2,z3\\}->\\{z0,z2,z3\\} -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>\\{z0,z2,z3\\}->\\{z0,z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M403.214,-296.177C413.335,-295.71 421,-292.984 421,-288 421,-284.885 418.006,-282.652 413.289,-281.301\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"413.616,-277.812 403.214,-279.823 412.6,-284.737 413.616,-277.812\"/>\n",
+ "<text text-anchor=\"middle\" x=\"431.107\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z3\\} -->\n",
+ "<g id=\"node24\" class=\"node\"><title>\\{z0,z1,z3\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"446.061,-126 369.939,-126 369.939,-90 446.061,-90 446.061,-126\"/>\n",
+ "<text text-anchor=\"middle\" x=\"408\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1,z3}</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z2,z3\\}->\\{z0,z1,z3\\} -->\n",
+ "<g id=\"edge26\" class=\"edge\"><title>\\{z0,z2,z3\\}->\\{z0,z1,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M365.892,-269.687C367.306,-248.306 370.797,-210.968 379,-180 383.021,-164.82 389.492,-148.558 395.302,-135.432\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"398.604,-136.628 399.565,-126.076 392.234,-133.725 398.604,-136.628\"/>\n",
+ "<text text-anchor=\"middle\" x=\"382.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z3\\} -->\n",
+ "<g id=\"node34\" class=\"node\"><title>\\{z0,z3\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"536.524,-216 477.476,-216 477.476,-180 536.524,-180 536.524,-216\"/>\n",
+ "<text text-anchor=\"middle\" x=\"507\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z3}</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z2,z3\\}->\\{z0,z3\\} -->\n",
+ "<g id=\"edge58\" class=\"edge\"><title>\\{z0,z2,z3\\}->\\{z0,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M392.716,-269.824C415,-256.014 446.483,-236.503 470.764,-221.456\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"472.697,-224.376 479.354,-216.133 469.01,-218.426 472.697,-224.376\"/>\n",
+ "<text text-anchor=\"middle\" x=\"452.5\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z2\\} -->\n",
+ "<g id=\"node7\" class=\"node\"><title>\\{z2\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"84,-486 30,-486 30,-450 84,-450 84,-486\"/>\n",
+ "<text text-anchor=\"middle\" x=\"57\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z2}</text>\n",
+ "</g>\n",
+ "<!-- \\{z2\\}->\\{z2\\} -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>\\{z2\\}->\\{z2\\}</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M84.2408,-476.242C94.0239,-476.419 102,-473.672 102,-468 102,-464.544 99.0382,-462.173 94.5105,-460.889\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"94.5639,-457.374 84.2408,-459.758 93.7975,-464.332 94.5639,-457.374\"/>\n",
+ "<text text-anchor=\"middle\" x=\"112.107\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
+ "</g>\n",
+ "<!-- \\{z2\\}->\\{z3\\} -->\n",
+ "<g id=\"edge28\" class=\"edge\"><title>\\{z2\\}->\\{z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M60.6361,-449.617C63.525,-438.671 68.3732,-424.649 76,-414 78.8347,-410.042 82.2349,-406.298 85.8727,-402.835\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"88.3202,-405.344 93.5685,-396.141 83.7263,-400.063 88.3202,-405.344\"/>\n",
+ "<text text-anchor=\"middle\" x=\"79.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z2\\}->\\{z3\\} -->\n",
+ "<g id=\"edge60\" class=\"edge\"><title>\\{z2\\}->\\{z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M69.7965,-449.984C74.0351,-444.293 78.753,-437.897 83,-432 89.3945,-423.122 96.2851,-413.319 102.367,-404.583\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"105.305,-406.487 108.13,-396.276 99.5535,-402.497 105.305,-406.487\"/>\n",
+ "<text text-anchor=\"middle\" x=\"99.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z2,z3\\} -->\n",
+ "<g id=\"node9\" class=\"node\"><title>\\{z0,z1,z2,z3\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"365.097,-36 272.903,-36 272.903,-0 365.097,-0 365.097,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"319\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1,z2,z3}</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z2,z3\\}->\\{z0,z2,z3\\} -->\n",
+ "<g id=\"edge62\" class=\"edge\"><title>\\{z0,z1,z2,z3\\}->\\{z0,z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M321.923,-36.0293C329.684,-81.2458 350.861,-204.624 360.324,-259.755\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"356.911,-260.564 362.053,-269.828 363.81,-259.38 356.911,-260.564\"/>\n",
+ "<text text-anchor=\"middle\" x=\"347.5\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\} -->\n",
+ "<g id=\"edge30\" class=\"edge\"><title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M365.462,-34.5249C385.713,-35.8778 403.215,-30.3695 403.215,-18 403.215,-7.75648 391.212,-2.21833 375.585,-1.38554\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"375.43,2.11332 365.462,-1.47508 375.492,-4.88641 375.43,2.11332\"/>\n",
+ "<text text-anchor=\"middle\" x=\"406.715\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\} -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>\\{z0,z1,z2,z3\\}->\\{z0,z1,z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M365.312,-22.014C375.546,-21.6368 383,-20.2988 383,-18 383,-16.5632 380.088,-15.5018 375.406,-14.8157\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"375.565,-11.317 365.312,-13.986 374.992,-18.2935 375.565,-11.317\"/>\n",
+ "<text text-anchor=\"middle\" x=\"393.107\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z2\\} -->\n",
+ "<g id=\"node11\" class=\"node\"><title>\\{z1,z2\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"263.524,-576 204.476,-576 204.476,-540 263.524,-540 263.524,-576\"/>\n",
+ "<text text-anchor=\"middle\" x=\"234\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z2}</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z2\\}->\\{z2,z3\\} -->\n",
+ "<g id=\"edge34\" class=\"edge\"><title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M216.969,-539.766C212.679,-534.468 208.568,-528.348 206,-522 202.783,-514.048 201.242,-504.896 200.584,-496.458\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"204.074,-496.145 200.163,-486.298 197.08,-496.434 204.074,-496.145\"/>\n",
+ "<text text-anchor=\"middle\" x=\"209.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z2\\}->\\{z2,z3\\} -->\n",
+ "<g id=\"edge66\" class=\"edge\"><title>\\{z1,z2\\}->\\{z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M227.48,-539.614C222.795,-527.119 216.389,-510.037 211.052,-495.804\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"214.182,-494.185 207.394,-486.05 207.628,-496.643 214.182,-494.185\"/>\n",
+ "<text text-anchor=\"middle\" x=\"224.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z2\\}->\\{z1,z2\\} -->\n",
+ "<g id=\"edge12\" class=\"edge\"><title>\\{z1,z2\\}->\\{z1,z2\\}</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M263.375,-566.25C273.167,-566.25 281,-563.5 281,-558 281,-554.648 278.091,-552.318 273.603,-551.009\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"273.728,-547.498 263.375,-549.75 272.873,-554.445 273.728,-547.498\"/>\n",
+ "<text text-anchor=\"middle\" x=\"291.107\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z2\\} -->\n",
+ "<g id=\"node13\" class=\"node\"><title>\\{z0,z1,z2\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"403.061,-396 326.939,-396 326.939,-360 403.061,-360 403.061,-396\"/>\n",
+ "<text text-anchor=\"middle\" x=\"365\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1,z2}</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z2\\}->\\{z0,z2,z3\\} -->\n",
+ "<g id=\"edge70\" class=\"edge\"><title>\\{z0,z1,z2\\}->\\{z0,z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M365,-359.614C365,-347.24 365,-330.369 365,-316.22\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"368.5,-316.05 365,-306.05 361.5,-316.05 368.5,-316.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"368.5\" y=\"-328.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z2\\}->\\{z0,z1,z2,z3\\} -->\n",
+ "<g id=\"edge38\" class=\"edge\"><title>\\{z0,z1,z2\\}->\\{z0,z1,z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M332.764,-359.919C309.075,-344.787 281,-320.259 281,-289 281,-289 281,-289 281,-107 281,-84.815 291.305,-61.8717 301.182,-44.9761\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"304.29,-46.6044 306.557,-36.255 298.331,-42.9315 304.29,-46.6044\"/>\n",
+ "<text text-anchor=\"middle\" x=\"284.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z2\\}->\\{z0,z1,z2\\} -->\n",
+ "<g id=\"edge14\" class=\"edge\"><title>\\{z0,z1,z2\\}->\\{z0,z1,z2\\}</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M403.214,-386.177C413.335,-385.71 421,-382.984 421,-378 421,-374.885 418.006,-372.652 413.289,-371.301\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"413.616,-367.812 403.214,-369.823 412.6,-374.737 413.616,-367.812\"/>\n",
+ "<text text-anchor=\"middle\" x=\"431.107\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z2\\} -->\n",
+ "<g id=\"node15\" class=\"node\"><title>\\{z0,z2\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"518.524,-306 459.476,-306 459.476,-270 518.524,-270 518.524,-306\"/>\n",
+ "<text text-anchor=\"middle\" x=\"489\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z2}</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z2\\}->\\{z0,z2\\} -->\n",
+ "<g id=\"edge16\" class=\"edge\"><title>\\{z0,z2\\}->\\{z0,z2\\}</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M518.375,-296.25C528.167,-296.25 536,-293.5 536,-288 536,-284.648 533.091,-282.318 528.603,-281.009\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"528.728,-277.498 518.375,-279.75 527.873,-284.445 528.728,-277.498\"/>\n",
+ "<text text-anchor=\"middle\" x=\"546.107\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">end</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z2\\}->\\{z0,z1,z3\\} -->\n",
+ "<g id=\"edge44\" class=\"edge\"><title>\\{z0,z2\\}->\\{z0,z1,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M481.233,-269.933C467.021,-238.7 436.745,-172.169 419.913,-135.178\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"423.071,-133.668 415.743,-126.016 416.699,-136.567 423.071,-133.668\"/>\n",
+ "<text text-anchor=\"middle\" x=\"460.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z2\\}->\\{z0,z3\\} -->\n",
+ "<g id=\"edge76\" class=\"edge\"><title>\\{z0,z2\\}->\\{z0,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M492.556,-269.614C495.087,-257.24 498.538,-240.369 501.432,-226.22\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"504.937,-226.549 503.512,-216.05 498.079,-225.146 504.937,-226.549\"/>\n",
+ "<text text-anchor=\"middle\" x=\"502.5\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z0\\} -->\n",
+ "<g id=\"node17\" class=\"node\"><title>\\{z0\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"451,-576 397,-576 397,-540 451,-540 451,-576\"/>\n",
+ "<text text-anchor=\"middle\" x=\"424\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0}</text>\n",
+ "</g>\n",
+ "<!-- \\{z0\\}->\\{z0\\} -->\n",
+ "<g id=\"edge80\" class=\"edge\"><title>\\{z0\\}->\\{z0\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M451.128,-572.838C471.639,-577.842 493.101,-572.896 493.101,-558 493.101,-545.548 478.104,-540.049 461.201,-541.503\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"460.426,-538.083 451.128,-543.162 461.564,-544.99 460.426,-538.083\"/>\n",
+ "<text text-anchor=\"middle\" x=\"496.601\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z0\\}->\\{z0\\} -->\n",
+ "<g id=\"edge18\" class=\"edge\"><title>\\{z0\\}->\\{z0\\}</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M451.241,-562.121C461.024,-562.21 469,-560.836 469,-558 469,-556.272 466.038,-555.087 461.51,-554.445\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"461.418,-550.934 451.241,-553.879 461.033,-557.924 461.418,-550.934\"/>\n",
+ "<text text-anchor=\"middle\" x=\"481.05\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">start</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1\\} -->\n",
+ "<g id=\"node37\" class=\"node\"><title>\\{z0,z1\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"453.524,-486 394.476,-486 394.476,-450 453.524,-450 453.524,-486\"/>\n",
+ "<text text-anchor=\"middle\" x=\"424\" y=\"-463.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z0,z1}</text>\n",
+ "</g>\n",
+ "<!-- \\{z0\\}->\\{z0,z1\\} -->\n",
+ "<g id=\"edge48\" class=\"edge\"><title>\\{z0\\}->\\{z0,z1\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M424,-539.614C424,-527.24 424,-510.369 424,-496.22\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"427.5,-496.05 424,-486.05 420.5,-496.05 427.5,-496.05\"/>\n",
+ "<text text-anchor=\"middle\" x=\"427.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z3\\}->\\{z3\\} -->\n",
+ "<g id=\"edge52\" class=\"edge\"><title>\\{z3\\}->\\{z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M147.198,-393.251C165.34,-397.544 183,-392.46 183,-378 183,-366.251 171.342,-360.692 157.239,-361.323\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"156.606,-357.878 147.198,-362.749 157.59,-364.808 156.606,-357.878\"/>\n",
+ "<text text-anchor=\"middle\" x=\"186.5\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z3\\}->\\{z3\\} -->\n",
+ "<g id=\"edge20\" class=\"edge\"><title>\\{z3\\}->\\{z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M147.241,-382.121C157.024,-382.21 165,-380.836 165,-378 165,-376.272 162.038,-375.087 157.51,-374.445\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"157.418,-370.934 147.241,-373.879 157.033,-377.924 157.418,-370.934\"/>\n",
+ "<text text-anchor=\"middle\" x=\"168.5\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z3\\}->\\{z0,z2,z3\\} -->\n",
+ "<g id=\"edge68\" class=\"edge\"><title>\\{z0,z1,z3\\}->\\{z0,z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M406.684,-126.14C404.221,-153.399 397.765,-208.04 383,-252 382.062,-254.793 380.929,-257.639 379.693,-260.439\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"376.442,-259.123 375.232,-269.649 382.742,-262.175 376.442,-259.123\"/>\n",
+ "<text text-anchor=\"middle\" x=\"403.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1,z3\\}->\\{z0,z1,z2,z3\\} -->\n",
+ "<g id=\"edge36\" class=\"edge\"><title>\\{z0,z1,z3\\}->\\{z0,z1,z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M390.416,-89.614C377.043,-76.3912 358.475,-58.0317 343.624,-43.3476\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"345.816,-40.5926 336.244,-36.0504 340.894,-45.5703 345.816,-40.5926\"/>\n",
+ "<text text-anchor=\"middle\" x=\"375.5\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z3\\} -->\n",
+ "<g id=\"node27\" class=\"node\"><title>\\{z1,z3\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"378.524,-576 319.476,-576 319.476,-540 378.524,-540 378.524,-576\"/>\n",
+ "<text text-anchor=\"middle\" x=\"349\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z3}</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z3\\}->\\{z2,z3\\} -->\n",
+ "<g id=\"edge32\" class=\"edge\"><title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M320.113,-539.824C296.785,-525.953 263.786,-506.332 238.434,-491.258\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"240.199,-488.235 229.814,-486.133 236.621,-494.252 240.199,-488.235\"/>\n",
+ "<text text-anchor=\"middle\" x=\"292.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z1,z3\\}->\\{z2,z3\\} -->\n",
+ "<g id=\"edge64\" class=\"edge\"><title>\\{z1,z3\\}->\\{z2,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M336.572,-539.66C327.555,-528.167 314.444,-513.509 300,-504 281.93,-492.104 259.339,-483.716 240.302,-478.14\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"241,-474.702 230.429,-475.402 239.13,-481.447 241,-474.702\"/>\n",
+ "<text text-anchor=\"middle\" x=\"325.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z1\\} -->\n",
+ "<g id=\"node32\" class=\"node\"><title>\\{z1\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"54,-576 0,-576 0,-540 54,-540 54,-576\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{z1}</text>\n",
+ "</g>\n",
+ "<!-- \\{z1\\}->\\{z2\\} -->\n",
+ "<g id=\"edge40\" class=\"edge\"><title>\\{z1\\}->\\{z2\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M25.4389,-539.765C25.086,-529.134 25.7508,-515.399 30,-504 31.1794,-500.836 32.751,-497.726 34.5452,-494.744\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"37.6054,-496.473 40.4255,-486.26 31.8522,-492.485 37.6054,-496.473\"/>\n",
+ "<text text-anchor=\"middle\" x=\"33.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z1\\}->\\{z2\\} -->\n",
+ "<g id=\"edge72\" class=\"edge\"><title>\\{z1\\}->\\{z2\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M32.927,-539.614C37.1867,-527.119 43.01,-510.037 47.8621,-495.804\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"51.2733,-496.645 51.1874,-486.05 44.6478,-494.386 51.2733,-496.645\"/>\n",
+ "<text text-anchor=\"middle\" x=\"48.5\" y=\"-508.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z3\\}->\\{z0,z1,z3\\} -->\n",
+ "<g id=\"edge42\" class=\"edge\"><title>\\{z0,z3\\}->\\{z0,z1,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M496.207,-179.918C488.647,-168.823 477.814,-154.523 466,-144 460.985,-139.533 455.32,-135.317 449.547,-131.462\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"451.391,-128.487 441.072,-126.087 447.641,-134.399 451.391,-128.487\"/>\n",
+ "<text text-anchor=\"middle\" x=\"485.5\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z3\\}->\\{z0,z3\\} -->\n",
+ "<g id=\"edge74\" class=\"edge\"><title>\\{z0,z3\\}->\\{z0,z3\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M536.375,-206.25C546.167,-206.25 554,-203.5 554,-198 554,-194.648 551.091,-192.318 546.603,-191.009\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"546.728,-187.498 536.375,-189.75 545.873,-194.445 546.728,-187.498\"/>\n",
+ "<text text-anchor=\"middle\" x=\"557.5\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1\\}->\\{z0,z1,z2\\} -->\n",
+ "<g id=\"edge46\" class=\"edge\"><title>\\{z0,z1\\}->\\{z0,z1,z2\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M412.343,-449.614C403.722,-436.755 391.844,-419.038 382.142,-404.568\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"384.907,-402.407 376.432,-396.05 379.093,-406.305 384.907,-402.407\"/>\n",
+ "<text text-anchor=\"middle\" x=\"403.5\" y=\"-418.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{z0,z1\\}->\\{z0,z2\\} -->\n",
+ "<g id=\"edge78\" class=\"edge\"><title>\\{z0,z1\\}->\\{z0,z2\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M430.312,-449.786C435.582,-435.409 443.288,-414.371 450,-396 460.016,-368.585 471.449,-337.208 479.334,-315.554\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"482.661,-316.646 482.794,-306.052 476.084,-314.251 482.661,-316.646\"/>\n",
+ "<text text-anchor=\"middle\" x=\"466.5\" y=\"-373.8\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n",
+ "</g>\n",
+ "<!-- \\{\\} -->\n",
+ "<g id=\"node40\" class=\"node\"><title>\\{\\}</title>\n",
+ "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"590,-576 536,-576 536,-540 590,-540 590,-576\"/>\n",
+ "<text text-anchor=\"middle\" x=\"563\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">{}</text>\n",
+ "</g>\n",
+ "<!-- \\{\\}->\\{\\} -->\n",
+ "<g id=\"edge50\" class=\"edge\"><title>\\{\\}->\\{\\}</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M590.241,-562.121C600.024,-562.21 608,-560.836 608,-558 608,-556.272 605.038,-555.087 600.51,-554.445\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"600.418,-550.934 590.241,-553.879 600.033,-557.924 600.418,-550.934\"/>\n",
+ "<text text-anchor=\"middle\" x=\"611.5\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- \\{\\}->\\{\\} -->\n",
+ "<g id=\"edge82\" class=\"edge\"><title>\\{\\}->\\{\\}</title>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M590.198,-573.251C608.34,-577.544 626,-572.46 626,-558 626,-546.251 614.342,-540.692 600.239,-541.323\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"599.606,-537.878 590.198,-542.749 600.59,-544.808 599.606,-537.878\"/>\n",
+ "<text text-anchor=\"middle\" x=\"629.5\" y=\"-553.8\" font-family=\"Times,serif\" font-size=\"14.00\">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": 16,
+ "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
+}