From 177ff99d001f5fbeb30a237c7e8a538b469a6a93 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Tue, 4 Apr 2023 16:13:20 +0200 Subject: [PATCH] Minor updates to FormaleSprachen.ipynb --- info4/kapitel-1/FormaleSprachen.ipynb | 680 ++++++++++++++------------ 1 file changed, 356 insertions(+), 324 deletions(-) diff --git a/info4/kapitel-1/FormaleSprachen.ipynb b/info4/kapitel-1/FormaleSprachen.ipynb index 44a9b80..9ae3942 100644 --- a/info4/kapitel-1/FormaleSprachen.ipynb +++ b/info4/kapitel-1/FormaleSprachen.ipynb @@ -38,7 +38,7 @@ "source": [ "Ein Wort ist eine endliche Folge von Elementen aus dem Alphabet.\n", "Im Skript schreiben wir $w \\in \\Sigma^{*}$; hier im Notebook schreiben wir\n", - "$w \\in seq(\\Sigma)$.\n", + "$w \\in \\mathrm{seq}(\\Sigma)$.\n", "\n", "Im Skript schreiben wir Wörter in dem wir die Symbole aus $\\Sigma$ hintereinander setzten: $abc$. Im Notebook schreiben wir $[a,b,c]$ für die Folge mit den drei Symbolen $a$, $b$ und $c$.\n", "\n", @@ -95,7 +95,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Die Länge eines Wortes $w$ ist die Anzahl der Symbole in $w$. Im Skript schreiben wir $|w|$, im Notebook benutzen wir ```size(w)```:" + "Die Länge eines Wortes $w$ ist die Anzahl der Symbole in $w$. Im Skript schreiben wir $|w|$, im Notebook benutzen wir $\\mathrm{size}(w)$:" ] }, { @@ -162,7 +162,7 @@ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $ε = \\emptyset$" + "* $\\mathit{ε} = \\emptyset$" ], "text/plain": [ "TRUE\n", @@ -184,7 +184,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Leider ist in der B Sprache das Symbol λ schon vergeben (zur Definition von Funktionen). Deshalb müssen wir in einer weiteren Abweichung vom Skript Epsilon verwenden.\n", + "Leider ist in der B-Sprache das Symbol $\\lambda$ schon vergeben (zur Definition von Funktionen). Deshalb müssen wir in einer weiteren Abweichung vom Skript Epsilon verwenden.\n", "\n", "Eine formale Sprache ist eine jede Teilmenge von $\\Sigma^*$." ] @@ -200,7 +200,7 @@ "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $\\mathit{Sprachen} = \\{\\mathit{L}\\mid \\mathit{L} \\subseteq \\mathit{seq}(Σ)\\}$" + "* $\\mathit{Sprachen} = \\{\\mathit{L}\\mid\\mathit{L} \\subseteq \\mathit{seq}(\\mathit{Σ})\\}$" ], "text/plain": [ "TRUE\n", @@ -222,7 +222,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "In folgender B Maschine werden wir ein paar Sprachen und Wörter definieren:" + "In folgender B-Maschine werden wir ein paar Sprachen und Wörter definieren:" ] }, { @@ -247,12 +247,12 @@ "SETS Σ = {a,b,c}\n", "CONSTANTS ε, Sprachen, w₁, w₂, L₁, L₂\n", "PROPERTIES \n", - " ε ∈ seq(Σ) ∧ size(ε) = 0 ∧\n", - " Sprachen = {L | L ⊆ seq(Σ)}∧\n", - " w₁ = [a,a,b,c] ∧\n", - " w₂ = [c,c] ∧\n", - " L₁ = {w₁,w₂} ∧\n", - " L₂ = {w₂, [a,a,a] }\n", + " ε ∈ seq(Σ) ∧ size(ε) = 0 ∧\n", + " Sprachen = {L | L ⊆ seq(Σ)} ∧\n", + " w₁ = [a,a,b,c] ∧\n", + " w₂ = [c,c] ∧\n", + " L₁ = {w₁,w₂} ∧\n", + " L₂ = {w₂, [a,a,a]}\n", "END" ] }, @@ -264,7 +264,7 @@ { "data": { "text/plain": [ - "Machine constants set up using operation 0: $setup_constants()" + "Executed operation: SETUP_CONSTANTS()" ] }, "execution_count": 9, @@ -284,7 +284,7 @@ { "data": { "text/markdown": [ - "$\\{(1\\mapsto \\mathit{a}),(2\\mapsto \\mathit{a}),(3\\mapsto \\mathit{b}),(4\\mapsto \\mathit{c})\\}$" + "$\\{(1\\mapsto\\mathit{a}),(2\\mapsto\\mathit{a}),(3\\mapsto\\mathit{b}),(4\\mapsto\\mathit{c})\\}$" ], "text/plain": [ "{(1↦a),(2↦a),(3↦b),(4↦c)}" @@ -334,7 +334,7 @@ { "data": { "text/markdown": [ - "$[a,\\mathit{a},\\mathit{b},c]$" + "$[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]$" ], "text/plain": [ "[a,a,b,c]" @@ -364,7 +364,7 @@ { "data": { "text/markdown": [ - "$[c,c]$" + "$[\\mathit{c},\\mathit{c}]$" ], "text/plain": [ "[c,c]" @@ -387,7 +387,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\}$" + "$\\{[\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c],[a,a,b,c]}" @@ -435,7 +435,7 @@ } ], "source": [ - "LeereSprache = ∅ ∧ LeereSprache ≠ {ε}" + "LeereSprache = ∅ ∧ LeereSprache ≠ {ε}" ] }, { @@ -488,7 +488,7 @@ } ], "source": [ - "card( {ε} )" + "card({ε})" ] }, { @@ -511,7 +511,7 @@ } ], "source": [ - "card( ∅ )" + "card(∅)" ] }, { @@ -529,7 +529,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\}$" + "$\\{[\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c],[a,a,b,c]}" @@ -552,7 +552,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c],[a,\\mathit{a},a]\\}$" + "$\\{[\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{a}]\\}$" ], "text/plain": [ "{[c,c],[a,a,a]}" @@ -575,7 +575,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c],[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c]\\}$" + "$\\{[\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{a}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c],[a,a,a],[a,a,b,c]}" @@ -598,7 +598,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c],[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c]\\}$" + "$\\{[\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{a}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c],[a,a,a],[a,a,b,c]}" @@ -610,7 +610,7 @@ } ], "source": [ - "{x| x∈seq(Σ) ∧ (x∈L₁ ∨ x∈L₂)}" + "{x | x∈seq(Σ) ∧ (x∈L₁ ∨ x∈L₂)}" ] }, { @@ -621,7 +621,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c]\\}$" + "$\\{[\\mathit{c},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c]}" @@ -644,7 +644,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c]\\}$" + "$\\{[\\mathit{c},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c]}" @@ -656,7 +656,7 @@ } ], "source": [ - "{x| x∈seq(Σ) ∧ (x∈L₁ ∧ x∈L₂)}" + "{x | x∈seq(Σ) ∧ (x∈L₁ ∧ x∈L₂)}" ] }, { @@ -667,7 +667,7 @@ { "data": { "text/markdown": [ - "$\\{[a,\\mathit{a},\\mathit{b},c]\\}$" + "$\\{[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[a,a,b,c]}" @@ -690,7 +690,7 @@ { "data": { "text/markdown": [ - "$\\{[a,\\mathit{a},a]\\}$" + "$\\{[\\mathit{a},\\mathit{a},\\mathit{a}]\\}$" ], "text/plain": [ "{[a,a,a]}" @@ -716,7 +716,7 @@ "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $\\mathit{Komplement} = (\\mathit{seq}(Σ) - \\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\})$" + "* $\\mathit{Komplement} = (\\mathit{seq}(\\mathit{Σ}) - \\{[\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\})$" ], "text/plain": [ "TRUE\n", @@ -751,7 +751,7 @@ { "data": { "text/markdown": [ - "$[a,\\mathit{a},\\mathit{b},c]$" + "$[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]$" ], "text/plain": [ "[a,a,b,c]" @@ -774,7 +774,7 @@ { "data": { "text/markdown": [ - "$[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c]$" + "$[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]$" ], "text/plain": [ "[a,a,b,c,a,a,b,c]" @@ -797,7 +797,7 @@ { "data": { "text/markdown": [ - "$[a,\\mathit{a},\\mathit{b},c]$" + "$[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]$" ], "text/plain": [ "[a,a,b,c]" @@ -820,7 +820,7 @@ { "data": { "text/markdown": [ - "$[a,\\mathit{a},\\mathit{b},c]$" + "$[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]$" ], "text/plain": [ "[a,a,b,c]" @@ -850,7 +850,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\}$" + "$\\{[\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c],[a,a,b,c]}" @@ -873,7 +873,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c],[a,\\mathit{a},a]\\}$" + "$\\{[\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{a}]\\}$" ], "text/plain": [ "{[c,c],[a,a,a]}" @@ -896,7 +896,7 @@ { "data": { "text/markdown": [ - "$\\{[c,\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},a],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},a]\\}$" + "$\\{[\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{a}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{a}]\\}$" ], "text/plain": [ "{[c,c,c,c],[c,c,a,a,a],[a,a,b,c,c,c],[a,a,b,c,a,a,a]}" @@ -908,7 +908,7 @@ } ], "source": [ - " {w | ∃(a,b).(a∈L₁ ∧ b∈L₂ ∧ w = a^b)}" + "{w | ∃(a,b).(a∈L₁ ∧ b∈L₂ ∧ w = a^b)}" ] }, { @@ -927,7 +927,7 @@ { "data": { "text/markdown": [ - "$\\{[c,\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c]\\}$" + "$\\{[\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c,c,c],[c,c,a,a,b,c],[a,a,b,c,c,c],[a,a,b,c,a,a,b,c]}" @@ -958,7 +958,7 @@ { "data": { "text/markdown": [ - "$\\{[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c]\\}$" + "$\\{[\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c,c,c,c,c],[c,c,a,a,b,c,c,c],[a,a,b,c,c,c,c,c],[c,c,c,c,a,a,b,c],[a,a,b,c,a,a,b,c,c,c],[c,c,a,a,b,c,a,a,b,c],[a,a,b,c,c,c,a,a,b,c],[a,a,b,c,a,a,b,c,a,a,b,c]}" @@ -981,7 +981,7 @@ { "data": { "text/markdown": [ - "$\\{[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c]\\}$" + "$\\{[\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[c,c,c,c,c,c,c,c],[c,c,c,c,a,a,b,c,c,c],[c,c,a,a,b,c,c,c,c,c],[a,a,b,c,c,c,c,c,c,c],[c,c,c,c,c,c,a,a,b,c],[a,a,b,c,a,a,b,c,c,c,c,c],[c,c,c,c,a,a,b,c,a,a,b,c],[c,c,a,a,b,c,c,c,a,a,b,c],[c,c,a,a,b,c,a,a,b,c,c,c],[a,a,b,c,c,c,c,c,a,a,b,c],[a,a,b,c,c,c,a,a,b,c,c,c],[c,c,a,a,b,c,a,a,b,c,a,a,b,c],[a,a,b,c,c,c,a,a,b,c,a,a,b,c],[a,a,b,c,a,a,b,c,c,c,a,a,b,c],[a,a,b,c,a,a,b,c,a,a,b,c,c,c],[a,a,b,c,a,a,b,c,a,a,b,c,a,a,b,c]}" @@ -1027,7 +1027,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Die Spiegelung eines Wortes kann im Notebook mit dem ```rev``` Operator verwirklicht werden:" + "Die Spiegelung eines Wortes kann im Notebook mit dem Operator `rev` verwirklicht werden:" ] }, { @@ -1038,7 +1038,7 @@ { "data": { "text/markdown": [ - "$[c,\\mathit{b},\\mathit{a},a]$" + "$[\\mathit{c},\\mathit{b},\\mathit{a},\\mathit{a}]$" ], "text/plain": [ "[c,b,a,a]" @@ -1068,7 +1068,7 @@ { "data": { "text/markdown": [ - "$\\{[c,c],[c,\\mathit{b},\\mathit{a},a]\\}$" + "$\\{[\\mathit{c},\\mathit{c}],[\\mathit{c},\\mathit{b},\\mathit{a},\\mathit{a}]\\}$" ], "text/plain": [ "{[c,c],[c,b,a,a]}" @@ -1087,7 +1087,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Die Teilwort und Präfix Relationen definieren wir in folgender B Maschine:" + "Die Teilwort- und Präfix-Relationen definieren wir in folgender B-Maschine:" ] }, { @@ -1112,16 +1112,16 @@ "SETS Sigma = {a,b,c}\n", "CONSTANTS ε, Sprachen, w₁, w₂, L₁, L₂\n", "ABSTRACT_CONSTANTS\n", - " teilwort, präfix\n", + " teilwort, präfix\n", "PROPERTIES \n", - " ε ∈ seq(Sigma) ∧ size(ε) = 0 ∧\n", - " Sprachen = {L | L ⊆ seq(Sigma)}∧\n", - " w₁ = [a,a,b,c] ∧\n", - " w₂ = [c,a,b,a] ∧\n", - " L₁ = {w₁,w₂} ∧\n", - " L₂ = {w₂, [a,a,a] } ∧\n", - " teilwort = {ut,vt | ut∈seq(Sigma) & vt∈seq(Sigma) ∧ ∃(vt1,vt2).(vt1^ut^vt2 = vt)} ∧\n", - " präfix = {up,vp | up∈seq(Sigma) & vp∈seq(Sigma) ∧ ∃(wp).(up^wp = vp)}\n", + " ε ∈ seq(Sigma) ∧ size(ε) = 0 ∧\n", + " Sprachen = {L | L ⊆ seq(Sigma)}∧\n", + " w₁ = [a,a,b,c] ∧\n", + " w₂ = [c,a,b,a] ∧\n", + " L₁ = {w₁,w₂} ∧\n", + " L₂ = {w₂, [a,a,a]} ∧\n", + " teilwort = {ut,vt | ut∈seq(Sigma) & vt∈seq(Sigma) ∧ ∃(vt1,vt2).(vt1^ut^vt2 = vt)} ∧\n", + " präfix = {up,vp | up∈seq(Sigma) & vp∈seq(Sigma) ∧ ∃(wp).(up^wp = vp)}\n", "DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE\n", "END" ] @@ -1134,7 +1134,7 @@ { "data": { "text/plain": [ - "Machine constants set up using operation 0: $setup_constants()" + "Executed operation: SETUP_CONSTANTS()" ] }, "execution_count": 44, @@ -1230,7 +1230,7 @@ { "data": { "text/markdown": [ - "$\\{[],[c],[c,b],[c,\\mathit{b},a],[c,\\mathit{b},\\mathit{a},a],[c,\\mathit{b},\\mathit{a},\\mathit{a},b]\\}$" + "$\\{[],[\\mathit{c}],[\\mathit{c},\\mathit{b}],[\\mathit{c},\\mathit{b},\\mathit{a}],[\\mathit{c},\\mathit{b},\\mathit{a},\\mathit{a}],[\\mathit{c},\\mathit{b},\\mathit{a},\\mathit{a},\\mathit{b}]\\}$" ], "text/plain": [ "{[],[c],[c,b],[c,b,a],[c,b,a,a],[c,b,a,a,b]}" @@ -1253,7 +1253,7 @@ { "data": { "text/markdown": [ - "$\\{[],[a],[a,a],[a,b],[b],[b,a],[c],[c,b],[a,\\mathit{a},b],[b,\\mathit{a},a],[b,\\mathit{a},\\mathit{a},b],[c,\\mathit{b},a],[c,\\mathit{b},\\mathit{a},a],[c,\\mathit{b},\\mathit{a},\\mathit{a},b]\\}$" + "$\\{[],[\\mathit{a}],[\\mathit{a},\\mathit{a}],[\\mathit{a},\\mathit{b}],[\\mathit{b}],[\\mathit{b},\\mathit{a}],[\\mathit{c}],[\\mathit{c},\\mathit{b}],[\\mathit{a},\\mathit{a},\\mathit{b}],[\\mathit{b},\\mathit{a},\\mathit{a}],[\\mathit{b},\\mathit{a},\\mathit{a},\\mathit{b}],[\\mathit{c},\\mathit{b},\\mathit{a}],[\\mathit{c},\\mathit{b},\\mathit{a},\\mathit{a}],[\\mathit{c},\\mathit{b},\\mathit{a},\\mathit{a},\\mathit{b}]\\}$" ], "text/plain": [ "{[],[a],[a,a],[a,b],[b],[b,a],[c],[c,b],[a,a,b],[b,a,a],[b,a,a,b],[c,b,a],[c,b,a,a],[c,b,a,a,b]}" @@ -1276,7 +1276,7 @@ { "data": { "text/markdown": [ - "$\\{[],[a],[a,b],[b],[b,c],[c],[a,\\mathit{b},c]\\}$" + "$\\{[],[\\mathit{a}],[\\mathit{a},\\mathit{b}],[\\mathit{b}],[\\mathit{b},\\mathit{c}],[\\mathit{c}],[\\mathit{a},\\mathit{b},\\mathit{c}]\\}$" ], "text/plain": [ "{[],[a],[a,b],[b],[b,c],[c],[a,b,c]}" @@ -1322,215 +1322,217 @@ "<?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.44.1 (0)\n", + "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n", " -->\n", "<!-- Title: state Pages: 1 -->\n", - "<svg width=\"441pt\" height=\"305pt\"\n", - " viewBox=\"0.00 0.00 440.61 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "<svg width=\"416pt\" height=\"305pt\"\n", + " viewBox=\"0.00 0.00 415.73 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n", "<title>state</title>\n", - "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-301 436.61,-301 436.61,4 -4,4\"/>\n", + "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 411.73,-301 411.73,4 -4,4\"/>\n", "<!-- [a,b,c] -->\n", "<g id=\"node1\" class=\"node\">\n", "<title>[a,b,c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"213.11,-36 152.11,-36 152.11,0 213.11,0 213.11,-36\"/>\n", - "<text text-anchor=\"middle\" x=\"182.61\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,c]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"200.73,-36 146.73,-36 146.73,0 200.73,0 200.73,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"173.73\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,c]</text>\n", "</g>\n", "<!-- [a,b,c]->[a,b,c] -->\n", "<g id=\"edge1\" class=\"edge\">\n", "<title>[a,b,c]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M213.39,-25.87C223.28,-25.79 231.11,-23.17 231.11,-18 231.11,-14.77 228.05,-12.53 223.34,-11.29\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"223.73,-7.81 213.39,-10.13 222.92,-14.77 223.73,-7.81\"/>\n", - "<text text-anchor=\"middle\" x=\"240.61\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M200.98,-26.15C210.76,-26.32 218.73,-23.61 218.73,-18 218.73,-14.85 216.21,-12.61 212.26,-11.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"212.84,-7.83 202.48,-10.04 211.96,-14.77 212.84,-7.83\"/>\n", + "<text text-anchor=\"middle\" x=\"225.73\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [c] -->\n", "<g id=\"node2\" class=\"node\">\n", "<title>[c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"67.61,-210 13.61,-210 13.61,-174 67.61,-174 67.61,-210\"/>\n", - "<text text-anchor=\"middle\" x=\"40.61\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[c]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"67.73,-210 13.73,-210 13.73,-174 67.73,-174 67.73,-210\"/>\n", + "<text text-anchor=\"middle\" x=\"40.73\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[c]</text>\n", "</g>\n", "<!-- [c]->[a,b,c] -->\n", "<g id=\"edge2\" class=\"edge\">\n", "<title>[c]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M38,-173.85C35.59,-151.75 34.7,-113.07 52.61,-87 73.53,-56.54 112.5,-38.76 142.33,-29.08\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"143.53,-32.37 152.06,-26.1 141.48,-25.68 143.53,-32.37\"/>\n", - "<text text-anchor=\"middle\" x=\"62.11\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M38.21,-173.55C35.96,-151.47 35.32,-113.18 52.73,-87 71.99,-58.04 108,-40.12 135.75,-29.99\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"136.55,-33.42 144.87,-26.86 134.28,-26.8 136.55,-33.42\"/>\n", + "<text text-anchor=\"middle\" x=\"59.73\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [c]->[c] -->\n", "<g id=\"edge3\" class=\"edge\">\n", "<title>[c]->[c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M67.85,-199.87C77.63,-200.04 85.61,-197.41 85.61,-192 85.61,-188.7 82.65,-186.44 78.12,-185.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"78.16,-181.7 67.85,-184.13 77.43,-188.66 78.16,-181.7\"/>\n", - "<text text-anchor=\"middle\" x=\"95.11\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M67.98,-200.15C77.76,-200.32 85.73,-197.61 85.73,-192 85.73,-188.85 83.21,-186.61 79.26,-185.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"79.84,-181.83 69.48,-184.04 78.96,-188.77 79.84,-181.83\"/>\n", + "<text text-anchor=\"middle\" x=\"92.73\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [b,c] -->\n", "<g id=\"node3\" class=\"node\">\n", "<title>[b,c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"134.61,-123 80.61,-123 80.61,-87 134.61,-87 134.61,-123\"/>\n", - "<text text-anchor=\"middle\" x=\"107.61\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[b,c]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"129.73,-123 75.73,-123 75.73,-87 129.73,-87 129.73,-123\"/>\n", + "<text text-anchor=\"middle\" x=\"102.73\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[b,c]</text>\n", "</g>\n", "<!-- [c]->[b,c] -->\n", "<g id=\"edge4\" class=\"edge\">\n", "<title>[c]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M54.17,-173.8C63.79,-161.59 76.87,-144.99 87.68,-131.28\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"90.63,-133.2 94.07,-123.18 85.13,-128.86 90.63,-133.2\"/>\n", - "<text text-anchor=\"middle\" x=\"87.11\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M53.28,-173.8C61.88,-162.01 73.46,-146.14 83.25,-132.72\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"86.04,-134.83 89.1,-124.69 80.38,-130.71 86.04,-134.83\"/>\n", + "<text text-anchor=\"middle\" x=\"81.73\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [b,c]->[a,b,c] -->\n", "<g id=\"edge5\" class=\"edge\">\n", "<title>[b,c]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M122.79,-86.8C133.66,-74.47 148.48,-57.68 160.65,-43.89\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"163.46,-45.99 167.45,-36.18 158.21,-41.36 163.46,-45.99\"/>\n", - "<text text-anchor=\"middle\" x=\"158.11\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M117.1,-86.8C127.14,-74.78 140.72,-58.52 152.07,-44.94\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"154.45,-47.55 158.17,-37.63 149.08,-43.06 154.45,-47.55\"/>\n", + "<text text-anchor=\"middle\" x=\"148.73\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [b,c]->[b,c] -->\n", "<g id=\"edge6\" class=\"edge\">\n", "<title>[b,c]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M134.85,-112.87C144.63,-113.04 152.61,-110.41 152.61,-105 152.61,-101.7 149.65,-99.44 145.12,-98.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"145.16,-94.7 134.85,-97.13 144.43,-101.66 145.16,-94.7\"/>\n", - "<text text-anchor=\"middle\" x=\"162.11\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M129.98,-113.15C139.76,-113.32 147.73,-110.61 147.73,-105 147.73,-101.85 145.21,-99.61 141.26,-98.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"141.84,-94.83 131.48,-97.04 140.96,-101.77 141.84,-94.83\"/>\n", + "<text text-anchor=\"middle\" x=\"154.73\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [b] -->\n", "<g id=\"node4\" class=\"node\">\n", "<title>[b]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"231.61,-210 177.61,-210 177.61,-174 231.61,-174 231.61,-210\"/>\n", - "<text text-anchor=\"middle\" x=\"204.61\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[b]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"221.73,-210 167.73,-210 167.73,-174 221.73,-174 221.73,-210\"/>\n", + "<text text-anchor=\"middle\" x=\"194.73\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[b]</text>\n", "</g>\n", "<!-- [b]->[a,b,c] -->\n", "<g id=\"edge7\" class=\"edge\">\n", "<title>[b]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M202.42,-173.88C198.6,-144 190.68,-82.11 186.1,-46.27\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"189.53,-45.53 184.79,-36.05 182.59,-46.41 189.53,-45.53\"/>\n", - "<text text-anchor=\"middle\" x=\"205.11\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M192.61,-173.56C188.99,-143.94 181.61,-83.54 177.23,-47.64\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"180.74,-47.49 176.05,-37.99 173.79,-48.34 180.74,-47.49\"/>\n", + "<text text-anchor=\"middle\" x=\"192.73\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [b]->[b,c] -->\n", "<g id=\"edge8\" class=\"edge\">\n", "<title>[b]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M187.28,-173.95C177.09,-164.1 163.84,-151.6 151.61,-141 147.17,-137.15 142.38,-133.18 137.66,-129.35\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"139.83,-126.61 129.84,-123.09 135.46,-132.07 139.83,-126.61\"/>\n", - "<text text-anchor=\"middle\" x=\"177.11\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M179.27,-173.78C170.12,-163.87 158.12,-151.37 146.73,-141 142.79,-137.41 138.53,-133.76 134.26,-130.23\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"136.76,-127.75 126.78,-124.19 132.36,-133.2 136.76,-127.75\"/>\n", + "<text text-anchor=\"middle\" x=\"168.73\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [b]->[b] -->\n", "<g id=\"edge9\" class=\"edge\">\n", "<title>[b]->[b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M231.85,-199.87C241.63,-200.04 249.61,-197.41 249.61,-192 249.61,-188.7 246.65,-186.44 242.12,-185.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"242.16,-181.7 231.85,-184.13 241.43,-188.66 242.16,-181.7\"/>\n", - "<text text-anchor=\"middle\" x=\"259.11\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M221.98,-200.15C231.76,-200.32 239.73,-197.61 239.73,-192 239.73,-188.85 237.21,-186.61 233.26,-185.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"233.84,-181.83 223.48,-184.04 232.96,-188.77 233.84,-181.83\"/>\n", + "<text text-anchor=\"middle\" x=\"246.73\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [a,b] -->\n", "<g id=\"node5\" class=\"node\">\n", "<title>[a,b]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"298.61,-123 244.61,-123 244.61,-87 298.61,-87 298.61,-123\"/>\n", - "<text text-anchor=\"middle\" x=\"271.61\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"283.73,-123 229.73,-123 229.73,-87 283.73,-87 283.73,-123\"/>\n", + "<text text-anchor=\"middle\" x=\"256.73\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\n", "</g>\n", "<!-- [b]->[a,b] -->\n", "<g id=\"edge10\" class=\"edge\">\n", "<title>[b]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M218.17,-173.8C227.79,-161.59 240.87,-144.99 251.68,-131.28\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"254.63,-133.2 258.07,-123.18 249.13,-128.86 254.63,-133.2\"/>\n", - "<text text-anchor=\"middle\" x=\"251.11\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M207.28,-173.8C215.88,-162.01 227.46,-146.14 237.25,-132.72\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"240.04,-134.83 243.1,-124.69 234.38,-130.71 240.04,-134.83\"/>\n", + "<text text-anchor=\"middle\" x=\"235.73\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [a,b]->[a,b,c] -->\n", "<g id=\"edge11\" class=\"edge\">\n", "<title>[a,b]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M254.71,-86.64C245.12,-76.92 232.84,-64.64 221.61,-54 217.82,-50.42 213.78,-46.68 209.79,-43.05\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"212.01,-40.34 202.24,-36.24 207.32,-45.54 212.01,-40.34\"/>\n", - "<text text-anchor=\"middle\" x=\"246.11\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M241.71,-86.51C233.14,-76.74 222.08,-64.46 211.73,-54 208.56,-50.79 205.17,-47.49 201.76,-44.26\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"204.21,-41.75 194.5,-37.49 199.43,-46.87 204.21,-41.75\"/>\n", + "<text text-anchor=\"middle\" x=\"232.73\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [a,b]->[a,b] -->\n", "<g id=\"edge12\" class=\"edge\">\n", "<title>[a,b]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M298.85,-112.87C308.63,-113.04 316.61,-110.41 316.61,-105 316.61,-101.7 313.65,-99.44 309.12,-98.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"309.16,-94.7 298.85,-97.13 308.43,-101.66 309.16,-94.7\"/>\n", - "<text text-anchor=\"middle\" x=\"326.11\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M283.98,-113.15C293.76,-113.32 301.73,-110.61 301.73,-105 301.73,-101.85 299.21,-99.61 295.26,-98.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"295.84,-94.83 285.48,-97.04 294.96,-101.77 295.84,-94.83\"/>\n", + "<text text-anchor=\"middle\" x=\"308.73\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [a] -->\n", "<g id=\"node6\" class=\"node\">\n", "<title>[a]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"395.61,-210 341.61,-210 341.61,-174 395.61,-174 395.61,-210\"/>\n", - "<text text-anchor=\"middle\" x=\"368.61\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"375.73,-210 321.73,-210 321.73,-174 375.73,-174 375.73,-210\"/>\n", + "<text text-anchor=\"middle\" x=\"348.73\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a]</text>\n", "</g>\n", "<!-- [a]->[a,b,c] -->\n", "<g id=\"edge13\" class=\"edge\">\n", "<title>[a]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M369.2,-173.8C369.04,-151.29 365.5,-111.8 344.61,-87 313.89,-50.54 260.29,-33.25 223.2,-25.32\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"223.7,-21.85 213.21,-23.32 222.33,-28.71 223.7,-21.85\"/>\n", - "<text text-anchor=\"middle\" x=\"371.11\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M349.23,-173.88C348.97,-151.46 345.31,-112.07 324.73,-87 296.38,-52.46 246.8,-34.79 212.21,-26.24\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"213.11,-22.86 202.58,-24.02 211.54,-29.68 213.11,-22.86\"/>\n", + "<text text-anchor=\"middle\" x=\"348.73\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [a]->[a,b] -->\n", "<g id=\"edge14\" class=\"edge\">\n", "<title>[a]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M351.28,-173.95C341.09,-164.1 327.84,-151.6 315.61,-141 311.17,-137.15 306.38,-133.18 301.66,-129.35\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"303.83,-126.61 293.84,-123.09 299.46,-132.07 303.83,-126.61\"/>\n", - "<text text-anchor=\"middle\" x=\"341.11\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M333.27,-173.78C324.12,-163.87 312.12,-151.37 300.73,-141 296.79,-137.41 292.53,-133.76 288.26,-130.23\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"290.76,-127.75 280.78,-124.19 286.36,-133.2 290.76,-127.75\"/>\n", + "<text text-anchor=\"middle\" x=\"322.73\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [a]->[a] -->\n", "<g id=\"edge15\" class=\"edge\">\n", "<title>[a]->[a]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M395.85,-199.87C405.63,-200.04 413.61,-197.41 413.61,-192 413.61,-188.7 410.65,-186.44 406.12,-185.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"406.16,-181.7 395.85,-184.13 405.43,-188.66 406.16,-181.7\"/>\n", - "<text text-anchor=\"middle\" x=\"423.11\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M375.98,-200.15C385.76,-200.32 393.73,-197.61 393.73,-192 393.73,-188.85 391.21,-186.61 387.26,-185.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"387.84,-181.83 377.48,-184.04 386.96,-188.77 387.84,-181.83\"/>\n", + "<text text-anchor=\"middle\" x=\"400.73\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- [] -->\n", "<g id=\"node7\" class=\"node\">\n", "<title>[]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"199.61,-297 145.61,-297 145.61,-261 199.61,-261 199.61,-297\"/>\n", - "<text text-anchor=\"middle\" x=\"172.61\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"191.73,-297 137.73,-297 137.73,-261 191.73,-261 191.73,-297\"/>\n", + "<text text-anchor=\"middle\" x=\"164.73\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n", "</g>\n", "<!-- []->[a,b,c] -->\n", "<g id=\"edge16\" class=\"edge\">\n", "<title>[]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M145.58,-276.1C106.63,-271.73 35.98,-257.34 4.61,-210 -4.23,-196.66 2.48,-189.86 4.61,-174 12.55,-114.7 14.72,-85.46 65.61,-54 88.86,-39.63 118.36,-30.85 141.93,-25.69\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"142.87,-29.07 151.96,-23.62 141.46,-22.21 142.87,-29.07\"/>\n", - "<text text-anchor=\"middle\" x=\"19.11\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M137.48,-275.39C100.15,-270.18 34.38,-254.81 4.73,-210 -4.09,-196.66 2.01,-189.77 4.73,-174 14.89,-115.24 14.87,-86.69 64.73,-54 86.11,-39.99 113.51,-31.22 135.49,-25.97\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"135.96,-29.45 144.96,-23.86 134.43,-22.62 135.96,-29.45\"/>\n", + "<text text-anchor=\"middle\" x=\"17.73\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- []->[c] -->\n", "<g id=\"edge17\" class=\"edge\">\n", "<title>[]->[c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M145.54,-264.56C133.67,-258.38 119.71,-250.72 107.61,-243 94.81,-234.84 81.28,-225 69.76,-216.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"71.82,-213.38 61.76,-210.04 67.54,-218.92 71.82,-213.38\"/>\n", - "<text text-anchor=\"middle\" x=\"117.11\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M137.45,-261.93C127.93,-256.15 117.25,-249.45 107.73,-243 95.82,-234.92 83.07,-225.59 71.93,-217.2\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"74.29,-214.59 64.21,-211.33 70.05,-220.17 74.29,-214.59\"/>\n", + "<text text-anchor=\"middle\" x=\"114.73\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- []->[b,c] -->\n", "<g id=\"edge18\" class=\"edge\">\n", "<title>[]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M166.14,-260.88C154.8,-230.87 131.26,-168.58 117.74,-132.81\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"120.86,-131.17 114.05,-123.05 114.31,-133.64 120.86,-131.17\"/>\n", - "<text text-anchor=\"middle\" x=\"155.11\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M158.45,-260.56C147.73,-230.81 125.81,-170.01 112.89,-134.17\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"116.23,-133.13 109.55,-124.91 109.65,-135.5 116.23,-133.13\"/>\n", + "<text text-anchor=\"middle\" x=\"146.73\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- []->[b] -->\n", "<g id=\"edge19\" class=\"edge\">\n", "<title>[]->[b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M179.08,-260.8C183.51,-249.05 189.46,-233.24 194.5,-219.84\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"197.89,-220.77 198.14,-210.18 191.34,-218.3 197.89,-220.77\"/>\n", - "<text text-anchor=\"middle\" x=\"199.11\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M170.81,-260.8C174.8,-249.47 180.13,-234.36 184.75,-221.29\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"188.04,-222.49 188.07,-211.89 181.44,-220.16 188.04,-222.49\"/>\n", + "<text text-anchor=\"middle\" x=\"187.73\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- []->[a,b] -->\n", "<g id=\"edge20\" class=\"edge\">\n", "<title>[]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M199.78,-268.99C225.06,-258.98 261.22,-240.15 277.61,-210 290.51,-186.27 286.32,-154.83 280.58,-132.76\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"283.92,-131.69 277.8,-123.04 277.19,-133.62 283.92,-131.69\"/>\n", - "<text text-anchor=\"middle\" x=\"295.11\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M191.97,-267.67C215.49,-257.12 247.95,-238.26 262.73,-210 274.96,-186.64 271.31,-156.15 265.91,-134.24\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"269.34,-133.51 263.31,-124.8 262.59,-135.37 269.34,-133.51\"/>\n", + "<text text-anchor=\"middle\" x=\"277.73\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- []->[a] -->\n", "<g id=\"edge21\" class=\"edge\">\n", "<title>[]->[a]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M199.78,-275.93C230.37,-272.63 280.74,-264.2 318.61,-243 329.88,-236.69 340.32,-227.13 348.73,-218.05\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"351.58,-220.1 355.55,-210.28 346.32,-215.48 351.58,-220.1\"/>\n", - "<text text-anchor=\"middle\" x=\"348.11\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M192.14,-275.85C221.56,-272.5 268.78,-264.06 303.73,-243 313.83,-236.92 322.96,-227.86 330.32,-219.11\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"332.92,-221.46 336.37,-211.44 327.43,-217.13 332.92,-221.46\"/>\n", + "<text text-anchor=\"middle\" x=\"328.73\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "<!-- []->[] -->\n", "<g id=\"edge22\" class=\"edge\">\n", "<title>[]->[]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M199.85,-286.87C209.63,-287.04 217.61,-284.41 217.61,-279 217.61,-275.7 214.65,-273.44 210.12,-272.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"210.16,-268.7 199.85,-271.13 209.43,-275.66 210.16,-268.7\"/>\n", - "<text text-anchor=\"middle\" x=\"227.11\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M191.98,-287.15C201.76,-287.32 209.73,-284.61 209.73,-279 209.73,-275.85 207.21,-273.61 203.26,-272.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"203.84,-268.83 193.48,-271.04 202.96,-275.77 203.84,-268.83\"/>\n", + "<text text-anchor=\"middle\" x=\"216.73\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ - "<Dot visualization: expr_as_graph [TWTW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]}(\"tw\",{x,y|(x,y):teilwort & y:TW})]>" + "<Dot visualization: expr_as_graph [LET TW BE TW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]} IN(\n", + "(\"tw\",{x,y | x |-> y : teilwort & y : TW})\n", + ")END]>" ] }, "execution_count": 52, @@ -1539,7 +1541,7 @@ } ], "source": [ - ":dot expr_as_graph (\"tw\",{x,y | x |-> y : teilwort & y : TW })" + ":dot expr_as_graph (\"tw\",{x,y | x |-> y : teilwort & y : TW})" ] }, { @@ -1553,180 +1555,182 @@ "<?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.44.1 (0)\n", + "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n", " -->\n", "<!-- Title: state Pages: 1 -->\n", - "<svg width=\"558pt\" height=\"305pt\"\n", - " viewBox=\"0.00 0.00 557.67 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "<svg width=\"512pt\" height=\"305pt\"\n", + " viewBox=\"0.00 0.00 512.01 305.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n", "<title>state</title>\n", - "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-301 553.67,-301 553.67,4 -4,4\"/>\n", + "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-301 508.01,-301 508.01,4 -4,4\"/>\n", "<!-- [a,b,c] -->\n", "<g id=\"node1\" class=\"node\">\n", "<title>[a,b,c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"397.17,-36 336.17,-36 336.17,0 397.17,0 397.17,-36\"/>\n", - "<text text-anchor=\"middle\" x=\"366.67\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,c]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"366.01,-36 312.01,-36 312.01,0 366.01,0 366.01,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"339.01\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,c]</text>\n", "</g>\n", "<!-- [a,b,c]->[a,b,c] -->\n", "<g id=\"edge1\" class=\"edge\">\n", "<title>[a,b,c]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M397.46,-25.87C407.34,-25.79 415.17,-23.17 415.17,-18 415.17,-14.77 412.11,-12.53 407.41,-11.29\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"407.8,-7.81 397.46,-10.13 406.98,-14.77 407.8,-7.81\"/>\n", - "<text text-anchor=\"middle\" x=\"436.17\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M366.25,-26.15C376.03,-26.32 384.01,-23.61 384.01,-18 384.01,-14.85 381.48,-12.61 377.53,-11.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"378.11,-7.83 367.75,-10.04 377.23,-14.77 378.11,-7.83\"/>\n", + "<text text-anchor=\"middle\" x=\"400.51\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [c] -->\n", "<g id=\"node2\" class=\"node\">\n", "<title>[c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"69.67,-210 15.67,-210 15.67,-174 69.67,-174 69.67,-210\"/>\n", - "<text text-anchor=\"middle\" x=\"42.67\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[c]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"69.01,-210 15.01,-210 15.01,-174 69.01,-174 69.01,-210\"/>\n", + "<text text-anchor=\"middle\" x=\"42.01\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[c]</text>\n", "</g>\n", "<!-- [c]->[c] -->\n", "<g id=\"edge2\" class=\"edge\">\n", "<title>[c]->[c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M69.91,-199.87C79.7,-200.04 87.67,-197.41 87.67,-192 87.67,-188.7 84.71,-186.44 80.18,-185.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.23,-181.7 69.91,-184.13 79.49,-188.66 80.23,-181.7\"/>\n", - "<text text-anchor=\"middle\" x=\"108.67\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M69.25,-200.15C79.03,-200.32 87.01,-197.61 87.01,-192 87.01,-188.85 84.48,-186.61 80.53,-185.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"81.11,-181.83 70.75,-184.04 80.23,-188.77 81.11,-181.83\"/>\n", + "<text text-anchor=\"middle\" x=\"103.51\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [b,c] -->\n", "<g id=\"node3\" class=\"node\">\n", "<title>[b,c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"214.67,-123 160.67,-123 160.67,-87 214.67,-87 214.67,-123\"/>\n", - "<text text-anchor=\"middle\" x=\"187.67\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[b,c]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"201.01,-123 147.01,-123 147.01,-87 201.01,-87 201.01,-123\"/>\n", + "<text text-anchor=\"middle\" x=\"174.01\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[b,c]</text>\n", "</g>\n", "<!-- [b,c]->[b,c] -->\n", "<g id=\"edge3\" class=\"edge\">\n", "<title>[b,c]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M214.91,-112.87C224.7,-113.04 232.67,-110.41 232.67,-105 232.67,-101.7 229.71,-99.44 225.18,-98.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"225.23,-94.7 214.91,-97.13 224.49,-101.66 225.23,-94.7\"/>\n", - "<text text-anchor=\"middle\" x=\"253.67\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M201.25,-113.15C211.03,-113.32 219.01,-110.61 219.01,-105 219.01,-101.85 216.48,-99.61 212.53,-98.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"213.11,-94.83 202.75,-97.04 212.23,-101.77 213.11,-94.83\"/>\n", + "<text text-anchor=\"middle\" x=\"235.51\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [b] -->\n", "<g id=\"node4\" class=\"node\">\n", "<title>[b]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"279.67,-210 225.67,-210 225.67,-174 279.67,-174 279.67,-210\"/>\n", - "<text text-anchor=\"middle\" x=\"252.67\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[b]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"261.01,-210 207.01,-210 207.01,-174 261.01,-174 261.01,-210\"/>\n", + "<text text-anchor=\"middle\" x=\"234.01\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[b]</text>\n", "</g>\n", "<!-- [b]->[b,c] -->\n", "<g id=\"edge4\" class=\"edge\">\n", "<title>[b]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M239.52,-173.8C230.18,-161.59 217.49,-144.99 207,-131.28\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"209.66,-128.99 200.81,-123.18 204.1,-133.25 209.66,-128.99\"/>\n", - "<text text-anchor=\"middle\" x=\"244.67\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M221.86,-173.8C213.54,-162.01 202.34,-146.14 192.86,-132.72\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"195.83,-130.85 187.21,-124.7 190.12,-134.89 195.83,-130.85\"/>\n", + "<text text-anchor=\"middle\" x=\"224.51\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [b]->[b] -->\n", "<g id=\"edge5\" class=\"edge\">\n", "<title>[b]->[b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M279.91,-199.87C289.7,-200.04 297.67,-197.41 297.67,-192 297.67,-188.7 294.71,-186.44 290.18,-185.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"290.23,-181.7 279.91,-184.13 289.49,-188.66 290.23,-181.7\"/>\n", - "<text text-anchor=\"middle\" x=\"318.67\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M261.25,-200.15C271.03,-200.32 279.01,-197.61 279.01,-192 279.01,-188.85 276.48,-186.61 272.53,-185.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"273.11,-181.83 262.75,-184.04 272.23,-188.77 273.11,-181.83\"/>\n", + "<text text-anchor=\"middle\" x=\"295.51\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [a,b] -->\n", "<g id=\"node5\" class=\"node\">\n", "<title>[a,b]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"393.67,-123 339.67,-123 339.67,-87 393.67,-87 393.67,-123\"/>\n", - "<text text-anchor=\"middle\" x=\"366.67\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"366.01,-123 312.01,-123 312.01,-87 366.01,-87 366.01,-123\"/>\n", + "<text text-anchor=\"middle\" x=\"339.01\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\n", "</g>\n", "<!-- [a,b]->[a,b,c] -->\n", "<g id=\"edge6\" class=\"edge\">\n", "<title>[a,b]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M366.67,-86.8C366.67,-75.16 366.67,-59.55 366.67,-46.24\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"370.17,-46.18 366.67,-36.18 363.17,-46.18 370.17,-46.18\"/>\n", - "<text text-anchor=\"middle\" x=\"387.67\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M339.01,-86.8C339.01,-75.58 339.01,-60.67 339.01,-47.69\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"342.51,-47.98 339.01,-37.98 335.51,-47.98 342.51,-47.98\"/>\n", + "<text text-anchor=\"middle\" x=\"355.51\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [a,b]->[a,b] -->\n", "<g id=\"edge7\" class=\"edge\">\n", "<title>[a,b]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M393.91,-112.87C403.7,-113.04 411.67,-110.41 411.67,-105 411.67,-101.7 408.71,-99.44 404.18,-98.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"404.23,-94.7 393.91,-97.13 403.49,-101.66 404.23,-94.7\"/>\n", - "<text text-anchor=\"middle\" x=\"432.67\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M366.25,-113.15C376.03,-113.32 384.01,-110.61 384.01,-105 384.01,-101.85 381.48,-99.61 377.53,-98.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"378.11,-94.83 367.75,-97.04 377.23,-101.77 378.11,-94.83\"/>\n", + "<text text-anchor=\"middle\" x=\"400.51\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [a] -->\n", "<g id=\"node6\" class=\"node\">\n", "<title>[a]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"489.67,-210 435.67,-210 435.67,-174 489.67,-174 489.67,-210\"/>\n", - "<text text-anchor=\"middle\" x=\"462.67\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"453.01,-210 399.01,-210 399.01,-174 453.01,-174 453.01,-210\"/>\n", + "<text text-anchor=\"middle\" x=\"426.01\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a]</text>\n", "</g>\n", "<!-- [a]->[a,b,c] -->\n", "<g id=\"edge8\" class=\"edge\">\n", "<title>[a]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M467.44,-173.91C472.47,-152.22 477.79,-114.34 462.67,-87 450.28,-64.58 426.98,-47.8 406.44,-36.52\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"408.03,-33.41 397.55,-31.88 404.79,-39.61 408.03,-33.41\"/>\n", - "<text text-anchor=\"middle\" x=\"492.67\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M430.4,-173.77C434.94,-152.27 439.62,-114.91 426.01,-87 415.54,-65.53 394.65,-48.85 375.96,-37.38\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"377.89,-34.46 367.48,-32.47 374.38,-40.51 377.89,-34.46\"/>\n", + "<text text-anchor=\"middle\" x=\"450.51\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [a]->[a,b] -->\n", "<g id=\"edge9\" class=\"edge\">\n", "<title>[a]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M443.25,-173.8C429.06,-161.24 409.65,-144.05 393.92,-130.12\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"395.88,-127.18 386.07,-123.18 391.24,-132.43 395.88,-127.18\"/>\n", - "<text text-anchor=\"middle\" x=\"440.67\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M408.4,-173.8C395.86,-161.55 378.82,-144.9 364.76,-131.16\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"367.56,-129.01 357.97,-124.52 362.67,-134.02 367.56,-129.01\"/>\n", + "<text text-anchor=\"middle\" x=\"403.51\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [a]->[a] -->\n", "<g id=\"edge10\" class=\"edge\">\n", "<title>[a]->[a]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M489.91,-199.87C499.7,-200.04 507.67,-197.41 507.67,-192 507.67,-188.7 504.71,-186.44 500.18,-185.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"500.23,-181.7 489.91,-184.13 499.49,-188.66 500.23,-181.7\"/>\n", - "<text text-anchor=\"middle\" x=\"528.67\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M453.25,-200.15C463.03,-200.32 471.01,-197.61 471.01,-192 471.01,-188.85 468.48,-186.61 464.53,-185.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"465.11,-181.83 454.75,-184.04 464.23,-188.77 465.11,-181.83\"/>\n", + "<text text-anchor=\"middle\" x=\"487.51\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- [] -->\n", "<g id=\"node7\" class=\"node\">\n", "<title>[]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"235.67,-297 181.67,-297 181.67,-261 235.67,-261 235.67,-297\"/>\n", - "<text text-anchor=\"middle\" x=\"208.67\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"222.01,-297 168.01,-297 168.01,-261 222.01,-261 222.01,-297\"/>\n", + "<text text-anchor=\"middle\" x=\"195.01\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n", "</g>\n", "<!-- []->[a,b,c] -->\n", "<g id=\"edge11\" class=\"edge\">\n", "<title>[]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M181.21,-275.43C117.36,-268.25 -32.78,-243.68 6.67,-174 71.97,-58.68 246.27,-29.11 325.93,-21.57\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"326.41,-25.04 336.07,-20.68 325.8,-18.07 326.41,-25.04\"/>\n", - "<text text-anchor=\"middle\" x=\"50.67\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M167.64,-274.84C107.18,-266.59 -29.69,-240.28 6.01,-174 64.7,-65.02 225.85,-32.19 300.32,-22.69\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"300.49,-26.19 310,-21.53 299.66,-19.24 300.49,-26.19\"/>\n", + "<text text-anchor=\"middle\" x=\"43.51\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- []->[c] -->\n", "<g id=\"edge12\" class=\"edge\">\n", "<title>[]->[c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M181.28,-270.74C160.87,-264.76 132.67,-255.28 109.67,-243 95.87,-235.63 81.81,-225.6 70.15,-216.45\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"72.12,-213.54 62.13,-210 67.73,-219 72.12,-213.54\"/>\n", - "<text text-anchor=\"middle\" x=\"130.67\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M167.84,-268.96C150.5,-262.71 127.82,-253.62 109.01,-243 96.07,-235.7 82.77,-226.24 71.46,-217.53\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"73.69,-214.83 63.67,-211.38 69.35,-220.32 73.69,-214.83\"/>\n", + "<text text-anchor=\"middle\" x=\"125.51\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- []->[b,c] -->\n", "<g id=\"edge13\" class=\"edge\">\n", "<title>[]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M197.35,-260.96C189.25,-247.7 179.04,-228.5 174.67,-210 168.59,-184.25 173.62,-154.19 179.09,-133.03\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"182.54,-133.7 181.85,-123.13 175.79,-131.82 182.54,-133.7\"/>\n", - "<text text-anchor=\"middle\" x=\"195.67\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M184.85,-260.5C177.73,-247.16 168.81,-228.06 165.01,-210 159.7,-184.83 163.04,-155.6 167.08,-134.55\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"170.46,-135.47 169.09,-124.97 163.61,-134.03 170.46,-135.47\"/>\n", + "<text text-anchor=\"middle\" x=\"181.51\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- []->[b] -->\n", "<g id=\"edge14\" class=\"edge\">\n", "<title>[]->[b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M217.58,-260.8C223.78,-248.82 232.17,-232.62 239.19,-219.06\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"242.29,-220.67 243.78,-210.18 236.08,-217.45 242.29,-220.67\"/>\n", - "<text text-anchor=\"middle\" x=\"253.67\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M202.9,-260.8C208.15,-249.35 215.17,-234.06 221.21,-220.89\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"224.37,-222.39 225.36,-211.84 218.01,-219.47 224.37,-222.39\"/>\n", + "<text text-anchor=\"middle\" x=\"232.51\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- []->[a,b] -->\n", "<g id=\"edge15\" class=\"edge\">\n", "<title>[]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M235.82,-272.63C268.07,-264.75 320.98,-246.81 348.67,-210 365.22,-188.01 368.55,-156.02 368.47,-133.33\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"371.97,-133.24 368.22,-123.33 364.97,-133.42 371.97,-133.24\"/>\n", - "<text text-anchor=\"middle\" x=\"384.67\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M222.37,-270.95C251.63,-261.92 297.05,-243.29 321.01,-210 336.72,-188.16 340.33,-157.17 340.55,-134.7\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"344.05,-134.67 340.4,-124.72 337.05,-134.77 344.05,-134.67\"/>\n", + "<text text-anchor=\"middle\" x=\"351.51\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- []->[a] -->\n", "<g id=\"edge16\" class=\"edge\">\n", "<title>[]->[a]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M235.74,-276.22C272.01,-273.07 337.85,-264.65 389.67,-243 405.6,-236.34 421.61,-225.9 434.57,-216.27\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"436.8,-218.97 442.6,-210.11 432.54,-213.41 436.8,-218.97\"/>\n", - "<text text-anchor=\"middle\" x=\"437.67\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M222.22,-276.1C256.29,-272.89 315.8,-264.47 362.01,-243 375.59,-236.69 388.93,-227 399.87,-217.83\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"402.09,-220.54 407.32,-211.33 397.49,-215.27 402.09,-220.54\"/>\n", + "<text text-anchor=\"middle\" x=\"402.51\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "<!-- []->[] -->\n", "<g id=\"edge17\" class=\"edge\">\n", "<title>[]->[]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M235.91,-286.87C245.7,-287.04 253.67,-284.41 253.67,-279 253.67,-275.7 250.71,-273.44 246.18,-272.21\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"246.23,-268.7 235.91,-271.13 245.49,-275.66 246.23,-268.7\"/>\n", - "<text text-anchor=\"middle\" x=\"274.67\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M222.25,-287.15C232.03,-287.32 240.01,-284.61 240.01,-279 240.01,-275.85 237.48,-273.61 233.53,-272.28\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"234.11,-268.83 223.75,-271.04 233.23,-275.77 234.11,-268.83\"/>\n", + "<text text-anchor=\"middle\" x=\"256.51\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", "</g>\n", "</g>\n", - "</svg>" + "</svg>\n" ], "text/plain": [ - "<Dot visualization: expr_as_graph [TWTW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]}(\"präfix\",{x,y|(x,y):präfix & y:TW})]>" + "<Dot visualization: expr_as_graph [LET TW BE TW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]} IN(\n", + "(\"präfix\",{x,y | x |-> y : präfix & y : TW})\n", + ")END]>" ] }, "execution_count": 53, @@ -1735,7 +1739,7 @@ } ], "source": [ - ":dot expr_as_graph (\"präfix\",{x,y | x |-> y : präfix & y : TW })" + ":dot expr_as_graph (\"präfix\",{x,y | x |-> y : präfix & y : TW})" ] }, { @@ -1749,7 +1753,7 @@ }, { "cell_type": "code", - "execution_count": 63, + "execution_count": 55, "metadata": {}, "outputs": [ { @@ -1758,7 +1762,7 @@ "Loaded machine: FormaleSprachen" ] }, - "execution_count": 63, + "execution_count": 55, "metadata": {}, "output_type": "execute_result" } @@ -1768,115 +1772,138 @@ "/* Formulierung in B der Grundbegriffe aus dem Foliensatz 1 von Informatik 4 */\n", "/* erstellt von Michael Leuschel, 2014 */\n", "SETS\n", - " Alphabet /* Ein Alphabet ist eine endliche, nichtleere Menge von Buchstaben (oder Symbolen). */\n", - " = {a,b,c} /* Hier als Beispiel {a,b,c} */\n", + "Alphabet /* Ein Alphabet ist eine endliche, nichtleere Menge von Buchstaben (oder Symbolen). */\n", + " = {a,b,c} /* Hier als Beispiel {a,b,c} */\n", "ABSTRACT_CONSTANTS\n", - " kat, Worte, Sprachen, kleene, sp, teilwort, praefix\n", + " kat, Worte, Sprachen, kleene, sp, teilwort, praefix\n", "CONSTANTS\n", - " w1, w2, lambda,\n", - " L1, L2, LeereSprache, KomplementL1, L1L2\n", + " w1, w2, lambda,\n", + " L1, L2, LeereSprache, KomplementL1, L1L2\n", "PROPERTIES\n", - " Worte = seq(Alphabet) /* Ein Wort ist eine endliche Folge von Elementen aus dem Alphabet */\n", - " &\n", - " /* Beispiele */\n", - " w1 = [a,a,b,c] & /* in den Folien schreiben wir aabc anstatt [a,a,b,c] */\n", - " w1 : Worte & /* w1 ist ein Wort */\n", - " w2 = [c,a,b,a] &\n", - " w2 : Worte &\n", - " /* Die Laenge eines Wortes ist die Anzahl der Symbole in w */\n", - " /* Beispiel: */\n", - " size(w1) = 4 &\n", - " \n", - "/* Das leere Wort ist das eindeutig bestimmte Wort der Laenge 0 */\n", - " lambda: Worte & size(lambda) = 0 &\n", - "\n", - "/* Die Menge aller Worte bezeichnen wir mit \\Sigma^*. Hier verwenden wir seq(Alphabet) */\n", - "\n", - " /* Eine formale Sprache ist eine jede Teilmenge von \\Sigma^*. */\n", - " Sprachen = {L | L <: Worte} &\n", - " /* Beispiel: */\n", - " L1 = {w1,w2} & L1 : Sprachen &\n", - " L2 = {w2, [a,a,a] } & L2 : Sprachen &\n", - "\n", - " /* Die Leere Sprache ist die Sprache die keine Wörter enthält */\n", - " LeereSprache = {} &\n", - " /* Beachte: */\n", - " LeereSprache /= {lambda} &\n", - "\n", - " /* Die Kardinalität einer Sprache L ist die Anzahl der Wörter von L. \n", - " Beispiel: */\n", - " card(L1) = 2 & card({lambda}) = 1 & card(LeereSprache) = 0 &\n", - "\n", - " /* Beispiele für die Vereinigung von Sprachen: */\n", - " L1 \\/ L2 = {x| x:Worte & (x:L1 or x:L2)} &\n", - "/* Beispiele für die Durchchnitt von Sprachen: */\n", - " L1 /\\ L2 = {x| x:Worte & x:L1 & x:L2} &\n", - "/* Beispiele für die Differenz von Sprachen: */\n", - " L1 - L2 = {x| x:Worte & x:L1 & x/: L2} &\n", - "/* Beispiele für das Komplement von Sprachen: */\n", - " KomplementL1 = Worte - L1 /* kann man auch so schreiben {x| x:Worte & x/: L1} */ &\n", - " w1 /: KomplementL1 & [a,a,a] : KomplementL1 & lambda : KomplementL1 &\n", - "\n", - " /* Konkatenation von Wörtern wird in B mit ^ geschrieben: */\n", - " w1^w2 = [a,a,b,c,c,a,b,a] &\n", - " w1^lambda = w1 & lambda^w1 = w1 &\n", - "\n", - " /* Verkettung von Sprachen */\n", - " L1L2 = {w | #(a,b).(a:L1 & b:L2 & w = a^b)}\n", - "\n", - " & kat = %(x,y).(x:Worte & y:Worte | x^y) /* Die Konkatenierung als explizite Funktion */\n", - " & kat(w1,w2) = [a,a,b,c,c,a,b,a] \n", - " & L1L2 = kat[L1*L2]\n", - "\n", - " /* Eine rekursive Definition von A^n: */\n", - " & kleene = %(A,n).(A : Sprachen & n=0|{lambda}) \\/\n", - " %(A,n).(A : Sprachen & n>0| kat[A*kleene(A,n-1)])\n", - " & kleene(L1,1) = L1\n", - " & kleene(L2,1) = L2\n", - "/* A^* ist momentan schwieriger darstellbar, zumindest so, dass man mit ProB damit\n", - " arbeiten könnte */\n", - "\n", - " & /* Die Spiegelbildoperation */\n", - " sp = %u.(u:Worte| %i.(i:dom(u)|u(size(u)+1-i)))\n", - " & sp(w1) = [c,b,a,a]\n", - " & sp(sp(w1)) = w1\n", - " & sp(lambda) = lambda\n", - "\n", - " /* Die Spiegelung einer Sprache bekommt man einfach durch das relational image: */\n", - " & sp[L1] = {sp(w1),sp(w2)}\n", - " & sp[sp[L1]] = L1\n", - " & sp[sp[L2]] = L2\n", - "\n", - " /* Die Teilwortrelation */\n", - " & teilwort = {u,v | u:Worte & v:Worte & #(v1,v2).(v1^u^v2 = v)}\n", - " & [a,a] |-> [c,b,a,a,b] : teilwort\n", - " & [a,a,a] |-> [c,b,a,a,b] /: teilwort\n", - " /* Wir können alle Teilworte durch das relational image der Umkehrrelation berechnen: */\n", - " & teilwort~[{[a,a,b]}] = { lambda, [a], [b], [a,a],[a,b], [a,a,b] }\n", - "\n", - " /* Die Anfangswortrelation */\n", - " & praefix = {u,v | u:Worte & v:Worte & #(w).(u^w = v)}\n", - " & [a,a] |-> [c,b,a,a,b] /: praefix\n", - " & [c,b] |-> [c,b,a,a,b] : praefix\n", - " /* Wir können alle Präfixe durch das relational image der Umkehrrelation berechnen: */\n", - " & praefix~[{[a,a,b]}] = { lambda, [a], [a,a], [a,a,b] }\n", + " Worte = seq(Alphabet) /* Ein Wort ist eine endliche Folge von Elementen aus dem Alphabet */\n", + " &\n", + " /* Beispiele */\n", + " w1 = [a,a,b,c] & /* in den Folien schreiben wir aabc anstatt [a,a,b,c] */\n", + " w1 : Worte & /* w1 ist ein Wort */\n", + " w2 = [c,a,b,a] &\n", + " w2 : Worte &\n", + " /* Die Laenge eines Wortes ist die Anzahl der Symbole in w */\n", + " /* Beispiel: */\n", + " size(w1) = 4 &\n", + " \n", + " /* Das leere Wort ist das eindeutig bestimmte Wort der Laenge 0 */\n", + " lambda: Worte & size(lambda) = 0 &\n", + " \n", + " /* Die Menge aller Worte bezeichnen wir mit \\Sigma^*. Hier verwenden wir seq(Alphabet) */\n", + " \n", + " /* Eine formale Sprache ist eine jede Teilmenge von \\Sigma^*. */\n", + " Sprachen = {L | L <: Worte} &\n", + " /* Beispiel: */\n", + " L1 = {w1,w2} & L1 : Sprachen &\n", + " L2 = {w2, [a,a,a] } & L2 : Sprachen &\n", + " \n", + " /* Die Leere Sprache ist die Sprache die keine Wörter enthält */\n", + " LeereSprache = {} &\n", + " /* Beachte: */\n", + " LeereSprache /= {lambda} &\n", + " \n", + " /* Die Kardinalität einer Sprache L ist die Anzahl der Wörter von L. \n", + " Beispiel: */\n", + " card(L1) = 2 & card({lambda}) = 1 & card(LeereSprache) = 0 &\n", + " \n", + " /* Beispiele für die Vereinigung von Sprachen: */\n", + " L1 \\/ L2 = {x| x:Worte & (x:L1 or x:L2)} &\n", + " /* Beispiele für die Durchchnitt von Sprachen: */\n", + " L1 /\\ L2 = {x| x:Worte & x:L1 & x:L2} &\n", + " /* Beispiele für die Differenz von Sprachen: */\n", + " L1 - L2 = {x| x:Worte & x:L1 & x/: L2} &\n", + " /* Beispiele für das Komplement von Sprachen: */\n", + " KomplementL1 = Worte - L1 /* kann man auch so schreiben {x| x:Worte & x/: L1} */ &\n", + " w1 /: KomplementL1 & [a,a,a] : KomplementL1 & lambda : KomplementL1 &\n", + " \n", + " /* Konkatenation von Wörtern wird in B mit ^ geschrieben: */\n", + " w1^w2 = [a,a,b,c,c,a,b,a] &\n", + " w1^lambda = w1 & lambda^w1 = w1 &\n", + " \n", + " /* Verkettung von Sprachen */\n", + " L1L2 = {w | #(a,b).(a:L1 & b:L2 & w = a^b)}\n", + " \n", + " & kat = %(x,y).(x:Worte & y:Worte | x^y) /* Die Konkatenierung als explizite Funktion */\n", + " & kat(w1,w2) = [a,a,b,c,c,a,b,a] \n", + " & L1L2 = kat[L1*L2]\n", + " \n", + " /* Eine rekursive Definition von A^n: */\n", + " & kleene = %(A,n).(A : Sprachen & n=0|{lambda}) \\/\n", + " %(A,n).(A : Sprachen & n>0| kat[A*kleene(A,n-1)])\n", + " & kleene(L1,1) = L1\n", + " & kleene(L2,1) = L2\n", + " /* A^* ist momentan schwieriger darstellbar, zumindest so, dass man mit ProB damit\n", + " arbeiten könnte */\n", + " \n", + " /* Die Spiegelbildoperation */\n", + " & sp = %u.(u:Worte| %i.(i:dom(u)|u(size(u)+1-i)))\n", + " & sp(w1) = [c,b,a,a]\n", + " & sp(sp(w1)) = w1\n", + " & sp(lambda) = lambda\n", + " \n", + " /* Die Spiegelung einer Sprache bekommt man einfach durch das relational image: */\n", + " & sp[L1] = {sp(w1),sp(w2)}\n", + " & sp[sp[L1]] = L1\n", + " & sp[sp[L2]] = L2\n", + " \n", + " /* Die Teilwortrelation */\n", + " & teilwort = {u,v | u:Worte & v:Worte & #(v1,v2).(v1^u^v2 = v)}\n", + " & [a,a] |-> [c,b,a,a,b] : teilwort\n", + " & [a,a,a] |-> [c,b,a,a,b] /: teilwort\n", + " /* Wir können alle Teilworte durch das relational image der Umkehrrelation berechnen: */\n", + " & teilwort~[{[a,a,b]}] = { lambda, [a], [b], [a,a],[a,b], [a,a,b] }\n", + " \n", + " /* Die Anfangswortrelation */\n", + " & praefix = {u,v | u:Worte & v:Worte & #(w).(u^w = v)}\n", + " & [a,a] |-> [c,b,a,a,b] /: praefix\n", + " & [c,b] |-> [c,b,a,a,b] : praefix\n", + " /* Wir können alle Präfixe durch das relational image der Umkehrrelation berechnen: */\n", + " & praefix~[{[a,a,b]}] = { lambda, [a], [a,a], [a,a,b] }\n", "ASSERTIONS\n", - " card(L1L2) = 4\n", + " card(L1L2) = 4\n", + "DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE\n", "END" ] }, { "cell_type": "code", - "execution_count": 66, + "execution_count": 56, "metadata": {}, "outputs": [ { - "ename": "IllegalArgumentException", - "evalue": "Executing operation $initialise_machine with predicate 1=1 produced errors: Could not execute operation INITIALISATION in state root", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Could not execute operation INITIALISATION in state root\u001b[0m" - ] + "data": { + "text/plain": [ + "Executed operation: SETUP_CONSTANTS()" + ] + }, + "execution_count": 56, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":constants" + ] + }, + { + "cell_type": "code", + "execution_count": 57, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: INITIALISATION()" + ] + }, + "execution_count": 57, + "metadata": {}, + "output_type": "execute_result" } ], "source": [ @@ -1885,16 +1912,21 @@ }, { "cell_type": "code", - "execution_count": 67, + "execution_count": 58, "metadata": {}, "outputs": [ { - "ename": "CommandExecutionException", - "evalue": ":eval: NOT-INITIALISED", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m:eval: NOT-INITIALISED\u001b[0m" - ] + "data": { + "text/markdown": [ + "$\\{[\\mathit{c},\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{c},\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{c},\\mathit{a},\\mathit{b},\\mathit{a}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}],[\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{b},\\mathit{a}]\\}$" + ], + "text/plain": [ + "{[c,a,b,a,a,a,b,c],[c,a,b,a,c,a,b,a],[a,a,b,c,a,a,b,c],[a,a,b,c,c,a,b,a]}" + ] + }, + "execution_count": 58, + "metadata": {}, + "output_type": "execute_result" } ], "source": [ -- GitLab