From a231c47211578fb046324f926c7e25423e43f3a3 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 29 Apr 2020 17:45:13 +0200
Subject: [PATCH] add more comments and Verkettung

---
 info4/kapitel-1/FormaleSprachen.ipynb | 400 +++++++++++++++++---------
 1 file changed, 260 insertions(+), 140 deletions(-)

diff --git a/info4/kapitel-1/FormaleSprachen.ipynb b/info4/kapitel-1/FormaleSprachen.ipynb
index 8739d6a..63632f0 100644
--- a/info4/kapitel-1/FormaleSprachen.ipynb
+++ b/info4/kapitel-1/FormaleSprachen.ipynb
@@ -4,12 +4,14 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "## Formale Sprachen"
+    "## Formale Sprachen\n",
+    "\n",
+    "Dieses Notebook begleitet Vorlesung 3 und erläutert die grundlegenden Definitionen der formalen Sprachen."
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 1,
+   "execution_count": 67,
    "metadata": {},
    "outputs": [
     {
@@ -18,7 +20,7 @@
        "Loaded machine: Alphabet"
       ]
      },
-     "execution_count": 1,
+     "execution_count": 67,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -45,7 +47,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": 70,
    "metadata": {},
    "outputs": [
     {
@@ -57,7 +59,7 @@
        "TRUE"
       ]
      },
-     "execution_count": 2,
+     "execution_count": 70,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -68,7 +70,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": 71,
    "metadata": {},
    "outputs": [
     {
@@ -80,7 +82,7 @@
        "TRUE"
       ]
      },
-     "execution_count": 3,
+     "execution_count": 71,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -98,7 +100,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": 72,
    "metadata": {},
    "outputs": [
     {
@@ -110,7 +112,7 @@
        "3"
       ]
      },
-     "execution_count": 4,
+     "execution_count": 72,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -121,7 +123,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": 73,
    "metadata": {},
    "outputs": [
     {
@@ -133,7 +135,7 @@
        "4"
       ]
      },
-     "execution_count": 5,
+     "execution_count": 73,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -151,7 +153,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": 74,
    "metadata": {},
    "outputs": [
     {
@@ -169,7 +171,7 @@
        "\tε = ∅"
       ]
      },
-     "execution_count": 6,
+     "execution_count": 74,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -189,7 +191,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 75,
    "metadata": {},
    "outputs": [
     {
@@ -207,7 +209,7 @@
        "\tSprachen = {L∣L ⊆ seq(Σ)}"
       ]
      },
-     "execution_count": 7,
+     "execution_count": 75,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -220,12 +222,12 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "In folgender B Maschine werden wir ein paar Sprachen definieren:"
+    "In folgender B Maschine werden wir ein paar Sprachen und Wörter definieren:"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 77,
    "metadata": {},
    "outputs": [
     {
@@ -234,7 +236,7 @@
        "Loaded machine: Alphabet"
       ]
      },
-     "execution_count": 8,
+     "execution_count": 77,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -248,7 +250,7 @@
     "  ε ∈ seq(Σ) ∧ size(ε) = 0 ∧\n",
     "  Sprachen = {L | L ⊆ seq(Σ)}∧\n",
     "  w₁ = [a,a,b,c] ∧\n",
-    "  w₂ = [c,a,b,a] ∧\n",
+    "  w₂ = [c,c] ∧\n",
     "  L₁ = {w₁,w₂} ∧\n",
     "  L₂ = {w₂, [a,a,a] }\n",
     "END"
@@ -256,7 +258,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 9,
+   "execution_count": 78,
    "metadata": {},
    "outputs": [
     {
@@ -265,7 +267,7 @@
        "Machine constants set up using operation 0: $setup_constants()"
       ]
      },
-     "execution_count": 9,
+     "execution_count": 78,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -276,7 +278,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 10,
+   "execution_count": 79,
    "metadata": {},
    "outputs": [
     {
@@ -288,7 +290,7 @@
        "{(1↦a),(2↦a),(3↦b),(4↦c)}"
       ]
      },
-     "execution_count": 10,
+     "execution_count": 79,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -306,7 +308,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 11,
+   "execution_count": 80,
    "metadata": {},
    "outputs": [
     {
@@ -315,7 +317,7 @@
        "Preference changed: PP_SEQUENCES = TRUE\n"
       ]
      },
-     "execution_count": 11,
+     "execution_count": 80,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -326,7 +328,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 12,
+   "execution_count": 81,
    "metadata": {},
    "outputs": [
     {
@@ -338,7 +340,7 @@
        "[a,a,b,c]"
       ]
      },
