diff --git a/notebooks/presentations/BadHonnef_2019.ipynb b/notebooks/presentations/BadHonnef_2019.ipynb
index 6fd39e38a4e84db324e960336c347b44f870b42d..605dc888af3e2088dbbad72aa1ad70d06bd82fd5 100644
--- a/notebooks/presentations/BadHonnef_2019.ipynb
+++ b/notebooks/presentations/BadHonnef_2019.ipynb
@@ -11,7 +11,9 @@
"# Ein Jupyter-Kernel für Logik und Mengentheorie\n",
"\n",
"### David Geleßus, Michael Leuschel\n",
- "### Bad Honnef, 2019"
+ "### Bad Honnef, 2019\n",
+ "\n",
+ ""
]
},
{
@@ -76,7 +78,7 @@
}
},
"source": [
- "## ProB\n",
+ "## ProB (https://www3.hhu.de/stups/prob)\n",
"\n",
"* Werkzeug zur Animation, Verifikation und Visualisierung formeller Spezifikationen\n",
"* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.\n",
@@ -86,6 +88,20 @@
" * Der ProB 2-Jupyter-Kernel unterstützt daher (fast) alle Sprachen, die ProB versteht"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Einsatz von ProB in der Industrie\n",
+ "* Datenvalidierung: Siemens (Paris Line 1, Barcelona, Alger, ...), Alstom (Amsterdam,...), Thales (Schweiz,...), RATP, SNCF, ...\n",
+ "* Zertifizierung als T2 Werkzeug nach EN50128\n",
+ "* Validierung von Systemmodellen: ClearSy (Octys, ...),...\n",
+ "* Ausführung formaler Modelle in Echtzeit\n",
+ " * SlotTool \n",
+ " * Hybrid Level 3 - ETCS (Thales, ProRail/Network Rail/DB), Video der Deutschen Bahn: https://www.youtube.com/watch?v=FjKnugbmrP4\n",
+ ""
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {
@@ -127,7 +143,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 1,
"metadata": {},
"outputs": [
{
@@ -139,7 +155,7 @@
"{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47}"
]
},
- "execution_count": 2,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
@@ -150,7 +166,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -162,7 +178,7 @@
"x > 1 ∧ x < 50 ∧ ¬(∃y·(y > 1 ∧ y < x ∧ x mod y = 0))"
]
},
- "execution_count": 4,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -173,14 +189,18 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"Eingabe als Unicode ist auch erlaubt:"
]
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 3,
"metadata": {},
"outputs": [
{
@@ -192,7 +212,7 @@
"{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47}"
]
},
- "execution_count": 7,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -203,14 +223,18 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"Mehrzeilige Eingabe ist möglich, es gibt Syntax-Highlighting und Code Completion."
]
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 4,
"metadata": {},
"outputs": [
{
@@ -242,7 +266,7 @@
"\tO = 0"
]
},
- "execution_count": 8,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -259,14 +283,18 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"Mithilfe der Mengentheorie kann man alle Lösungen finden, und mit dem ```:table``` Kommando als Tabelle ausgeben."
]
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 5,
"metadata": {},
"outputs": [
{
@@ -281,7 +309,7 @@
"9\t5\t6\t7\t1\t0\t8\t2\n"
]
},
- "execution_count": 12,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -302,7 +330,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"In B sind Folgen auch Funktionen, Funktionen auch Relationen, Relationen auch Mengen.\n",
"Relationen können in Jupyter auch grafisch dargestellt werden."
@@ -310,7 +342,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 6,
"metadata": {},
"outputs": [
{
@@ -419,7 +451,7 @@
"<Dot visualization: expr_as_graph [(\"k5\",{x,y|x:1..5 & y:1..5 & x>y})]>"
]
},
- "execution_count": 13,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -430,7 +462,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
@@ -439,7 +471,7 @@
"Preference changed: DOT_ENGINE = circo\n"
]
},
- "execution_count": 14,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -450,7 +482,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 8,
"metadata": {},
"outputs": [
{
@@ -559,7 +591,7 @@
"<Dot visualization: expr_as_graph [(\"k5\",{x,y|x:1..5 & y:1..5 & x>y})]>"
]
},
- "execution_count": 15,
+ "execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
@@ -642,7 +674,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 9,
"metadata": {},
"outputs": [
{
@@ -651,7 +683,7 @@
"Loaded machine: Jupyter_LibraryRegex"
]
},
- "execution_count": 16,
+ "execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
@@ -665,7 +697,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"### REGEX_SEARCH_ALL\n",
"This external function searches for **all** occurences of a pattern in a string and returns the matched strings as a B sequence.\n",
@@ -676,7 +712,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 10,
"metadata": {},
"outputs": [
{
@@ -688,7 +724,7 @@
"{(1↦\"234\"),(2↦\"567\")}"
]
},
- "execution_count": 18,
+ "execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
@@ -699,7 +735,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 11,
"metadata": {},
"outputs": [
{
@@ -711,7 +747,7 @@
"[\"a\",\"b\",\"c\",\"ä\",\"é\",\"à\"]"
]
},
- "execution_count": 19,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -728,15 +764,26 @@
}
},
"source": [
- "# Anwendung: Interaktive Skripte\n",
+ "# Anwendung: Interaktive Skripte für Vorlesungen\n",
"\n"
]
},
{
"cell_type": "code",
- "execution_count": null,
+ "execution_count": 12,
"metadata": {},
- "outputs": [],
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: BaseTypes"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
"source": [
"::load\n",
"MACHINE BaseTypes\n",
@@ -746,7 +793,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"In mathematics a binary relation over the sets $A$ and $B$ is defined to be\n",
" a subset of $A\\times B$.\n",
@@ -757,7 +808,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 13,
"metadata": {},
"outputs": [
{
@@ -769,7 +820,7 @@
"{(peter↦red),(peter↦green),(peter↦blue),(paul↦red),(paul↦green),(paul↦blue),(mary↦red),(mary↦green),(mary↦blue)}"
]
},
- "execution_count": 24,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -780,14 +831,18 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"A particular relation could be the following one, which is a subset of PERSONS × COLOURS:"
]
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 14,
"metadata": {},
"outputs": [
{
@@ -799,7 +854,7 @@
"{(peter↦green),(peter↦blue),(mary↦blue)}"
]
},
- "execution_count": 25,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -810,14 +865,18 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"We can visualize this relation graphically as follows:"
]
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 15,
"metadata": {},
"outputs": [
{
@@ -887,7 +946,7 @@
"<Dot visualization: expr_as_graph [(\"r1\",{(peter,green),(peter,blue),(mary,blue)})]>"
]
},
- "execution_count": 29,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -898,7 +957,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 16,
"metadata": {},
"outputs": [
{
@@ -917,7 +976,7 @@
"mary\tblue\n"
]
},
- "execution_count": 31,
+ "execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
@@ -928,7 +987,11 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
"source": [
"As in B a relation is a set of pairs, all set operators can be applied to relations.\n",
"For example,"
@@ -936,7 +999,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 17,
"metadata": {},
"outputs": [
{
@@ -948,7 +1011,7 @@
"{(peter↦green),(peter↦blue)}"
]
},
- "execution_count": 30,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
@@ -959,7 +1022,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 18,
"metadata": {},
"outputs": [
{
@@ -971,7 +1034,7 @@
"{(mary↦blue)}"
]
},
- "execution_count": 32,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
@@ -980,6 +1043,1575 @@
"{peter|->green,peter|->blue,mary|->blue} /\\ {mary}*COLOURS"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "# Anwendung: Skript für theoretische Informatik\n",
+ "\n",
+ "## NFA\n",
+ "\n",
+ "Nun erweitern wir die Überführungsfunktion in der Definition eines DFA \n",
+ "und bezeichnen die neuen Automaten als NFA.\n",
+ "\n",
+ "#### DEFINITION 2.9 (NFA)\n",
+ "Ein nichtdeterministischer endlicher Automat \n",
+ "(kurz NFA) ist ein Quintupel $M = (\\Sigma, Z, \\delta , S, F)$, wobei\n",
+ "\n",
+ "* $\\Sigma$ ein Alphabet ist,\n",
+ "* $Z$ eine endliche Menge von Zust\"anden mit $\\Sigma \\cap Z = \\emptyset$,\n",
+ "* $\\delta : Z \\times \\Sigma \\rightarrow \\pow(Z)$ die\n",
+ " Überführungsfunktion (hier: $\\pow(Z)$ ist die Potenzmenge\n",
+ " von $Z$, also die Menge aller Teilmengen von $Z$),\n",
+ "* $S \\subseteq Z$ die Menge der Startzustände und\n",
+ "* $F \\subseteq Z$ die Menge der Endzustände (Finalzustände).\n",
+ "\n",
+ "\n",
+ "#### DEFINITION 2.10 (Sprache eines 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"
+ ]
+ },
+ {
+ "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 $\\Sigma$.\n",
+ "Auch kann man leider weder ' noch $\\hat$ in Bezeichnern verwenden.\n",
+ "Deshalb wird aus\n",
+ "* $\\Sigma$ wird ```Sig```\n",
+ "* $\\Sigma^*$ wird ```seq(Seq)```\n",
+ "* $\\delta$ wird ```delta```\n",
+ "* $\\widehat{\\delta}$ wird ```deltas```"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 122,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NFA_to_DFA"
+ ]
+ },
+ "execution_count": 122,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE NFA_nach_DFA\n",
+ "SETS\n",
+ " Z = {z0,z1,z2,z3}\n",
+ "ABSTRACT_CONSTANTS deltas, L\n",
+ "CONSTANTS S, F, delta\n",
+ "PROPERTIES\n",
+ " S ⊆ Z ∧ F ⊆ Z ∧ delta ∈ (Z×Sig) → ℙ(Z) ∧\n",
+ "\n",
+ " /* Definition der erweiterten Übergangsfunktion */\n",
+ " deltas = λ(ZZ,s).(ZZ⊆Z | IF s=[] THEN ZZ ELSE UNION(z).(z∈ZZ|deltas(delta(z,first(s)),tail(s))) END )\n",
+ " ∧\n",
+ " /* die vom Automaten generierte Sprache */\n",
+ " L = {s|s∈seq(Sig) ∧ deltas(S,s) ∩ F ≠ ∅}\n",
+ " ∧\n",
+ " /* Nun ein Beispiel-Automat von Folie 24 (Info 4) */\n",
+ " S = {z0} ∧ F={z2} ∧\n",
+ " delta = { (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": 123,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 123,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 124,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 124,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "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": 125,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{z0},\\mathit{z1}\\}$"
+ ],
+ "text/plain": [
+ "{z0,z1}"
+ ]
+ },
+ "execution_count": 125,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "delta(z0,1)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Der obige Automat ist nichtdeterministisch, da zum Beispiel:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 126,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2$"
+ ],
+ "text/plain": [
+ "2"
+ ]
+ },
+ "execution_count": 126,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "card(delta(z0,1))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Wir können die Übergangsfunktion $\\delta$ des Automaten auch als Tabelle oder Graphen darstellen:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 134,
+ "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": 134,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table delta"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 133,
+ "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:delta(x, 0)})]>"
+ ]
+ },
+ "execution_count": 133,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"0\",{x,y| x∈Z & y:delta(x,0)},\"1\",{x,y| x∈S & y:delta(x,1)})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "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": 131,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{z0},\\mathit{z1},\\mathit{z2},\\mathit{z3}\\}$"
+ ],
+ "text/plain": [
+ "{z0,z1,z2,z3}"
+ ]
+ },
+ "execution_count": 131,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "deltas(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": 128,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{z2}\\}$"
+ ],
+ "text/plain": [
+ "{z2}"
+ ]
+ },
+ "execution_count": 128,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "deltas(S,[1,1,1]) ∩ F"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 129,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 129,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "deltas(S,[1,0,1]) ∩ F"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Folgende Wörter der Länge 3 werden vom Automaten akzeptiert:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 136,
+ "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": 136,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {x,y,z| [x,y,z]∈L}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "und folgende werden nicht akzeptiert:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 140,
+ "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": 140,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {x,y,z| {x,y,z} ⊆ Sig & not([x,y,z]∈L)}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "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\\}$."
+ ]
+ },
+ {
+ "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": 141,
+ "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": 141,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "ℙ(Z)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "Tabellarisch k¨ønnen wir $\\widehat{\\delta}$ für $\\pow(Z)$ wie folgt ausrechnen:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 144,
+ "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": 144,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {x,a,y| a:Sig & x∈ℙ(Z) & y=deltas(x,[a])}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "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": 147,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n"
+ ]
+ },
+ "execution_count": 147,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref DOT_DECOMPOSE_NODES=FALSE"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 153,
+ "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) & deltas(x, [0])=y})]>"
+ ]
+ },
+ "execution_count": 153,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"0\",{x,y| x∈ℙ(Z) & deltas(x,[0]) = y},\n",
+ " \"1\",{x,y| x∈ℙ(Z) & deltas(x,[1]) = y},\n",
+ " \"start\", {x,y|x=y & x={z0}},\n",
+ " \"end\", {x,y|x=y & x∩F ≠ ∅})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Anwendung: Prüfbericht\n",
+ "\n",
+ "Dieser Bericht wurde mit folgender Version von ProB erstellt:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "ProB CLI: 1.9.0-nightly (6b5c5ef186e29710bc4c6a651339f67f972db657)\n",
+ "ProB 2: 3.2.12-SNAPSHOT (16945773c7a5d9b44c1061db2a89cdd9e1da3cc3)"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":version"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "We read in a CSV data file containing the chemical elements:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: ChemicalElements"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE ChemicalElements\n",
+ "DEFINITIONS\n",
+ " \"LibraryStrings.def\";\n",
+ " \"LibraryCSV.def\"\n",
+ "CONSTANTS eltable\n",
+ "PROPERTIES\n",
+ " eltable : POW(STRING*STRING*INTEGER*STRING) &\n",
+ " eltable = READ_CSV(\"csv/elementdata.csv\",TRUE,TRUE) // we skip line 1 and extra columns\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "We have read in the following number of elements:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$118$"
+ ],
+ "text/plain": [
+ "118"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "card(eltable)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|prj111|prj112|prj12|prj2|\n",
+ "|---|---|---|---|\n",
+ "|$\\text{\"Actinium\"}$|$\\text{\"Ac\"}$|$89$|$\\text{\"227.0278\"}$|\n",
+ "|$\\text{\"Aluminum\"}$|$\\text{\"Al\"}$|$13$|$\\text{\"26.981539\"}$|\n",
+ "|$\\text{\"Americium\"}$|$\\text{\"Am\"}$|$95$|$\\text{\"243.0614\"}$|\n",
+ "|$\\text{\"Antimony\"}$|$\\text{\"Sb\"}$|$51$|$\\text{\"121.76\"}$|\n",
+ "|$\\text{\"Argon\"}$|$\\text{\"Ar\"}$|$18$|$\\text{\"39.948\"}$|\n",
+ "|$\\text{\"Arsenic\"}$|$\\text{\"As\"}$|$33$|$\\text{\"74.92159\"}$|\n",
+ "|$\\text{\"Astatine\"}$|$\\text{\"At\"}$|$85$|$\\text{\"209.9871\"}$|\n",
+ "|$\\text{\"Barium\"}$|$\\text{\"Ba\"}$|$56$|$\\text{\"137.327\"}$|\n",
+ "|$\\text{\"Berkelium\"}$|$\\text{\"Bk\"}$|$97$|$\\text{\"247.0703\"}$|\n",
+ "|$\\text{\"Beryllium\"}$|$\\text{\"Be\"}$|$4$|$\\text{\"9.01218\"}$|\n",
+ "|$\\text{\"Bismuth\"}$|$\\text{\"Bi\"}$|$83$|$\\text{\"208.98037\"}$|\n",
+ "|$\\text{\"Bohrium\"}$|$\\text{\"Bh\"}$|$107$|$\\text{\"[264]\"}$|\n",
+ "|$\\text{\"Boron\"}$|$\\text{\"B\"}$|$5$|$\\text{\"10.811\"}$|\n",
+ "|$\\text{\"Bromine\"}$|$\\text{\"Br\"}$|$35$|$\\text{\"79.904\"}$|\n",
+ "|$\\text{\"Cadmium\"}$|$\\text{\"Cd\"}$|$48$|$\\text{\"112.411\"}$|\n",
+ "|$\\text{\"Calcium\"}$|$\\text{\"Ca\"}$|$20$|$\\text{\"40.078\"}$|\n",
+ "|$\\text{\"Californium\"}$|$\\text{\"Cf\"}$|$98$|$\\text{\"251.0796\"}$|\n",
+ "|$\\text{\"Carbon\"}$|$\\text{\"C\"}$|$6$|$\\text{\"12.011\"}$|\n",
+ "|$\\text{\"Cerium\"}$|$\\text{\"Ce\"}$|$58$|$\\text{\"140.115\"}$|\n",
+ "|$\\text{\"Cesium\"}$|$\\text{\"Cs\"}$|$55$|$\\text{\"132.90543\"}$|\n",
+ "|$\\text{\"Chlorine\"}$|$\\text{\"Cl\"}$|$17$|$\\text{\"35.4527\"}$|\n",
+ "|$\\text{\"Chromium\"}$|$\\text{\"Cr\"}$|$24$|$\\text{\"51.9961\"}$|\n",
+ "|$\\text{\"Cobalt\"}$|$\\text{\"Co\"}$|$27$|$\\text{\"58.9332\"}$|\n",
+ "|$\\text{\"Copper\"}$|$\\text{\"Cu\"}$|$29$|$\\text{\"63.546\"}$|\n",
+ "|$\\text{\"Curium\"}$|$\\text{\"Cm\"}$|$96$|$\\text{\"247.0703\"}$|\n",
+ "|$\\text{\"Dubnium\"}$|$\\text{\"Db\"}$|$105$|$\\text{\"[262]\"}$|\n",
+ "|$\\text{\"Dysprosium\"}$|$\\text{\"Dy\"}$|$66$|$\\text{\"162.5\"}$|\n",
+ "|$\\text{\"Einsteinium\"}$|$\\text{\"Es\"}$|$99$|$\\text{\"252.083\"}$|\n",
+ "|$\\text{\"Erbium\"}$|$\\text{\"Er\"}$|$68$|$\\text{\"167.26\"}$|\n",
+ "|$\\text{\"Europium\"}$|$\\text{\"Eu\"}$|$63$|$\\text{\"151.965\"}$|\n",
+ "|$\\text{\"Fermium\"}$|$\\text{\"Fm\"}$|$100$|$\\text{\"257.0951\"}$|\n",
+ "|$\\text{\"Fluorine\"}$|$\\text{\"F\"}$|$9$|$\\text{\"18.998403\"}$|\n",
+ "|$\\text{\"Francium\"}$|$\\text{\"Fr\"}$|$87$|$\\text{\"223.0197\"}$|\n",
+ "|$\\text{\"Gadolinium\"}$|$\\text{\"Gd\"}$|$64$|$\\text{\"157.25\"}$|\n",
+ "|$\\text{\"Gallium\"}$|$\\text{\"Ga\"}$|$31$|$\\text{\"69.723\"}$|\n",
+ "|$\\text{\"Germanium\"}$|$\\text{\"Ge\"}$|$32$|$\\text{\"72.61\"}$|\n",
+ "|$\\text{\"Gold\"}$|$\\text{\"Au\"}$|$79$|$\\text{\"196.96654\"}$|\n",
+ "|$\\text{\"Hafnium\"}$|$\\text{\"Hf\"}$|$72$|$\\text{\"178.49\"}$|\n",
+ "|$\\text{\"Hassium\"}$|$\\text{\"Hs\"}$|$108$|$\\text{\"[269]\"}$|\n",
+ "|$\\text{\"Helium\"}$|$\\text{\"He\"}$|$2$|$\\text{\"4.002602\"}$|\n",
+ "|$\\text{\"Holmium\"}$|$\\text{\"Ho\"}$|$67$|$\\text{\"164.93032\"}$|\n",
+ "|$\\text{\"Hydrogen\"}$|$\\text{\"H\"}$|$1$|$\\text{\"1.00794\"}$|\n",
+ "|$\\text{\"Indium\"}$|$\\text{\"In\"}$|$49$|$\\text{\"114.818\"}$|\n",
+ "|$\\text{\"Iodine\"}$|$\\text{\"I\"}$|$53$|$\\text{\"126.90447\"}$|\n",
+ "|$\\text{\"Iridium\"}$|$\\text{\"Ir\"}$|$77$|$\\text{\"192.22\"}$|\n",
+ "|$\\text{\"Iron\"}$|$\\text{\"Fe\"}$|$26$|$\\text{\"55.847\"}$|\n",
+ "|$\\text{\"Krypton\"}$|$\\text{\"Kr\"}$|$36$|$\\text{\"83.8\"}$|\n",
+ "|$\\text{\"Lanthanum\"}$|$\\text{\"La\"}$|$57$|$\\text{\"138.9055\"}$|\n",
+ "|$\\text{\"Lawrencium\"}$|$\\text{\"Lr\"}$|$103$|$\\text{\"262.11\"}$|\n",
+ "|$\\text{\"Lead\"}$|$\\text{\"Pb\"}$|$82$|$\\text{\"207.2\"}$|\n",
+ "|$\\text{\"Lithium\"}$|$\\text{\"Li\"}$|$3$|$\\text{\"6.941\"}$|\n",
+ "|$\\text{\"Lutetium\"}$|$\\text{\"Lu\"}$|$71$|$\\text{\"174.967\"}$|\n",
+ "|$\\text{\"Magnesium\"}$|$\\text{\"Mg\"}$|$12$|$\\text{\"24.305\"}$|\n",
+ "|$\\text{\"Manganese\"}$|$\\text{\"Mn\"}$|$25$|$\\text{\"54.93805\"}$|\n",
+ "|$\\text{\"Meitnerium\"}$|$\\text{\"Mt\"}$|$109$|$\\text{\"[268]\"}$|\n",
+ "|$\\text{\"Mendelevium\"}$|$\\text{\"Md\"}$|$101$|$\\text{\"258.1\"}$|\n",
+ "|$\\text{\"Mercury\"}$|$\\text{\"Hg\"}$|$80$|$\\text{\"200.59\"}$|\n",
+ "|$\\text{\"Molybdenum\"}$|$\\text{\"Mo\"}$|$42$|$\\text{\"95.94\"}$|\n",
+ "|$\\text{\"Neodymium\"}$|$\\text{\"Nd\"}$|$60$|$\\text{\"144.24\"}$|\n",
+ "|$\\text{\"Neon\"}$|$\\text{\"Ne\"}$|$10$|$\\text{\"20.1797\"}$|\n",
+ "|$\\text{\"Neptunium\"}$|$\\text{\"Np\"}$|$93$|$\\text{\"237.048\"}$|\n",
+ "|$\\text{\"Nickel\"}$|$\\text{\"Ni\"}$|$28$|$\\text{\"58.6934\"}$|\n",
+ "|$\\text{\"Niobium\"}$|$\\text{\"Nb\"}$|$41$|$\\text{\"92.90638\"}$|\n",
+ "|$\\text{\"Nitrogen\"}$|$\\text{\"N\"}$|$7$|$\\text{\"14.00674\"}$|\n",
+ "|$\\text{\"Nobelium\"}$|$\\text{\"No\"}$|$102$|$\\text{\"259.1009\"}$|\n",
+ "|$\\text{\"Osmium\"}$|$\\text{\"Os\"}$|$76$|$\\text{\"190.23\"}$|\n",
+ "|$\\text{\"Oxygen\"}$|$\\text{\"O\"}$|$8$|$\\text{\"15.9994\"}$|\n",
+ "|$\\text{\"Palladium\"}$|$\\text{\"Pd\"}$|$46$|$\\text{\"106.42\"}$|\n",
+ "|$\\text{\"Phosphorus\"}$|$\\text{\"P\"}$|$15$|$\\text{\"30.973762\"}$|\n",
+ "|$\\text{\"Platinum\"}$|$\\text{\"Pt\"}$|$78$|$\\text{\"195.08\"}$|\n",
+ "|$\\text{\"Plutonium\"}$|$\\text{\"Pu\"}$|$94$|$\\text{\"244.0642\"}$|\n",
+ "|$\\text{\"Polonium\"}$|$\\text{\"Po\"}$|$84$|$\\text{\"208.9824\"}$|\n",
+ "|$\\text{\"Potassium\"}$|$\\text{\"K\"}$|$19$|$\\text{\"39.0983\"}$|\n",
+ "|$\\text{\"Praseodymium\"}$|$\\text{\"Pr\"}$|$59$|$\\text{\"140.90765\"}$|\n",
+ "|$\\text{\"Promethium\"}$|$\\text{\"Pm\"}$|$61$|$\\text{\"144.9127\"}$|\n",
+ "|$\\text{\"Protactinium\"}$|$\\text{\"Pa\"}$|$91$|$\\text{\"231.03588\"}$|\n",
+ "|$\\text{\"Radium\"}$|$\\text{\"Ra\"}$|$88$|$\\text{\"226.0254\"}$|\n",
+ "|$\\text{\"Radon\"}$|$\\text{\"Rn\"}$|$86$|$\\text{\"222.0176\"}$|\n",
+ "|$\\text{\"Rhenium\"}$|$\\text{\"Re\"}$|$75$|$\\text{\"186.207\"}$|\n",
+ "|$\\text{\"Rhodium\"}$|$\\text{\"Rh\"}$|$45$|$\\text{\"102.9055\"}$|\n",
+ "|$\\text{\"Rubidium\"}$|$\\text{\"Rb\"}$|$37$|$\\text{\"85.4678\"}$|\n",
+ "|$\\text{\"Ruthenium\"}$|$\\text{\"Ru\"}$|$44$|$\\text{\"101.07\"}$|\n",
+ "|$\\text{\"Rutherfordium\"}$|$\\text{\"Rf\"}$|$104$|$\\text{\"[261]\"}$|\n",
+ "|$\\text{\"Samarium\"}$|$\\text{\"Sm\"}$|$62$|$\\text{\"150.36\"}$|\n",
+ "|$\\text{\"Scandium\"}$|$\\text{\"Sc\"}$|$21$|$\\text{\"44.95591\"}$|\n",
+ "|$\\text{\"Seaborgium\"}$|$\\text{\"Sg\"}$|$106$|$\\text{\"[266]\"}$|\n",
+ "|$\\text{\"Selenium\"}$|$\\text{\"Se\"}$|$34$|$\\text{\"78.96\"}$|\n",
+ "|$\\text{\"Silicon\"}$|$\\text{\"Si\"}$|$14$|$\\text{\"28.0855\"}$|\n",
+ "|$\\text{\"Silver\"}$|$\\text{\"Ag\"}$|$47$|$\\text{\"107.8682\"}$|\n",
+ "|$\\text{\"Sodium\"}$|$\\text{\"Na\"}$|$11$|$\\text{\"22.989768\"}$|\n",
+ "|$\\text{\"Strontium\"}$|$\\text{\"Sr\"}$|$38$|$\\text{\"87.62\"}$|\n",
+ "|$\\text{\"Sulfur\"}$|$\\text{\"S\"}$|$16$|$\\text{\"32.066\"}$|\n",
+ "|$\\text{\"Tantalum\"}$|$\\text{\"Ta\"}$|$73$|$\\text{\"180.9479\"}$|\n",
+ "|$\\text{\"Technetium\"}$|$\\text{\"Tc\"}$|$43$|$\\text{\"97.9072\"}$|\n",
+ "|$\\text{\"Tellurium\"}$|$\\text{\"Te\"}$|$52$|$\\text{\"127.6\"}$|\n",
+ "|$\\text{\"Terbium\"}$|$\\text{\"Tb\"}$|$65$|$\\text{\"158.92534\"}$|\n",
+ "|$\\text{\"Thallium\"}$|$\\text{\"Tl\"}$|$81$|$\\text{\"204.3833\"}$|\n",
+ "|$\\text{\"Thorium\"}$|$\\text{\"Th\"}$|$90$|$\\text{\"232.0381\"}$|\n",
+ "|$\\text{\"Thulium\"}$|$\\text{\"Tm\"}$|$69$|$\\text{\"168.93421\"}$|\n",
+ "|$\\text{\"Tin\"}$|$\\text{\"Sn\"}$|$50$|$\\text{\"118.71\"}$|\n",
+ "|$\\text{\"Titanium\"}$|$\\text{\"Ti\"}$|$22$|$\\text{\"47.88\"}$|\n",
+ "|$\\text{\"Tungsten\"}$|$\\text{\"W\"}$|$74$|$\\text{\"183.84\"}$|\n",
+ "|$\\text{\"Ununbium\"}$|$\\text{\"Uub\"}$|$112$|$\\text{\"[277]\"}$|\n",
+ "|$\\text{\"Ununhexium\"}$|$\\text{\"Uuh\"}$|$116$|$\\text{\"-\"}$|\n",
+ "|$\\text{\"Ununnilium\"}$|$\\text{\"Uun\"}$|$110$|$\\text{\"[269]\"}$|\n",
+ "|$\\text{\"Ununoctium\"}$|$\\text{\"Uuo\"}$|$118$|$\\text{\"-\"}$|\n",
+ "|$\\text{\"Ununpentium\"}$|$\\text{\"Uup\"}$|$115$|$\\text{\"-\"}$|\n",
+ "|$\\text{\"Ununquadium\"}$|$\\text{\"Uuq\"}$|$114$|$\\text{\"[289]\"}$|\n",
+ "|$\\text{\"Ununseptium\"}$|$\\text{\"Uus\"}$|$117$|$\\text{\"-\"}$|\n",
+ "|$\\text{\"Ununtrium\"}$|$\\text{\"Uut\"}$|$113$|$\\text{\"-\"}$|\n",
+ "|$\\text{\"Unununium\"}$|$\\text{\"Uuu\"}$|$111$|$\\text{\"[272]\"}$|\n",
+ "|$\\text{\"Uranium\"}$|$\\text{\"U\"}$|$92$|$\\text{\"238.0289\"}$|\n",
+ "|$\\text{\"Vanadium\"}$|$\\text{\"V\"}$|$23$|$\\text{\"50.9415\"}$|\n",
+ "|$\\text{\"Xenon\"}$|$\\text{\"Xe\"}$|$54$|$\\text{\"131.29\"}$|\n",
+ "|$\\text{\"Ytterbium\"}$|$\\text{\"Yb\"}$|$70$|$\\text{\"173.04\"}$|\n",
+ "|$\\text{\"Yttrium\"}$|$\\text{\"Y\"}$|$39$|$\\text{\"88.90585\"}$|\n",
+ "|$\\text{\"Zinc\"}$|$\\text{\"Zn\"}$|$30$|$\\text{\"65.39\"}$|\n",
+ "|$\\text{\"Zirconium\"}$|$\\text{\"Zr\"}$|$40$|$\\text{\"91.224\"}$|\n"
+ ],
+ "text/plain": [
+ "prj111\tprj112\tprj12\tprj2\n",
+ "\"Actinium\"\t\"Ac\"\t89\t\"227.0278\"\n",
+ "\"Aluminum\"\t\"Al\"\t13\t\"26.981539\"\n",
+ "\"Americium\"\t\"Am\"\t95\t\"243.0614\"\n",
+ "\"Antimony\"\t\"Sb\"\t51\t\"121.76\"\n",
+ "\"Argon\"\t\"Ar\"\t18\t\"39.948\"\n",
+ "\"Arsenic\"\t\"As\"\t33\t\"74.92159\"\n",
+ "\"Astatine\"\t\"At\"\t85\t\"209.9871\"\n",
+ "\"Barium\"\t\"Ba\"\t56\t\"137.327\"\n",
+ "\"Berkelium\"\t\"Bk\"\t97\t\"247.0703\"\n",
+ "\"Beryllium\"\t\"Be\"\t4\t\"9.01218\"\n",
+ "\"Bismuth\"\t\"Bi\"\t83\t\"208.98037\"\n",
+ "\"Bohrium\"\t\"Bh\"\t107\t\"[264]\"\n",
+ "\"Boron\"\t\"B\"\t5\t\"10.811\"\n",
+ "\"Bromine\"\t\"Br\"\t35\t\"79.904\"\n",
+ "\"Cadmium\"\t\"Cd\"\t48\t\"112.411\"\n",
+ "\"Calcium\"\t\"Ca\"\t20\t\"40.078\"\n",
+ "\"Californium\"\t\"Cf\"\t98\t\"251.0796\"\n",
+ "\"Carbon\"\t\"C\"\t6\t\"12.011\"\n",
+ "\"Cerium\"\t\"Ce\"\t58\t\"140.115\"\n",
+ "\"Cesium\"\t\"Cs\"\t55\t\"132.90543\"\n",
+ "\"Chlorine\"\t\"Cl\"\t17\t\"35.4527\"\n",
+ "\"Chromium\"\t\"Cr\"\t24\t\"51.9961\"\n",
+ "\"Cobalt\"\t\"Co\"\t27\t\"58.9332\"\n",
+ "\"Copper\"\t\"Cu\"\t29\t\"63.546\"\n",
+ "\"Curium\"\t\"Cm\"\t96\t\"247.0703\"\n",
+ "\"Dubnium\"\t\"Db\"\t105\t\"[262]\"\n",
+ "\"Dysprosium\"\t\"Dy\"\t66\t\"162.5\"\n",
+ "\"Einsteinium\"\t\"Es\"\t99\t\"252.083\"\n",
+ "\"Erbium\"\t\"Er\"\t68\t\"167.26\"\n",
+ "\"Europium\"\t\"Eu\"\t63\t\"151.965\"\n",
+ "\"Fermium\"\t\"Fm\"\t100\t\"257.0951\"\n",
+ "\"Fluorine\"\t\"F\"\t9\t\"18.998403\"\n",
+ "\"Francium\"\t\"Fr\"\t87\t\"223.0197\"\n",
+ "\"Gadolinium\"\t\"Gd\"\t64\t\"157.25\"\n",
+ "\"Gallium\"\t\"Ga\"\t31\t\"69.723\"\n",
+ "\"Germanium\"\t\"Ge\"\t32\t\"72.61\"\n",
+ "\"Gold\"\t\"Au\"\t79\t\"196.96654\"\n",
+ "\"Hafnium\"\t\"Hf\"\t72\t\"178.49\"\n",
+ "\"Hassium\"\t\"Hs\"\t108\t\"[269]\"\n",
+ "\"Helium\"\t\"He\"\t2\t\"4.002602\"\n",
+ "\"Holmium\"\t\"Ho\"\t67\t\"164.93032\"\n",
+ "\"Hydrogen\"\t\"H\"\t1\t\"1.00794\"\n",
+ "\"Indium\"\t\"In\"\t49\t\"114.818\"\n",
+ "\"Iodine\"\t\"I\"\t53\t\"126.90447\"\n",
+ "\"Iridium\"\t\"Ir\"\t77\t\"192.22\"\n",
+ "\"Iron\"\t\"Fe\"\t26\t\"55.847\"\n",
+ "\"Krypton\"\t\"Kr\"\t36\t\"83.8\"\n",
+ "\"Lanthanum\"\t\"La\"\t57\t\"138.9055\"\n",
+ "\"Lawrencium\"\t\"Lr\"\t103\t\"262.11\"\n",
+ "\"Lead\"\t\"Pb\"\t82\t\"207.2\"\n",
+ "\"Lithium\"\t\"Li\"\t3\t\"6.941\"\n",
+ "\"Lutetium\"\t\"Lu\"\t71\t\"174.967\"\n",
+ "\"Magnesium\"\t\"Mg\"\t12\t\"24.305\"\n",
+ "\"Manganese\"\t\"Mn\"\t25\t\"54.93805\"\n",
+ "\"Meitnerium\"\t\"Mt\"\t109\t\"[268]\"\n",
+ "\"Mendelevium\"\t\"Md\"\t101\t\"258.1\"\n",
+ "\"Mercury\"\t\"Hg\"\t80\t\"200.59\"\n",
+ "\"Molybdenum\"\t\"Mo\"\t42\t\"95.94\"\n",
+ "\"Neodymium\"\t\"Nd\"\t60\t\"144.24\"\n",
+ "\"Neon\"\t\"Ne\"\t10\t\"20.1797\"\n",
+ "\"Neptunium\"\t\"Np\"\t93\t\"237.048\"\n",
+ "\"Nickel\"\t\"Ni\"\t28\t\"58.6934\"\n",
+ "\"Niobium\"\t\"Nb\"\t41\t\"92.90638\"\n",
+ "\"Nitrogen\"\t\"N\"\t7\t\"14.00674\"\n",
+ "\"Nobelium\"\t\"No\"\t102\t\"259.1009\"\n",
+ "\"Osmium\"\t\"Os\"\t76\t\"190.23\"\n",
+ "\"Oxygen\"\t\"O\"\t8\t\"15.9994\"\n",
+ "\"Palladium\"\t\"Pd\"\t46\t\"106.42\"\n",
+ "\"Phosphorus\"\t\"P\"\t15\t\"30.973762\"\n",
+ "\"Platinum\"\t\"Pt\"\t78\t\"195.08\"\n",
+ "\"Plutonium\"\t\"Pu\"\t94\t\"244.0642\"\n",
+ "\"Polonium\"\t\"Po\"\t84\t\"208.9824\"\n",
+ "\"Potassium\"\t\"K\"\t19\t\"39.0983\"\n",
+ "\"Praseodymium\"\t\"Pr\"\t59\t\"140.90765\"\n",
+ "\"Promethium\"\t\"Pm\"\t61\t\"144.9127\"\n",
+ "\"Protactinium\"\t\"Pa\"\t91\t\"231.03588\"\n",
+ "\"Radium\"\t\"Ra\"\t88\t\"226.0254\"\n",
+ "\"Radon\"\t\"Rn\"\t86\t\"222.0176\"\n",
+ "\"Rhenium\"\t\"Re\"\t75\t\"186.207\"\n",
+ "\"Rhodium\"\t\"Rh\"\t45\t\"102.9055\"\n",
+ "\"Rubidium\"\t\"Rb\"\t37\t\"85.4678\"\n",
+ "\"Ruthenium\"\t\"Ru\"\t44\t\"101.07\"\n",
+ "\"Rutherfordium\"\t\"Rf\"\t104\t\"[261]\"\n",
+ "\"Samarium\"\t\"Sm\"\t62\t\"150.36\"\n",
+ "\"Scandium\"\t\"Sc\"\t21\t\"44.95591\"\n",
+ "\"Seaborgium\"\t\"Sg\"\t106\t\"[266]\"\n",
+ "\"Selenium\"\t\"Se\"\t34\t\"78.96\"\n",
+ "\"Silicon\"\t\"Si\"\t14\t\"28.0855\"\n",
+ "\"Silver\"\t\"Ag\"\t47\t\"107.8682\"\n",
+ "\"Sodium\"\t\"Na\"\t11\t\"22.989768\"\n",
+ "\"Strontium\"\t\"Sr\"\t38\t\"87.62\"\n",
+ "\"Sulfur\"\t\"S\"\t16\t\"32.066\"\n",
+ "\"Tantalum\"\t\"Ta\"\t73\t\"180.9479\"\n",
+ "\"Technetium\"\t\"Tc\"\t43\t\"97.9072\"\n",
+ "\"Tellurium\"\t\"Te\"\t52\t\"127.6\"\n",
+ "\"Terbium\"\t\"Tb\"\t65\t\"158.92534\"\n",
+ "\"Thallium\"\t\"Tl\"\t81\t\"204.3833\"\n",
+ "\"Thorium\"\t\"Th\"\t90\t\"232.0381\"\n",
+ "\"Thulium\"\t\"Tm\"\t69\t\"168.93421\"\n",
+ "\"Tin\"\t\"Sn\"\t50\t\"118.71\"\n",
+ "\"Titanium\"\t\"Ti\"\t22\t\"47.88\"\n",
+ "\"Tungsten\"\t\"W\"\t74\t\"183.84\"\n",
+ "\"Ununbium\"\t\"Uub\"\t112\t\"[277]\"\n",
+ "\"Ununhexium\"\t\"Uuh\"\t116\t\"-\"\n",
+ "\"Ununnilium\"\t\"Uun\"\t110\t\"[269]\"\n",
+ "\"Ununoctium\"\t\"Uuo\"\t118\t\"-\"\n",
+ "\"Ununpentium\"\t\"Uup\"\t115\t\"-\"\n",
+ "\"Ununquadium\"\t\"Uuq\"\t114\t\"[289]\"\n",
+ "\"Ununseptium\"\t\"Uus\"\t117\t\"-\"\n",
+ "\"Ununtrium\"\t\"Uut\"\t113\t\"-\"\n",
+ "\"Unununium\"\t\"Uuu\"\t111\t\"[272]\"\n",
+ "\"Uranium\"\t\"U\"\t92\t\"238.0289\"\n",
+ "\"Vanadium\"\t\"V\"\t23\t\"50.9415\"\n",
+ "\"Xenon\"\t\"Xe\"\t54\t\"131.29\"\n",
+ "\"Ytterbium\"\t\"Yb\"\t70\t\"173.04\"\n",
+ "\"Yttrium\"\t\"Y\"\t39\t\"88.90585\"\n",
+ "\"Zinc\"\t\"Zn\"\t30\t\"65.39\"\n",
+ "\"Zirconium\"\t\"Zr\"\t40\t\"91.224\"\n"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table eltable"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "We now check the following property, that the atomic weights are not decreasing with increasing atomic number:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":assert: Assertion is not true: FALSE",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:assert: Assertion is not true: FALSE\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":assert !(n1,n2,s1,s2,nr,aw1,aw2).(\n",
+ " (n1,s1,nr,aw1):eltable & (n2,s2,nr+1,aw2):eltable\n",
+ " =>\n",
+ " DEC_STRING_TO_INT(aw1,3) <= DEC_STRING_TO_INT(aw2,3)\n",
+ " )"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "subslide"
+ }
+ },
+ "source": [
+ "We can now extract a table with the counter examples to the rule:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|n1|aw1|n2|aw2|\n",
+ "|---|---|---|---|\n",
+ "|$\\text{\"Argon\"}$|$\\text{\"39.948\"}$|$\\text{\"Potassium\"}$|$\\text{\"39.0983\"}$|\n",
+ "|$\\text{\"Cobalt\"}$|$\\text{\"58.9332\"}$|$\\text{\"Nickel\"}$|$\\text{\"58.6934\"}$|\n",
+ "|$\\text{\"Plutonium\"}$|$\\text{\"244.0642\"}$|$\\text{\"Americium\"}$|$\\text{\"243.0614\"}$|\n",
+ "|$\\text{\"Tellurium\"}$|$\\text{\"127.6\"}$|$\\text{\"Iodine\"}$|$\\text{\"126.90447\"}$|\n",
+ "|$\\text{\"Thorium\"}$|$\\text{\"232.0381\"}$|$\\text{\"Protactinium\"}$|$\\text{\"231.03588\"}$|\n",
+ "|$\\text{\"Uranium\"}$|$\\text{\"238.0289\"}$|$\\text{\"Neptunium\"}$|$\\text{\"237.048\"}$|\n"
+ ],
+ "text/plain": [
+ "n1\taw1\tn2\taw2\n",
+ "\"Argon\"\t\"39.948\"\t\"Potassium\"\t\"39.0983\"\n",
+ "\"Cobalt\"\t\"58.9332\"\t\"Nickel\"\t\"58.6934\"\n",
+ "\"Plutonium\"\t\"244.0642\"\t\"Americium\"\t\"243.0614\"\n",
+ "\"Tellurium\"\t\"127.6\"\t\"Iodine\"\t\"126.90447\"\n",
+ "\"Thorium\"\t\"232.0381\"\t\"Protactinium\"\t\"231.03588\"\n",
+ "\"Uranium\"\t\"238.0289\"\t\"Neptunium\"\t\"237.048\"\n"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {n1,aw1,n2,aw2|#(s1,s2,nr).(\n",
+ " (n1,s1,nr,aw1):eltable & STRING_IS_NUMBER(aw1) &\n",
+ " (n2,s2,nr+1,aw2):eltable & STRING_IS_NUMBER(aw2) &\n",
+ " DEC_STRING_TO_INT(aw1,3) > DEC_STRING_TO_INT(aw2,3))}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "# Future Work\n",
+ "\n",
+ "* Mehr Kommandos:\n",
+ " * Temporäre (\"lokale\") Variablen mit `:let`\n",
+ " * Verifikation (LTL, Model Checking)\n",
+ " * Diagramme: Plotten von Werten im Verlauf des Traces\n",
+ "* `In`/`Out`-Arrays um vorherige Eingaben/Ergebnisse abzurufen\n",
+ "* Integration mit ProB 2-Trace-Dateien\n",
+ " * Konvertierung zwischen `.prob2trace` und `.ipynb`"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "TO DO:\n",
+ "- Info4 Beispiel ?\n",
+ "- Railway Beispiel : Szenario mit Visualisierung"
+ ]
+ },
{
"cell_type": "code",
"execution_count": null,
diff --git a/notebooks/presentations/csv/elementdata.csv b/notebooks/presentations/csv/elementdata.csv
new file mode 100644
index 0000000000000000000000000000000000000000..be24205e33ca338d14da7694f538ffb8c7959df6
--- /dev/null
+++ b/notebooks/presentations/csv/elementdata.csv
@@ -0,0 +1,119 @@
+Name, Symbol, Atomic_Number, Atomic_Weight, Density, Melting_Point, Boiling_Point, Atomic_Radius, Covalent_Radius, Ionic_Radius, Specific_Volume, Specific_Heat, Heat_Fusion, Heat_Evaporation, Thermal_Conductivity, Pauling_Electronegativity, First_Ionisation_Energy, Oxidation_States, Electronic_Configuration, Lattice, Lattice_Constant
+Hydrogen, H,1,1.00794, 0.0708 (@ -253degC),14.01,20.28,79,32, ,14.1,14.267 (H-H), 0.117 (H-H), 0.904 (H-H),0.1815,2.2,1311.3, 1 -1, 1s¹, HEX,3.75
+Helium, He,2,4.002602, 0.147 (@ -270degC),0.95,4.216,0, -, ,31.8,5.188, -,0.08,0.152, -,2361.3, -, 1s², HEX,3.57
+Lithium, Li,3,6.941,0.534,553.69,1118.15,155,163, ,13.1,3.489,2.89,148,84.8,0.98,519.9,1, [He]2s¹, BCC,3.49
+Beryllium, Be,4,9.01218,1.848,1551,3243,112,90, ,5,1.824,12.21,309,201,1.57,898.8,2, [He]2s², HEX,2.29
+Boron, B,5,10.811,2.34,2573,3931,98,82, ,4.6,1.025,23.6,504.5,27.4,2.04,800.2,3, [He]2s²2p¹, TET,8.73
+Carbon, C,6,12.011, 2.25 (graphite),3820,5100,91,77, ,5.3,0.711, -, -,1.59,2.55,1085.7, 4 2 -4, [He]2s²2p², DIA,3.57
+Nitrogen, N,7,14.00674, 0.808 (@ -195.8degC),63.29,77.4,92,75, ,17.3,1.042 (N-N), -, -,0.026,3.04,1401.5, 5 4 3 2 -3, [He]2s²2p³, HEX,4.039
+Oxygen, O,8,15.9994, 1.149 (@ -183degC),54.8,90.19, -,73, ,14,0.916 (O-O), -, -,0.027,3.44,1313.1, -2 -1, [He]2s²2p, CUB,6.83
+Fluorine, F,9,18.998403, 1.108 (@ -189degC),53.53,85.01, -,72, ,17.1,0.824 (F-F), 0.51 (F-F), 6.54 (F-F),0.028,3.98,1680,-1, [He]2s²2p, MCL, -
+Neon, Ne,10,20.1797, 1.204 (@ -246degC),48,27.1, -,71, ,16.8,1.029, -,1.74,<0.0493>,0,2079.4, -, [He]2s²2p, FCC,4.43
+Sodium, Na,11,22.989768,0.971,370.96,1156.1,190,154, ,23.7,1.222,2.64,97.9,142,0.93,495.6,1, [Ne]3s¹, BCC,4.23
+Magnesium, Mg,12,24.305,1.738,922,1363,160,136, ,14,1.025,9.2,131.8,156,1.31,737.3,2, [Ne]3s², HEX,3.21
+Aluminum, Al,13,26.981539,2.6989,933.5,2740,143,118, ,10,0.9,10.75,284.1,237,1.61,577.2,3, [Ne]3s²3p¹, FCC,4.05
+Silicon, Si,14,28.0855,2.33,1683,2628,132,111, ,12.1,0.703,50.6,383,149,1.9,786, 4 -4, [Ne]3s²3p², DIA,5.43
+Phosphorus, P,15,30.973762, 1.82 (white phosphorus),317.3,553,128,106, ,17,0.757,2.51,49.8,<0.236>,2.19,1011.2, 5 3 -3, [Ne]3s²3p³, CUB,7.17
+Sulfur, S,16,32.066,2.07,386,717.824,127,102, ,15.5,0.732,1.23,10.5,0.27,2.58,999, 6 4 2 -2, [Ne]3s²3p, ORC,10.47
+Chlorine, Cl,17,35.4527, 1.56 (@ -33.6degC),172.2,238.6, -,99, ,18.7, 0.477 (Cl-Cl), 6.41 (Cl-Cl), 20.41 (Cl-Cl),0.009,3.16,1254.9, 7 5 3 1 -1, [Ne]3s²3p, ORC,6.24
+Argon, Ar,18,39.948, 1.40 (@ -186degC),83.8,87.3, -,98, ,24.2,0.138, -,6.52,0.0177,0,1519.6, -, [Ne]3s²3p, FCC,5.26
+Potassium, K,19,39.0983,0.856,336.8,1047,235,203, ,45.3,0.753,102.5,2.33,79,0.82,418.5,1, [Ar]4s¹, BCC,5.23
+Calcium, Ca,20,40.078,1.55,1112,1757,197,174, ,29.9,0.653,9.2,153.6,<201>,1,589.4,2, [Ar]4s², FCC,5.58
+Scandium, Sc,21,44.95591,2.99,1814,3104,162,144, ,15,0.556,15.8,332.7,15.8,1.36,630.8,3, [Ar]3d¹4s², HEX,3.31
+Titanium, Ti,22,47.88,4.54,1933,3560,147,132, ,10.6,0.523,18.8,422.6,21.9,1.54,657.8, 4 3, [Ar]3d²4s², HEX,2.95
+Vanadium, V,23,50.9415,6.11,2160,3650,134,122, ,8.35,0.485,17.5,460,30.7,1.63,650.1, 5 4 3 2 0, [Ar]3d³4s², BCC,3.02
+Chromium, Cr,24,51.9961,7.18,2130,2945,130,118, ,7.23,0.488,21,342,93.9,1.66,652.4, 6 3 2 0, [Ar]3d4s¹, BCC,2.88
+Manganese, Mn,25,54.93805,7.21,1517,2235,135,117, ,7.39,0.477,-13.4,221,<7.8>,1.55,716.8, 7 6 4 3 2 0 -1, [Ar]3d4s², CUB,8.89
+Iron, Fe,26,55.847,7.874,1808,3023,126,117, ,7.1,0.443,13.8, ~340,80.4,1.83,759.1, 6 3 2 0 -2, [Ar]3d4s², BCC,2.87
+Cobalt, Co,27,58.9332,8.9,1768,3143,125,116, ,6.7,0.456,15.48,389.1,100,1.88,758.1, 3 2 0 -1, [Ar]3d4s², HEX,2.51
+Nickel, Ni,28,58.6934,8.902,1726,3005,124,115, ,6.6,0.443,17.61,378.6,90.9,1.91,736.2, 3 2 0, [Ar]3d4s², FCC,3.52
+Copper, Cu,29,63.546,8.96,1356.6,2840,128,117, ,7.1,0.385,13.01,304.6,401,1.9,745, 2 1, [Ar]3d¹4s¹, FCC,3.61
+Zinc, Zn,30,65.39,7.133,692.73,1180,138,125, ,9.2,0.388,7.28,114.8,116,1.65,905.8,2, [Ar]3d¹4s², HEX,2.66
+Gallium, Ga,31,69.723,5.91,302.93,2676,141,126, ,11.8,0.372,5.59,270.3,28.1,1.81,578.7,3, [Ar]3d¹4s²4p¹, ORC,4.51
+Germanium, Ge,32,72.61,5.323,1210.6,3103,137,122, ,13.6,0.322,36.8,328,60.2,2.01,760,4, [Ar]3d¹4s²4p², DIA,5.66
+Arsenic, As,33,74.92159, 5.73 (grey arsenic),1090,876,139,120, ,13.1,0.328, -,32.4,<50.2>,2.18,946.2, 5 3 -2, [Ar]3d¹4s²4p³, RHL,4.13
+Selenium, Se,34,78.96,4.79,490,958.1,140,116, ,16.5,0.321 (Se-Se),5.23,59.7,0.52,2.55,940.4, 6 4 -2, [Ar]3d¹4s²4p, HEX,4.36
+Bromine, Br,35,79.904,3.12,265.9,331.9, -,114, ,23.5,0.473 (Br-Br), 10.57 (Br-Br), 29.56 (Br-Br),0.005,2.96,1142, 7 5 3 1 -1, [Ar]3d¹4s²4p, ORC,6.67
+Krypton, Kr,36,83.8, 2.155 (@ -153degC),116.6,120.85, -,112, ,32.2,0.247, -,9.05,0.0095,0,1350,2, [Ar]3d¹4s²4p, FCC,5.72
+Rubidium, Rb,37,85.4678,1.532,312.2,961,248,216, ,55.9,0.36,2.2,75.8,58.2,0.82,402.8,1, [Kr]5s¹, BCC,5.59
+Strontium, Sr,38,87.62,2.54,1042,1657,215,191, ,33.7,0.301,9.2,144,<35.4>,0.95,549,2, [Kr]5s², FCC,6.08
+Yttrium, Y,39,88.90585,4.47,1795,3611,178,162, ,19.8,0.284,11.5,367,<17.2>,1.22,615.4,3, [Kr]4d¹5s², HEX,3.65
+Zirconium, Zr,40,91.224,6.506,2125,4650,160,145, ,14.1,0.281,19.2,567,22.7,1.33,659.7,4, [Kr]4d²5s², HEX,3.23
+Niobium, Nb,41,92.90638,8.57,2741,5015,146,134, ,10.8,0.268,26.8,680,53.7,1.6,663.6, 5 3, [Kr]4d5s¹, BCC,3.3
+Molybdenum, Mo,42,95.94,10.22,2890,4885,139,130, ,9.4,0.251,28, ~590,<138>,2.16,684.8, 6 5 4 3 2 0, [Kr]4d5s¹, BCC,3.15
+Technetium, Tc,43,97.9072,11.5,2445,5150,136,127, ,8.5,0.243,23.8,585,50.6,1.9,702.2,7, [Kr]4d5s¹, HEX,2.74
+Ruthenium, Ru,44,101.07,12.41,2583,4173,134,125, ,8.3,0.238,<25.5>, -,117,2.2,710.3, 8 6 4 3 2 0 -2, [Kr]4d5s¹, HEX,2.7
+Rhodium, Rh,45,102.9055,12.41,2239,4000,134,125, ,8.3,0.244,21.8,494,150,2.28,719.5, 5 4 3 2 1 0, [Kr]4d5s¹, FCC,3.8
+Palladium, Pd,46,106.42,12.02,1825,3413,137,128, ,8.9,0.244,17.24,372.4,71.8,2.2,803.5, 4 2 0, [Kr]4d5s, FCC,3.89
+Silver, Ag,47,107.8682,10.5,1235.1,2485,144,134, ,10.3,0.237,11.95,254.1,429,1.93,730.5, 2 1, [Kr]4d5s¹, FCC,4.09
+Cadmium, Cd,48,112.411,8.65,594.1,1038,154,148, ,13.1,0.232,6.11,59.1,96.9,1.69,867.2,2, [Kr]4d5s², HEX,2.98
+Indium, In,49,114.818,7.31,429.32,2353,166,144, ,15.7,0.234,3.24,225.1,81.8,1.78,558,3, [Kr]4d5s²5p¹, TET,4.59
+Tin, Sn,50,118.71,7.31,505.1,2543,162,141, ,16.3,0.222,7.07,296,66.8,1.96,708.2, 4 2, [Kr]4d5s²5p², TET,5.82
+Antimony, Sb,51,121.76,6.691,903.9,1908,159,140, ,18.4,0.205,20.08,195.2,24.43,2.05,833.3, 5 3 -2, [Kr]4d5s²5p³, RHL,4.51
+Tellurium, Te,52,127.6,6.24,722.7,1263,160,136, ,20.5,0.201,17.91,49.8,14.3,2.1,869, 6 4 2, [Kr]4d5s²5p, HEX,4.45
+Iodine, I,53,126.90447,4.93,386.7,457.5, -,133, ,25.7,0.427 (I-I), 15.52 (I-I), 41.95 (I-I),<0.45>,2.66,1008.3, 7 5 1 -1, [Kr]4d5s²5p, ORC,7.72
+Xenon, Xe,54,131.29, 3.52 (@ -109degC),161.3,166.1, -,131, ,42.9,0.158, -,12.65,0.0057,0,1170,7, [Kr]4d5s²5p, FCC,6.2
+Cesium, Cs,55,132.90543,1.873,301.6,951.6,267,235, ,70,0.241,2.09,68.3,35.9,0.79,375.5,1, [Xe]6s¹, BCC,6.05
+Barium, Ba,56,137.327,3.5,1002,1910,222,198, ,39,0.192,7.66,142,<18.4>,0.89,502.5,2, [Xe]6s², BCC,5.02
+Lanthanum, La,57,138.9055,6.15,1194,3730,187,169, ,22.5,0.197,8.5,402,13.4,1.1,541.1,3, [Xe]6d¹6s², HEX,3.75
+Cerium, Ce,58,140.115,6.757,1072,3699,181,165, ,21,0.205,5.2,398,11.3,1.12,540.1, 4 3, [Xe]4f¹5d¹6s², FCC,5.16
+Praseodymium, Pr,59,140.90765,6.773,1204,3785,182,165, ,20.8,0.192,11.3,331,12.5,1.13,526.6, 4 3, [Xe]4f³5d6s², HEX,3.67
+Neodymium, Nd,60,144.24,7.007,1294,3341,182,184, ,20.6,0.205,7.1,289,<16.5>,1.14,531.5,3, [Xe]4f5d6s², HEX,3.66
+Promethium, Pm,61,144.9127,7.2,1441,3000, -,163, , -,0.185, -, -,17.9,0,536,3, [Xe]4f5d6s², -, -
+Samarium, Sm,62,150.36,7.52,1350,2064,181,162, ,19.9,0.18,8.9,165,<13.3>,1.17,540.1, 3 2, [Xe]4f5d6s², RHL,9
+Europium, Eu,63,151.965,5.243,1095,1870,199,185, ,28.9,0.176, -,176,13.9,0,546.9, 3 2, [Xe]4f5d6s², BCC,4.61
+Gadolinium, Gd,64,157.25,7.9,1586,3539,179,161, ,19.9,0.23, -,398,<10.5>,1.2,594.2,3, [Xe]4f5d¹6s², HEX,3.64
+Terbium, Tb,65,158.92534,8.229,1629,3296,180,159, ,19.2,0.183, -,389,11.1,1.2,569, 4 3, [Xe]4f5d6s², HEX,3.6
+Dysprosium, Dy,66,162.5,8.55,1685,2835,180,159, ,19,0.173, -,291,10.7, -,567,3, [Xe]4f5d6s², HEX,3.59
+Holmium, Ho,67,164.93032,8.795,1747,2968,179,158, ,18.7,0.164, -,301,<16.2>,1.23,574,3, [Xe]4f¹¹5d6s², HEX,3.58
+Erbium, Er,68,167.26,9.06,1802,3136,178,157, ,18.4,0.168, -,317,<14.5>,1.24,581,3, [Xe]4f¹²5d6s², HEX,3.56
+Thulium, Tm,69,168.93421,9.321,1818,2220,177,156, ,18.1,0.16, -,232,<16.9>,1.25,589, 3 2, [Xe]4f¹³5d6s², HEX,3.54
+Ytterbium, Yb,70,173.04,6.9654,1097,1466,194, -, ,24.8,0.145,3.35,159,<34.9>,1.1,603, 3 2, [Xe]4f¹5d¹6s², FCC,5.49
+Lutetium, Lu,71,174.967,9.8404,1936,3668,175,156, ,17.8,0.155, -,414,<16.4>,1.27,513,3, [Xe]4f¹5d¹6s², HEX,3.51
+Hafnium, Hf,72,178.49,13.31,2503,5470,167,144, ,13.6,0.146,-25.1,575,23,1.3,575.2,4, [Xe]4f¹5d²6s², HEX,3.2
+Tantalum, Ta,73,180.9479,16.654,3269,5698,149,134, ,10.9,0.14,24.7,758,57.5,1.5,760.1,5, [Xe]4f¹5d³6s², BCC,3.31
+Tungsten, W,74,183.84,19.3,3680,5930,141,130, ,9.53,0.133,-35,824,173,1.7,769.7, 6 5 4 3 2 0, [Xe]4f¹5d6s², BCC,3.16
+Rhenium, Re,75,186.207,21.02,3453,5900,137,128, ,8.85,0.138,34,704,48,1.9,759.1, 5 4 3 2 -1, [Xe]4f¹5d6s², HEX,2.76
+Osmium, Os,76,190.23,22.57,3327,5300,135,126, ,8.43,0.131,31.7,738,<87.6>,2.2,819.8, 8 6 4 3 2 0 -2, [Xe]4f¹5d6s², HEX,2.74
+Iridium, Ir,77,192.22,22.42,2683,4403,136,127, ,8.54,0.133,27.61,604,147,2.2,868.1, 6 4 3 2 1 0 -1, [Xe]4f¹5d6s², FCC,3.84
+Platinum, Pt,78,195.08,21.45,2045,4100,139,130, ,9.1,0.133,21.76, ~470,71.6,2.28,868.1, 4 2 0, [Xe]4f¹5d6s², FCC,3.92
+Gold, Au,79,196.96654,19.3,1337.58,3080,146,134, ,10.2,0.129,12.68, ~340,318,2.54,889.3, 3 1, [Xe]4f¹5d¹6s², FCC,4.08
+Mercury, Hg,80,200.59, 13.546 (@ +20degC),234.28,629.73,157,149, ,14.8,0.138,2.295,58.5,8.3,2,1006, 2 1, [Xe]4f¹5d¹6s², RHL,2.99
+Thallium, Tl,81,204.3833,11.85,576.6,1730,171,148, ,17.2,0.128,4.31,162.4,46.1,1.62,588.9, 3 1, [Xe]4f¹5d¹6s²6p¹, HEX,3.46
+Lead, Pb,82,207.2,11.35,600.65,2013,175,147, ,18.3,0.159,4.77,177.8,35.3,1.8,715.2, 4 2, [Xe]4f¹5d¹6s²6p², FCC,4.95
+Bismuth, Bi,83,208.98037,9.747,544.5,1883,170,146, ,21.3,0.124,11,172,7.9,2.02,702.9, 5 3, [Xe]4f¹5d¹6s²6p³, RHL,4.75
+Polonium, Po,84,208.9824,9.32,527,1235,176,146, ,22.7,0.125,-10,-102.9, -,2,813.1, 6 4 2, [Xe]4f¹5d¹6s²6p, SC,3.35
+Astatine, At,85,209.9871, -,575,610, -,<145>, , -, -, -, -, -,2.2,916.3, 7 5 3 1 -1, [Xe]4f¹5d¹6s²6p, -, -
+Radon, Rn,86,222.0176, 4.4 (@ -62degC),202,211.4, -, -, , -,0.094, -,18.1,0.0036, -,1036.5, -, [Xe]4f¹5d¹6s²6p, FCC, -
+Francium, Fr,87,223.0197, -,300,950, -, -, , -, -,15, -, -,0.7, ~375,2, [Rn]7s¹, BCC, -
+Radium, Ra,88,226.0254,<5.5>,973,1413, -, -, ,45,0.12,-9.6,-113,<18.6>,0.9,509,2, [Rn]7s², -, -
+Actinium, Ac,89,227.0278, -,1320,3470,188, -, ,22.54, -,-10.5,-292.9, -,1.1,665.5,3, [Rn]6d¹7s², FCC,5.31
+Thorium, Th,90,232.0381,11.78,2028,5060,180,165, ,19.8,0.113,16.11,513.7,<54>,1.3,670.4,4, [Rn]5f6d¹7s², FCC,5.08
+Protactinium, Pa,91,231.03588,15.37,2113,4300,161, -, ,15,0.121,16.7,481.2, -,1.5, -, 5 4, [Rn]5f²6d¹7s², TET,3.92
+Uranium, U,92,238.0289,19.05,1405.5,4018,138,142, ,12.5,0.115,12.6,417,27.5,1.38,686.4, 6 5 4 3, [Rn]5f³6d¹7s², ORC,2.85
+Neptunium, Np,93,237.048,20.25,913,4175,130, -, ,21.1, -,-9.6,336,<6.3>,1.36, -, 6 5 4 3, [Rn]5f6d¹7s², ORC,4.72
+Plutonium, Pu,94,244.0642,19.84,914,3505,151, -, , -, -,2.8,343.5,<6.7>,1.28,491.9, 6 5 4 3, [Rn]5f6d7s², MCL, -
+Americium, Am,95,243.0614,13.67,1267,2880,173, -, ,20.8, -,-10,238.5, -,1.3, -, 6 5 4 3, [Rn]5f6d7s², -, -
+Curium, Cm,96,247.0703,13.51,1340, -,299, -, ,18.28, -, -, -, -,1.3,<580>, 4 3, [Rn]5f6d¹7s², -, -
+Berkelium, Bk,97,247.0703,13.25, -, -,297, -, , -, -, -, -, -,1.3,<600>, 4 3, [Rn]5f6d7s², -, -
+Californium, Cf,98,251.0796,15.1,900, -,295, -, , -, -, -, -, -,1.3,<610>, 4 3, [Rn]5f¹6d7s², -, -
+Einsteinium, Es,99,252.083, -, -,1130,292, -, , -, -, -, -, -,1.3,<620>,3, [Rn]5f¹¹6d7s², -, -
+Fermium, Fm,100,257.0951, -,1800, -,290, -, , -, -, -, -, -,1.3,<630>,3, [Rn]5f¹²6d7s², -, -
+Mendelevium, Md,101,258.1, -,1100, -,287, -, , -, -, -, -, -,1.3,<635>,3, [Rn]5f¹³6d7s², -, -
+Nobelium, No,102,259.1009, -,1100, -,285, -, , -, -, -, -, -,1.3,<640>,32, [Rn]5f¹6d7s², -, -
+Lawrencium, Lr,103,262.11, -, -, -,282, -, , -, -, -, -, -, -, -,3, [Rn]5f¹6d¹7s², -, -
+Rutherfordium, Rf,104, [261], -, -, -, -, -, , -, -, -, -, -, -, -, -, [Rn]5f¹6d²7s², -, -
+Dubnium, Db,105, [262], -, -, -, -, -, , -, -, -, -, -, -, -, -, [Rn]5f¹6d³6s², -, -
+Seaborgium, Sg,106, [266], -, -, -, -, -, , -, -, -, -, -, -, -, -, [Rn]5f¹6d¹7s², -, -
+Bohrium, Bh,107, [264], -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Hassium, Hs,108, [269], -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Meitnerium, Mt,109, [268], -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Ununnilium, Uun,110, [269], -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Unununium, Uuu,111, [272], -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Ununbium, Uub,112, [277], -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Ununtrium, Uut,113, -, -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Ununquadium, Uuq,114, [289], -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Ununpentium, Uup,115, -, -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Ununhexium, Uuh,116, -, -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Ununseptium, Uus,117, -, -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
+Ununoctium, Uuo,118, -, -, -, -, -, -, , -, -, -, -, -, -, -, -, -, -, -
\ No newline at end of file