-     "execution_count": 12,
+     "execution_count": 81,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -356,19 +358,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 13,
+   "execution_count": 82,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$[c,\\mathit{a},\\mathit{b},a]$"
+       "$[c,c]$"
       ],
       "text/plain": [
-       "[c,a,b,a]"
+       "[c,c]"
       ]
      },
-     "execution_count": 13,
+     "execution_count": 82,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -379,19 +381,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 83,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\}$"
       ],
       "text/plain": [
-       "{[a,a,b,c],[c,a,b,a]}"
+       "{[c,c],[a,a,b,c]}"
       ]
      },
-     "execution_count": 14,
+     "execution_count": 83,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -409,7 +411,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": 84,
    "metadata": {},
    "outputs": [
     {
@@ -427,7 +429,7 @@
        "\tLeereSprache = []"
       ]
      },
-     "execution_count": 15,
+     "execution_count": 84,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -445,7 +447,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
+   "execution_count": 85,
    "metadata": {},
    "outputs": [
     {
@@ -457,7 +459,7 @@
        "2"
       ]
      },
-     "execution_count": 16,
+     "execution_count": 85,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -468,7 +470,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 86,
    "metadata": {},
    "outputs": [
     {
@@ -480,7 +482,7 @@
        "1"
       ]
      },
-     "execution_count": 17,
+     "execution_count": 86,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -491,7 +493,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 18,
+   "execution_count": 87,
    "metadata": {},
    "outputs": [
     {
@@ -503,7 +505,7 @@
        "0"
       ]
      },
-     "execution_count": 18,
+     "execution_count": 87,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -521,19 +523,65 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 19,
+   "execution_count": 88,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\}$"
+      ],
+      "text/plain": [
+       "{[c,c],[a,a,b,c]}"
+      ]
+     },
+     "execution_count": 88,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "L₁"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 90,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{[c,c],[a,\\mathit{a},a]\\}$"
+      ],
+      "text/plain": [
+       "{[c,c],[a,a,a]}"
+      ]
+     },
+     "execution_count": 90,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "L₂"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 91,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[c,c],[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c]\\}$"
       ],
       "text/plain": [
-       "{[a,a,a],[a,a,b,c],[c,a,b,a]}"
+       "{[c,c],[a,a,a],[a,a,b,c]}"
       ]
      },
-     "execution_count": 19,
+     "execution_count": 91,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -544,19 +592,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 20,
+   "execution_count": 92,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[c,c],[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c]\\}$"
       ],
       "text/plain": [
-       "{[a,a,a],[a,a,b,c],[c,a,b,a]}"
+       "{[c,c],[a,a,a],[a,a,b,c]}"
       ]
      },
-     "execution_count": 20,
+     "execution_count": 92,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -567,19 +615,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": 93,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[c,\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[c,c]\\}$"
       ],
       "text/plain": [
-       "{[c,a,b,a]}"
+       "{[c,c]}"
       ]
      },
-     "execution_count": 21,
+     "execution_count": 93,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -590,19 +638,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 22,
+   "execution_count": 94,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[c,\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[c,c]\\}$"
       ],
       "text/plain": [
-       "{[c,a,b,a]}"
+       "{[c,c]}"
       ]
      },
-     "execution_count": 22,
+     "execution_count": 94,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -613,7 +661,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 23,
+   "execution_count": 95,
    "metadata": {},
    "outputs": [
     {
@@ -625,7 +673,7 @@
        "{[a,a,b,c]}"
       ]
      },
-     "execution_count": 23,
+     "execution_count": 95,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -636,7 +684,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 24,
+   "execution_count": 96,
    "metadata": {},
    "outputs": [
     {
@@ -648,7 +696,7 @@
        "{[a,a,a]}"
       ]
      },
-     "execution_count": 24,
+     "execution_count": 96,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -659,7 +707,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 25,
+   "execution_count": 97,
    "metadata": {},
    "outputs": [
     {
@@ -668,16 +716,16 @@
        "$\\mathit{TRUE}$\n",
        "\n",
        "**Solution:**\n",
-       "* $\\mathit{Komplement} = (\\mathit{seq}(Σ) - \\{[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\})$"
+       "* $\\mathit{Komplement} = (\\mathit{seq}(Σ) - \\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\})$"
       ],
       "text/plain": [
        "TRUE\n",
        "\n",
        "Solution:\n",
-       "\tKomplement = (seq(Σ) − {[a,a,b,c],[c,a,b,a]})"
+       "\tKomplement = (seq(Σ) − {[c,c],[a,a,b,c]})"
       ]
      },
-     "execution_count": 25,
+     "execution_count": 97,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -697,7 +745,30 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 26,
+   "execution_count": 101,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$[a,\\mathit{a},\\mathit{b},c]$"
+      ],
+      "text/plain": [
+       "[a,a,b,c]"
+      ]
+     },
+     "execution_count": 101,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "w₁"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 102,
    "metadata": {},
    "outputs": [
     {
@@ -709,7 +780,7 @@
        "[a,a,b,c,a,a,b,c]"
       ]
      },
-     "execution_count": 26,
+     "execution_count": 102,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -720,7 +791,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 27,
+   "execution_count": 103,
    "metadata": {},
    "outputs": [
     {
@@ -732,7 +803,7 @@
        "[a,a,b,c]"
       ]
      },
-     "execution_count": 27,
+     "execution_count": 103,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -743,7 +814,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 28,
+   "execution_count": 104,
    "metadata": {},
    "outputs": [
     {
@@ -755,7 +826,7 @@
        "[a,a,b,c]"
       ]
      },
-     "execution_count": 28,
+     "execution_count": 104,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -773,19 +844,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 29,
+   "execution_count": 105,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\}$"
       ],
       "text/plain": [
-       "{[a,a,b,c],[c,a,b,a]}"
+       "{[c,c],[a,a,b,c]}"
       ]
      },
-     "execution_count": 29,
+     "execution_count": 105,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -796,19 +867,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 30,
+   "execution_count": 106,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[a,\\mathit{a},a],[c,\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[c,c],[a,\\mathit{a},a]\\}$"
       ],
       "text/plain": [
-       "{[a,a,a],[c,a,b,a]}"
+       "{[c,c],[a,a,a]}"
       ]
      },
-     "execution_count": 30,
+     "execution_count": 106,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -819,19 +890,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 31,
+   "execution_count": 107,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[c,\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{a},\\mathit{a},a],[c,\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{c},\\mathit{a},\\mathit{b},a],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},a],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[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]\\}$"
       ],
       "text/plain": [
-       "{[c,a,b,a,a,a,a],[c,a,b,a,c,a,b,a],[a,a,b,c,a,a,a],[a,a,b,c,c,a,b,a]}"
+       "{[c,c,c,c],[c,c,a,a,a],[a,a,b,c,c,c],[a,a,b,c,a,a,a]}"
       ]
      },
-     "execution_count": 31,
+     "execution_count": 107,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -844,53 +915,112 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "Man kann eine Sprache auch mit sich selber verketten:"
+    "Man kann eine Sprache auch mit sich selber verketten.\n",
+    "Dies ist die Sprache $L_1^2$:"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 32,
+   "execution_count": 114,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[c,\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{c},\\mathit{a},\\mathit{b},a],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[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]\\}$"
       ],
       "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]}"
+       "{[c,c,c,c],[c,c,a,a,b,c],[a,a,b,c,c,c],[a,a,b,c,a,a,b,c]}"
       ]
      },
-     "execution_count": 32,
+     "execution_count": 114,
      "metadata": {},
      "output_type": "execute_result"
     }
    ],
    "source": [
-    "{w | ∃(a,b).(a∈L₁ ∧ b∈L₁ ∧ w = a^b)}"
+    ":let L1_2 {w | ∃(a,b).(a∈L₁ ∧ b∈L₁ ∧ w = a^b)}"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Man kann eine Sprache auch mehrfach mit sich selber verketten.\n",
+    "Dies sind die Sprachen $L_1^3$ und $L_1^4$:"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 33,
+   "execution_count": 118,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$"
+       "$\\{[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]\\}$"
       ],
       "text/plain": [
-       "{[a,a,b,c],[c,a,b,a]}"
+       "{[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]}"
       ]
      },
-     "execution_count": 33,
+     "execution_count": 118,
      "metadata": {},
      "output_type": "execute_result"
     }
    ],
    "source": [
-    "L₁"
+    ":let L1_3 {w | ∃(a,b).(a∈L₁ ∧ b∈L1_2 ∧ w = a^b)}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 119,
+   "metadata": {},
+   "outputs": [
+    {
+     "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]\\}$"
+      ],
+      "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]}"
+      ]
+     },
+     "execution_count": 119,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let L1_4 {w | ∃(a,b).(a∈L₁ ∧ b∈L1_3 ∧ w = a^b)}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 129,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    ":unlet L1_2"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 130,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    ":unlet L1_3"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 131,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    ":unlet L1_4"
    ]
   },
   {
@@ -902,7 +1032,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 34,
+   "execution_count": 132,
    "metadata": {},
    "outputs": [
     {
@@ -914,7 +1044,7 @@
        "[c,b,a,a]"
       ]
      },
-     "execution_count": 34,
+     "execution_count": 132,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -932,7 +1062,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 35,
+   "execution_count": 133,
    "metadata": {},
    "outputs": [
     {
@@ -944,7 +1074,7 @@
        "{[a,b,a,c],[c,b,a,a]}"
       ]
      },
-     "execution_count": 35,
+     "execution_count": 133,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -962,7 +1092,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 56,
+   "execution_count": 134,
    "metadata": {},
    "outputs": [
     {
@@ -971,7 +1101,7 @@
        "Loaded machine: Alphabet"
       ]
      },
-     "execution_count": 56,
+     "execution_count": 134,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -998,7 +1128,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 57,
+   "execution_count": 135,
    "metadata": {},
    "outputs": [
     {
@@ -1007,7 +1137,7 @@
        "Machine constants set up using operation 0: $setup_constants()"
       ]
      },
-     "execution_count": 57,
+     "execution_count": 135,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1018,25 +1148,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 58,
+   "execution_count": 136,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\mathit{TRUE}$\n",
-       "\n",
-       "**Solution:**\n",
-       "* $\\mathit{TW} = \\{[],[a],[a,b],[b],[b,c],[c],[a,\\mathit{b},c]\\}$"
+       "$\\mathit{TRUE}$"
       ],
       "text/plain": [
-       "TRUE\n",
-       "\n",
-       "Solution:\n",
-       "\tTW = {[],[a],[a,b],[b],[b,c],[c],[a,b,c]}"
+       "TRUE"
       ]
      },
-     "execution_count": 58,
+     "execution_count": 136,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1047,7 +1171,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 59,
+   "execution_count": 137,
    "metadata": {},
    "outputs": [
     {
@@ -1059,7 +1183,7 @@
        "FALSE"
       ]
      },
-     "execution_count": 59,
+     "execution_count": 137,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1070,25 +1194,19 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 60,
+   "execution_count": 138,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\mathit{TRUE}$\n",
-       "\n",
-       "**Solution:**\n",
-       "* $\\mathit{TW} = \\{[],[a],[a,b],[b],[b,c],[c],[a,\\mathit{b},c]\\}$"
+       "$\\mathit{TRUE}$"
       ],
       "text/plain": [
-       "TRUE\n",
-       "\n",
-       "Solution:\n",
-       "\tTW = {[],[a],[a,b],[b],[b,c],[c],[a,b,c]}"
+       "TRUE"
       ]
      },
-     "execution_count": 60,
+     "execution_count": 138,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1106,7 +1224,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 61,
+   "execution_count": 139,
    "metadata": {},
    "outputs": [
     {
@@ -1118,7 +1236,7 @@
        "{[],[c],[c,b],[c,b,a],[c,b,a,a],[c,b,a,a,b]}"
       ]
      },
-     "execution_count": 61,
+     "execution_count": 139,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1129,7 +1247,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 62,
+   "execution_count": 140,
    "metadata": {},
    "outputs": [
     {
@@ -1141,7 +1259,7 @@
        "{[],[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]}"
       ]
      },
-     "execution_count": 62,
+     "execution_count": 140,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1152,7 +1270,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 63,
+   "execution_count": 141,
    "metadata": {},
    "outputs": [
     {
@@ -1164,7 +1282,7 @@
        "{[],[a],[a,b],[b],[b,c],[c],[a,b,c]}"
       ]
      },
-     "execution_count": 63,
+     "execution_count": 141,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1175,7 +1293,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 64,
+   "execution_count": 142,
    "metadata": {},
    "outputs": [
     {
@@ -1184,7 +1302,7 @@
        "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n"
       ]
      },
-     "execution_count": 64,
+     "execution_count": 142,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1195,7 +1313,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 65,
+   "execution_count": 143,
    "metadata": {},
    "outputs": [
     {
@@ -1386,7 +1504,7 @@
        "<Dot visualization: expr_as_graph [TWTW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]}(\"tw\",{x,y|(x,y):teilwort & y:TW})]>"
       ]
      },
-     "execution_count": 65,
+     "execution_count": 143,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1397,7 +1515,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 66,
+   "execution_count": 144,
    "metadata": {},
    "outputs": [
     {
@@ -1558,7 +1676,7 @@
        "<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})]>"
       ]
      },
-     "execution_count": 66,
+     "execution_count": 144,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1569,10 +1687,12 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 145,
    "metadata": {},
    "outputs": [],
-   "source": []
+   "source": [
+    ":unlet TW"
+   ]
   },
   {
    "cell_type": "code",
-- 
GitLab