diff --git a/info4/kapitel-1/FormaleSprachen.ipynb b/info4/kapitel-1/FormaleSprachen.ipynb index 5371160f86a09efa875eacfbcac3ec6896006d33..44a9b80a328235cea1b6d1629207f06bbb6e159b 100644 --- a/info4/kapitel-1/FormaleSprachen.ipynb +++ b/info4/kapitel-1/FormaleSprachen.ipynb @@ -11,7 +11,7 @@ }, { "cell_type": "code", - "execution_count": 67, + "execution_count": 1, "metadata": {}, "outputs": [ { @@ -20,7 +20,7 @@ "Loaded machine: Alphabet" ] }, - "execution_count": 67, + "execution_count": 1, "metadata": {}, "output_type": "execute_result" } @@ -47,7 +47,7 @@ }, { "cell_type": "code", - "execution_count": 70, + "execution_count": 2, "metadata": {}, "outputs": [ { @@ -59,7 +59,7 @@ "TRUE" ] }, - "execution_count": 70, + "execution_count": 2, "metadata": {}, "output_type": "execute_result" } @@ -70,7 +70,7 @@ }, { "cell_type": "code", - "execution_count": 71, + "execution_count": 3, "metadata": {}, "outputs": [ { @@ -82,7 +82,7 @@ "TRUE" ] }, - "execution_count": 71, + "execution_count": 3, "metadata": {}, "output_type": "execute_result" } @@ -100,7 +100,7 @@ }, { "cell_type": "code", - "execution_count": 72, + "execution_count": 4, "metadata": {}, "outputs": [ { @@ -112,7 +112,7 @@ "3" ] }, - "execution_count": 72, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -123,7 +123,7 @@ }, { "cell_type": "code", - "execution_count": 73, + "execution_count": 5, "metadata": {}, "outputs": [ { @@ -135,7 +135,7 @@ "4" ] }, - "execution_count": 73, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -153,7 +153,7 @@ }, { "cell_type": "code", - "execution_count": 74, + "execution_count": 6, "metadata": {}, "outputs": [ { @@ -171,7 +171,7 @@ "\tε = ∅" ] }, - "execution_count": 74, + "execution_count": 6, "metadata": {}, "output_type": "execute_result" } @@ -191,7 +191,7 @@ }, { "cell_type": "code", - "execution_count": 75, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -209,7 +209,7 @@ "\tSprachen = {L∣L ⊆ seq(Σ)}" ] }, - "execution_count": 75, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } @@ -227,7 +227,7 @@ }, { "cell_type": "code", - "execution_count": 77, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -236,7 +236,7 @@ "Loaded machine: Alphabet" ] }, - "execution_count": 77, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -258,7 +258,7 @@ }, { "cell_type": "code", - "execution_count": 78, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -267,7 +267,7 @@ "Machine constants set up using operation 0: $setup_constants()" ] }, - "execution_count": 78, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -278,7 +278,7 @@ }, { "cell_type": "code", - "execution_count": 79, + "execution_count": 10, "metadata": {}, "outputs": [ { @@ -290,7 +290,7 @@ "{(1↦a),(2↦a),(3↦b),(4↦c)}" ] }, - "execution_count": 79, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -308,7 +308,7 @@ }, { "cell_type": "code", - "execution_count": 80, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -317,7 +317,7 @@ "Preference changed: PP_SEQUENCES = TRUE\n" ] }, - "execution_count": 80, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -328,7 +328,7 @@ }, { "cell_type": "code", - "execution_count": 81, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -340,7 +340,7 @@ "[a,a,b,c]" ] }, - "execution_count": 81, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -358,7 +358,7 @@ }, { "cell_type": "code", - "execution_count": 82, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -370,7 +370,7 @@ "[c,c]" ] }, - "execution_count": 82, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -381,7 +381,7 @@ }, { "cell_type": "code", - "execution_count": 83, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -393,7 +393,7 @@ "{[c,c],[a,a,b,c]}" ] }, - "execution_count": 83, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -411,7 +411,7 @@ }, { "cell_type": "code", - "execution_count": 84, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -429,7 +429,7 @@ "\tLeereSprache = []" ] }, - "execution_count": 84, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -447,7 +447,7 @@ }, { "cell_type": "code", - "execution_count": 85, + "execution_count": 16, "metadata": {}, "outputs": [ { @@ -459,7 +459,7 @@ "2" ] }, - "execution_count": 85, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } @@ -470,7 +470,7 @@ }, { "cell_type": "code", - "execution_count": 86, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -482,7 +482,7 @@ "1" ] }, - "execution_count": 86, + "execution_count": 17, "metadata": {}, "output_type": "execute_result" } @@ -493,7 +493,7 @@ }, { "cell_type": "code", - "execution_count": 87, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -505,7 +505,7 @@ "0" ] }, - "execution_count": 87, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -523,7 +523,7 @@ }, { "cell_type": "code", - "execution_count": 88, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -535,7 +535,7 @@ "{[c,c],[a,a,b,c]}" ] }, - "execution_count": 88, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -546,7 +546,7 @@ }, { "cell_type": "code", - "execution_count": 90, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -558,7 +558,7 @@ "{[c,c],[a,a,a]}" ] }, - "execution_count": 90, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -569,7 +569,7 @@ }, { "cell_type": "code", - "execution_count": 91, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -581,7 +581,7 @@ "{[c,c],[a,a,a],[a,a,b,c]}" ] }, - "execution_count": 91, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } @@ -592,7 +592,7 @@ }, { "cell_type": "code", - "execution_count": 92, + "execution_count": 22, "metadata": {}, "outputs": [ { @@ -604,7 +604,7 @@ "{[c,c],[a,a,a],[a,a,b,c]}" ] }, - "execution_count": 92, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } @@ -615,7 +615,7 @@ }, { "cell_type": "code", - "execution_count": 93, + "execution_count": 23, "metadata": {}, "outputs": [ { @@ -627,7 +627,7 @@ "{[c,c]}" ] }, - "execution_count": 93, + "execution_count": 23, "metadata": {}, "output_type": "execute_result" } @@ -638,7 +638,7 @@ }, { "cell_type": "code", - "execution_count": 94, + "execution_count": 24, "metadata": {}, "outputs": [ { @@ -650,7 +650,7 @@ "{[c,c]}" ] }, - "execution_count": 94, + "execution_count": 24, "metadata": {}, "output_type": "execute_result" } @@ -661,7 +661,7 @@ }, { "cell_type": "code", - "execution_count": 95, + "execution_count": 25, "metadata": {}, "outputs": [ { @@ -673,7 +673,7 @@ "{[a,a,b,c]}" ] }, - "execution_count": 95, + "execution_count": 25, "metadata": {}, "output_type": "execute_result" } @@ -684,7 +684,7 @@ }, { "cell_type": "code", - "execution_count": 96, + "execution_count": 26, "metadata": {}, "outputs": [ { @@ -696,7 +696,7 @@ "{[a,a,a]}" ] }, - "execution_count": 96, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -707,7 +707,7 @@ }, { "cell_type": "code", - "execution_count": 97, + "execution_count": 27, "metadata": {}, "outputs": [ { @@ -725,7 +725,7 @@ "\tKomplement = (seq(Σ) − {[c,c],[a,a,b,c]})" ] }, - "execution_count": 97, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -745,7 +745,7 @@ }, { "cell_type": "code", - "execution_count": 101, + "execution_count": 28, "metadata": {}, "outputs": [ { @@ -757,7 +757,7 @@ "[a,a,b,c]" ] }, - "execution_count": 101, + "execution_count": 28, "metadata": {}, "output_type": "execute_result" } @@ -768,7 +768,7 @@ }, { "cell_type": "code", - "execution_count": 102, + "execution_count": 29, "metadata": {}, "outputs": [ { @@ -780,7 +780,7 @@ "[a,a,b,c,a,a,b,c]" ] }, - "execution_count": 102, + "execution_count": 29, "metadata": {}, "output_type": "execute_result" } @@ -791,7 +791,7 @@ }, { "cell_type": "code", - "execution_count": 103, + "execution_count": 30, "metadata": {}, "outputs": [ { @@ -803,7 +803,7 @@ "[a,a,b,c]" ] }, - "execution_count": 103, + "execution_count": 30, "metadata": {}, "output_type": "execute_result" } @@ -814,7 +814,7 @@ }, { "cell_type": "code", - "execution_count": 104, + "execution_count": 31, "metadata": {}, "outputs": [ { @@ -826,7 +826,7 @@ "[a,a,b,c]" ] }, - "execution_count": 104, + "execution_count": 31, "metadata": {}, "output_type": "execute_result" } @@ -844,7 +844,7 @@ }, { "cell_type": "code", - "execution_count": 105, + "execution_count": 32, "metadata": {}, "outputs": [ { @@ -856,7 +856,7 @@ "{[c,c],[a,a,b,c]}" ] }, - "execution_count": 105, + "execution_count": 32, "metadata": {}, "output_type": "execute_result" } @@ -867,7 +867,7 @@ }, { "cell_type": "code", - "execution_count": 106, + "execution_count": 33, "metadata": {}, "outputs": [ { @@ -879,7 +879,7 @@ "{[c,c],[a,a,a]}" ] }, - "execution_count": 106, + "execution_count": 33, "metadata": {}, "output_type": "execute_result" } @@ -890,7 +890,7 @@ }, { "cell_type": "code", - "execution_count": 107, + "execution_count": 34, "metadata": {}, "outputs": [ { @@ -902,7 +902,7 @@ "{[c,c,c,c],[c,c,a,a,a],[a,a,b,c,c,c],[a,a,b,c,a,a,a]}" ] }, - "execution_count": 107, + "execution_count": 34, "metadata": {}, "output_type": "execute_result" } @@ -921,7 +921,7 @@ }, { "cell_type": "code", - "execution_count": 114, + "execution_count": 35, "metadata": {}, "outputs": [ { @@ -933,7 +933,7 @@ "{[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": 114, + "execution_count": 35, "metadata": {}, "output_type": "execute_result" } @@ -952,7 +952,7 @@ }, { "cell_type": "code", - "execution_count": 118, + "execution_count": 36, "metadata": {}, "outputs": [ { @@ -964,7 +964,7 @@ "{[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": 118, + "execution_count": 36, "metadata": {}, "output_type": "execute_result" } @@ -975,7 +975,7 @@ }, { "cell_type": "code", - "execution_count": 119, + "execution_count": 37, "metadata": {}, "outputs": [ { @@ -987,7 +987,7 @@ "{[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, + "execution_count": 37, "metadata": {}, "output_type": "execute_result" } @@ -998,7 +998,7 @@ }, { "cell_type": "code", - "execution_count": 129, + "execution_count": 38, "metadata": {}, "outputs": [], "source": [ @@ -1007,7 +1007,7 @@ }, { "cell_type": "code", - "execution_count": 130, + "execution_count": 39, "metadata": {}, "outputs": [], "source": [ @@ -1016,7 +1016,7 @@ }, { "cell_type": "code", - "execution_count": 131, + "execution_count": 40, "metadata": {}, "outputs": [], "source": [ @@ -1032,7 +1032,7 @@ }, { "cell_type": "code", - "execution_count": 132, + "execution_count": 41, "metadata": {}, "outputs": [ { @@ -1044,7 +1044,7 @@ "[c,b,a,a]" ] }, - "execution_count": 132, + "execution_count": 41, "metadata": {}, "output_type": "execute_result" } @@ -1062,19 +1062,19 @@ }, { "cell_type": "code", - "execution_count": 133, + "execution_count": 42, "metadata": {}, "outputs": [ { "data": { "text/markdown": [ - "$\\{[a,\\mathit{b},\\mathit{a},c],[c,\\mathit{b},\\mathit{a},a]\\}$" + "$\\{[c,c],[c,\\mathit{b},\\mathit{a},a]\\}$" ], "text/plain": [ - "{[a,b,a,c],[c,b,a,a]}" + "{[c,c],[c,b,a,a]}" ] }, - "execution_count": 133, + "execution_count": 42, "metadata": {}, "output_type": "execute_result" } @@ -1092,7 +1092,7 @@ }, { "cell_type": "code", - "execution_count": 134, + "execution_count": 43, "metadata": {}, "outputs": [ { @@ -1101,7 +1101,7 @@ "Loaded machine: Alphabet" ] }, - "execution_count": 134, + "execution_count": 43, "metadata": {}, "output_type": "execute_result" } @@ -1128,7 +1128,7 @@ }, { "cell_type": "code", - "execution_count": 135, + "execution_count": 44, "metadata": {}, "outputs": [ { @@ -1137,7 +1137,7 @@ "Machine constants set up using operation 0: $setup_constants()" ] }, - "execution_count": 135, + "execution_count": 44, "metadata": {}, "output_type": "execute_result" } @@ -1148,7 +1148,7 @@ }, { "cell_type": "code", - "execution_count": 136, + "execution_count": 45, "metadata": {}, "outputs": [ { @@ -1160,7 +1160,7 @@ "TRUE" ] }, - "execution_count": 136, + "execution_count": 45, "metadata": {}, "output_type": "execute_result" } @@ -1171,7 +1171,7 @@ }, { "cell_type": "code", - "execution_count": 137, + "execution_count": 46, "metadata": {}, "outputs": [ { @@ -1183,7 +1183,7 @@ "FALSE" ] }, - "execution_count": 137, + "execution_count": 46, "metadata": {}, "output_type": "execute_result" } @@ -1194,7 +1194,7 @@ }, { "cell_type": "code", - "execution_count": 138, + "execution_count": 47, "metadata": {}, "outputs": [ { @@ -1206,7 +1206,7 @@ "TRUE" ] }, - "execution_count": 138, + "execution_count": 47, "metadata": {}, "output_type": "execute_result" } @@ -1224,7 +1224,7 @@ }, { "cell_type": "code", - "execution_count": 139, + "execution_count": 48, "metadata": {}, "outputs": [ { @@ -1236,7 +1236,7 @@ "{[],[c],[c,b],[c,b,a],[c,b,a,a],[c,b,a,a,b]}" ] }, - "execution_count": 139, + "execution_count": 48, "metadata": {}, "output_type": "execute_result" } @@ -1247,7 +1247,7 @@ }, { "cell_type": "code", - "execution_count": 140, + "execution_count": 49, "metadata": {}, "outputs": [ { @@ -1259,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": 140, + "execution_count": 49, "metadata": {}, "output_type": "execute_result" } @@ -1270,7 +1270,7 @@ }, { "cell_type": "code", - "execution_count": 141, + "execution_count": 50, "metadata": {}, "outputs": [ { @@ -1282,7 +1282,7 @@ "{[],[a],[a,b],[b],[b,c],[c],[a,b,c]}" ] }, - "execution_count": 141, + "execution_count": 50, "metadata": {}, "output_type": "execute_result" } @@ -1293,7 +1293,7 @@ }, { "cell_type": "code", - "execution_count": 142, + "execution_count": 51, "metadata": {}, "outputs": [ { @@ -1302,7 +1302,7 @@ "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n" ] }, - "execution_count": 142, + "execution_count": 51, "metadata": {}, "output_type": "execute_result" } @@ -1313,7 +1313,7 @@ }, { "cell_type": "code", - "execution_count": 143, + "execution_count": 52, "metadata": {}, "outputs": [ { @@ -1322,180 +1322,209 @@ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", - "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n", + "<!-- Generated by graphviz version 2.44.1 (0)\n", " -->\n", "<!-- Title: state Pages: 1 -->\n", - "<svg width=\"414pt\" height=\"314pt\"\n", - " viewBox=\"0.00 0.00 413.60 314.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", - "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 310)\">\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", + "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n", "<title>state</title>\n", - "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-310 410.603,-310 410.603,5 -4,5\"/>\n", + "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-301 436.61,-301 436.61,4 -4,4\"/>\n", "<!-- [a,b,c] -->\n", - "<g id=\"node1\" class=\"node\"><title>[a,b,c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"192.606,-36 138.606,-36 138.606,-0 192.606,-0 192.606,-36\"/>\n", - "<text text-anchor=\"middle\" x=\"165.606\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,c]</text>\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", "</g>\n", "<!-- [a,b,c]->[a,b,c] -->\n", - "<g id=\"edge2\" class=\"edge\"><title>[a,b,c]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M192.846,-26.2419C202.629,-26.4192 210.606,-23.6719 210.606,-18 210.606,-14.5437 207.644,-12.1734 203.116,-10.8891\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"203.169,-7.3739 192.846,-9.75806 202.403,-14.3318 203.169,-7.3739\"/>\n", - "<text text-anchor=\"middle\" x=\"217.604\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [c] -->\n", - "<g id=\"node3\" class=\"node\"><title>[c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"67.6055,-216 13.6055,-216 13.6055,-180 67.6055,-180 67.6055,-216\"/>\n", - "<text text-anchor=\"middle\" x=\"40.6055\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[c]</text>\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", "</g>\n", "<!-- [c]->[a,b,c] -->\n", - "<g id=\"edge4\" class=\"edge\"><title>[c]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M38.2249,-179.963C35.9901,-157.532 35.2109,-117.703 52.6083,-90 70.0898,-62.1634 102.9,-43.3742 128.68,-32.1538\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"130.272,-35.283 138.17,-28.221 127.592,-28.8163 130.272,-35.283\"/>\n", - "<text text-anchor=\"middle\" x=\"60.6041\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [c]->[c] -->\n", - "<g id=\"edge6\" class=\"edge\"><title>[c]->[c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M67.8463,-206.242C77.6295,-206.419 85.6055,-203.672 85.6055,-198 85.6055,-194.544 82.6437,-192.173 78.116,-190.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"78.1694,-187.374 67.8463,-189.758 77.403,-194.332 78.1694,-187.374\"/>\n", - "<text text-anchor=\"middle\" x=\"92.6041\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [b,c] -->\n", - "<g id=\"node7\" class=\"node\"><title>[b,c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"129.606,-126 75.6055,-126 75.6055,-90 129.606,-90 129.606,-126\"/>\n", - "<text text-anchor=\"middle\" x=\"102.606\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[b,c]</text>\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", "</g>\n", "<!-- [c]->[b,c] -->\n", - "<g id=\"edge8\" class=\"edge\"><title>[c]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M52.8547,-179.614C61.9145,-166.755 74.3967,-149.038 84.5916,-134.568\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"87.6944,-136.241 90.5928,-126.05 81.972,-132.209 87.6944,-136.241\"/>\n", - "<text text-anchor=\"middle\" x=\"84.6041\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [b,c]->[a,b,c] -->\n", - "<g id=\"edge10\" class=\"edge\"><title>[b,c]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M115.052,-89.614C124.258,-76.7551 136.942,-59.0384 147.301,-44.5682\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"150.424,-46.2189 153.399,-36.0504 144.732,-42.1441 150.424,-46.2189\"/>\n", - "<text text-anchor=\"middle\" x=\"147.604\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [b,c]->[b,c] -->\n", - "<g id=\"edge12\" class=\"edge\"><title>[b,c]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M129.846,-116.242C139.629,-116.419 147.606,-113.672 147.606,-108 147.606,-104.544 144.644,-102.173 140.116,-100.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"140.169,-97.3739 129.846,-99.7581 139.403,-104.332 140.169,-97.3739\"/>\n", - "<text text-anchor=\"middle\" x=\"154.604\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [b] -->\n", - "<g id=\"node10\" class=\"node\"><title>[b]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"220.606,-216 166.606,-216 166.606,-180 220.606,-180 220.606,-216\"/>\n", - "<text text-anchor=\"middle\" x=\"193.606\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[b]</text>\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", "</g>\n", "<!-- [b]->[a,b,c] -->\n", - "<g id=\"edge14\" class=\"edge\"><title>[b]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M190.921,-179.933C186.05,-148.966 175.72,-83.2989 169.873,-46.1292\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"173.294,-45.3503 168.282,-36.0157 166.379,-46.4381 173.294,-45.3503\"/>\n", - "<text text-anchor=\"middle\" x=\"189.604\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [b]->[b,c] -->\n", - "<g id=\"edge16\" class=\"edge\"><title>[b]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M179.098,-179.68C169.884,-169.016 157.494,-155.278 145.606,-144 141.59,-140.191 137.209,-136.327 132.829,-132.626\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"134.967,-129.851 125.027,-126.185 130.51,-135.25 134.967,-129.851\"/>\n", - "<text text-anchor=\"middle\" x=\"169.604\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [b]->[b] -->\n", - "<g id=\"edge18\" class=\"edge\"><title>[b]->[b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M220.846,-206.242C230.629,-206.419 238.606,-203.672 238.606,-198 238.606,-194.544 235.644,-192.173 231.116,-190.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"231.169,-187.374 220.846,-189.758 230.403,-194.332 231.169,-187.374\"/>\n", - "<text text-anchor=\"middle\" x=\"245.604\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [a,b] -->\n", - "<g id=\"node15\" class=\"node\"><title>[a,b]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"282.606,-126 228.606,-126 228.606,-90 282.606,-90 282.606,-126\"/>\n", - "<text text-anchor=\"middle\" x=\"255.606\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\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", "</g>\n", "<!-- [b]->[a,b] -->\n", - "<g id=\"edge20\" class=\"edge\"><title>[b]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M205.855,-179.614C214.914,-166.755 227.397,-149.038 237.592,-134.568\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"240.694,-136.241 243.593,-126.05 234.972,-132.209 240.694,-136.241\"/>\n", - "<text text-anchor=\"middle\" x=\"237.604\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [a,b]->[a,b,c] -->\n", - "<g id=\"edge22\" class=\"edge\"><title>[a,b]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M242.644,-89.9856C234.067,-79.1861 222.285,-65.1893 210.606,-54 206.585,-50.1487 202.159,-46.3001 197.7,-42.6389\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"199.722,-39.7756 189.717,-36.2911 195.366,-45.2545 199.722,-39.7756\"/>\n", - "<text text-anchor=\"middle\" x=\"233.604\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [a,b]->[a,b] -->\n", - "<g id=\"edge24\" class=\"edge\"><title>[a,b]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M282.846,-116.242C292.629,-116.419 300.606,-113.672 300.606,-108 300.606,-104.544 297.644,-102.173 293.116,-100.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"293.169,-97.3739 282.846,-99.7581 292.403,-104.332 293.169,-97.3739\"/>\n", - "<text text-anchor=\"middle\" x=\"307.604\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [a] -->\n", - "<g id=\"node18\" class=\"node\"><title>[a]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"373.606,-216 319.606,-216 319.606,-180 373.606,-180 373.606,-216\"/>\n", - "<text text-anchor=\"middle\" x=\"346.606\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a]</text>\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", "</g>\n", "<!-- [a]->[a,b,c] -->\n", - "<g id=\"edge26\" class=\"edge\"><title>[a]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M347.226,-179.804C347.149,-156.832 343.725,-116.013 322.606,-90 292.574,-53.0088 239.137,-34.5634 203.044,-25.9056\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"203.427,-22.4042 192.902,-23.6194 201.888,-29.2328 203.427,-22.4042\"/>\n", - "<text text-anchor=\"middle\" x=\"346.604\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [a]->[a,b] -->\n", - "<g id=\"edge28\" class=\"edge\"><title>[a]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M332.098,-179.68C322.884,-169.016 310.494,-155.278 298.606,-144 294.59,-140.191 290.209,-136.327 285.829,-132.626\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"287.967,-129.851 278.027,-126.185 283.51,-135.25 287.967,-129.851\"/>\n", - "<text text-anchor=\"middle\" x=\"322.604\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [a]->[a] -->\n", - "<g id=\"edge30\" class=\"edge\"><title>[a]->[a]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M373.846,-206.242C383.629,-206.419 391.606,-203.672 391.606,-198 391.606,-194.544 388.644,-192.173 384.116,-190.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"384.169,-187.374 373.846,-189.758 383.403,-194.332 384.169,-187.374\"/>\n", - "<text text-anchor=\"middle\" x=\"398.604\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- [] -->\n", - "<g id=\"node22\" class=\"node\"><title>[]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"184.606,-306 130.606,-306 130.606,-270 184.606,-270 184.606,-306\"/>\n", - "<text text-anchor=\"middle\" x=\"157.606\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\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", "</g>\n", "<!-- []->[a,b,c] -->\n", - "<g id=\"edge32\" class=\"edge\"><title>[]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M130.501,-283.347C94.4995,-276.875 32.244,-259.674 4.60554,-216 -3.95044,-202.48 1.88589,-195.767 4.60554,-180 15.1162,-119.065 13.6017,-90.376 63.6055,-54 82.7738,-40.0558 107.931,-31.3434 128.465,-26.0986\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"129.507,-29.4484 138.425,-23.7286 127.887,-22.6385 129.507,-29.4484\"/>\n", - "<text text-anchor=\"middle\" x=\"17.6041\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- []->[c] -->\n", - "<g id=\"edge34\" class=\"edge\"><title>[]->[c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M131.92,-269.924C123.738,-264.338 114.711,-258.02 106.608,-252 94.0787,-242.69 80.5838,-231.982 69.0817,-222.638\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"71.0586,-219.733 61.1008,-216.115 66.6287,-225.153 71.0586,-219.733\"/>\n", - "<text text-anchor=\"middle\" x=\"114.604\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- []->[b,c] -->\n", - "<g id=\"edge36\" class=\"edge\"><title>[]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M152.332,-269.933C142.723,-238.833 122.299,-172.735 110.841,-135.652\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"114.159,-134.537 107.863,-126.016 107.471,-136.603 114.159,-134.537\"/>\n", - "<text text-anchor=\"middle\" x=\"142.604\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- []->[b] -->\n", - "<g id=\"edge38\" class=\"edge\"><title>[]->[b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M164.718,-269.614C169.879,-256.998 176.953,-239.705 182.809,-225.391\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"186.083,-226.631 186.63,-216.05 179.605,-223.981 186.083,-226.631\"/>\n", - "<text text-anchor=\"middle\" x=\"186.604\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- []->[a,b] -->\n", - "<g id=\"edge40\" class=\"edge\"><title>[]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M184.789,-276.902C209.602,-266.052 244.75,-246.188 260.606,-216 273.595,-191.27 269.62,-158.722 264.116,-136.045\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"267.416,-134.838 261.447,-126.084 260.654,-136.649 267.416,-134.838\"/>\n", - "<text text-anchor=\"middle\" x=\"276.604\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- []->[a] -->\n", - "<g id=\"edge42\" class=\"edge\"><title>[]->[a]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M184.732,-285.403C215.199,-282.528 265.145,-274.487 301.606,-252 312.923,-245.02 322.833,-234.234 330.451,-224.209\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"333.306,-226.234 336.291,-216.068 327.618,-222.153 333.306,-226.234\"/>\n", - "<text text-anchor=\"middle\" x=\"328.604\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "<!-- []->[] -->\n", - "<g id=\"edge44\" class=\"edge\"><title>[]->[]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M184.846,-296.242C194.629,-296.419 202.606,-293.672 202.606,-288 202.606,-284.544 199.644,-282.173 195.116,-280.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"195.169,-277.374 184.846,-279.758 194.403,-284.332 195.169,-277.374\"/>\n", - "<text text-anchor=\"middle\" x=\"209.604\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\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", "</g>\n", "</g>\n", "</svg>" @@ -1504,7 +1533,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": 143, + "execution_count": 52, "metadata": {}, "output_type": "execute_result" } @@ -1515,7 +1544,7 @@ }, { "cell_type": "code", - "execution_count": 144, + "execution_count": 53, "metadata": {}, "outputs": [ { @@ -1524,150 +1553,174 @@ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", - "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n", + "<!-- Generated by graphviz version 2.44.1 (0)\n", " -->\n", "<!-- Title: state Pages: 1 -->\n", - "<svg width=\"517pt\" height=\"314pt\"\n", - " viewBox=\"0.00 0.00 517.25 314.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", - "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 310)\">\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", + "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 301)\">\n", "<title>state</title>\n", - "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-310 514.25,-310 514.25,5 -4,5\"/>\n", + "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-301 553.67,-301 553.67,4 -4,4\"/>\n", "<!-- [a,b,c] -->\n", - "<g id=\"node1\" class=\"node\"><title>[a,b,c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"369.041,-36 315.041,-36 315.041,-0 369.041,-0 369.041,-36\"/>\n", - "<text text-anchor=\"middle\" x=\"342.041\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,c]</text>\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", "</g>\n", "<!-- [a,b,c]->[a,b,c] -->\n", - "<g id=\"edge2\" class=\"edge\"><title>[a,b,c]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M369.282,-26.2419C379.065,-26.4192 387.041,-23.6719 387.041,-18 387.041,-14.5437 384.079,-12.1734 379.551,-10.8891\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"379.605,-7.3739 369.282,-9.75806 378.838,-14.3318 379.605,-7.3739\"/>\n", - "<text text-anchor=\"middle\" x=\"404.145\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [c] -->\n", - "<g id=\"node3\" class=\"node\"><title>[c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"69.041,-216 15.041,-216 15.041,-180 69.041,-180 69.041,-216\"/>\n", - "<text text-anchor=\"middle\" x=\"42.041\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[c]</text>\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", "</g>\n", "<!-- [c]->[c] -->\n", - "<g id=\"edge4\" class=\"edge\"><title>[c]->[c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M69.2817,-206.242C79.0649,-206.419 87.041,-203.672 87.041,-198 87.041,-194.544 84.0792,-192.173 79.5515,-190.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"79.6048,-187.374 69.2817,-189.758 78.8385,-194.332 79.6048,-187.374\"/>\n", - "<text text-anchor=\"middle\" x=\"104.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [b,c] -->\n", - "<g id=\"node5\" class=\"node\"><title>[b,c]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"212.041,-126 158.041,-126 158.041,-90 212.041,-90 212.041,-126\"/>\n", - "<text text-anchor=\"middle\" x=\"185.041\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[b,c]</text>\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", "</g>\n", "<!-- [b,c]->[b,c] -->\n", - "<g id=\"edge6\" class=\"edge\"><title>[b,c]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M212.282,-116.242C222.065,-116.419 230.041,-113.672 230.041,-108 230.041,-104.544 227.079,-102.173 222.551,-100.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"222.605,-97.3739 212.282,-99.7581 221.838,-104.332 222.605,-97.3739\"/>\n", - "<text text-anchor=\"middle\" x=\"247.145\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [b] -->\n", - "<g id=\"node7\" class=\"node\"><title>[b]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"263.041,-216 209.041,-216 209.041,-180 263.041,-180 263.041,-216\"/>\n", - "<text text-anchor=\"middle\" x=\"236.041\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[b]</text>\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", "</g>\n", "<!-- [b]->[b,c] -->\n", - "<g id=\"edge8\" class=\"edge\"><title>[b]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M225.965,-179.614C218.583,-166.876 208.439,-149.372 200.097,-134.979\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"202.965,-132.947 194.922,-126.05 196.909,-136.457 202.965,-132.947\"/>\n", - "<text text-anchor=\"middle\" x=\"232.145\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [b]->[b] -->\n", - "<g id=\"edge10\" class=\"edge\"><title>[b]->[b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M263.282,-206.242C273.065,-206.419 281.041,-203.672 281.041,-198 281.041,-194.544 278.079,-192.173 273.551,-190.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"273.605,-187.374 263.282,-189.758 272.838,-194.332 273.605,-187.374\"/>\n", - "<text text-anchor=\"middle\" x=\"298.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [a,b] -->\n", - "<g id=\"node10\" class=\"node\"><title>[a,b]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"369.041,-126 315.041,-126 315.041,-90 369.041,-90 369.041,-126\"/>\n", - "<text text-anchor=\"middle\" x=\"342.041\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\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", "</g>\n", "<!-- [a,b]->[a,b,c] -->\n", - "<g id=\"edge12\" class=\"edge\"><title>[a,b]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M342.041,-89.614C342.041,-77.2403 342.041,-60.3686 342.041,-46.2198\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"345.541,-46.0504 342.041,-36.0504 338.541,-46.0504 345.541,-46.0504\"/>\n", - "<text text-anchor=\"middle\" x=\"359.145\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [a,b]->[a,b] -->\n", - "<g id=\"edge14\" class=\"edge\"><title>[a,b]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M369.282,-116.242C379.065,-116.419 387.041,-113.672 387.041,-108 387.041,-104.544 384.079,-102.173 379.551,-100.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"379.605,-97.3739 369.282,-99.7581 378.838,-104.332 379.605,-97.3739\"/>\n", - "<text text-anchor=\"middle\" x=\"404.145\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [a] -->\n", - "<g id=\"node13\" class=\"node\"><title>[a]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"457.041,-216 403.041,-216 403.041,-180 457.041,-180 457.041,-216\"/>\n", - "<text text-anchor=\"middle\" x=\"430.041\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a]</text>\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", "</g>\n", "<!-- [a]->[a,b,c] -->\n", - "<g id=\"edge16\" class=\"edge\"><title>[a]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M434.497,-179.653C439.203,-157.582 444.17,-118.865 430.041,-90 419.039,-67.5242 397.174,-49.8272 377.992,-37.7228\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"379.788,-34.7189 369.416,-32.5577 376.177,-40.7153 379.788,-34.7189\"/>\n", - "<text text-anchor=\"middle\" x=\"455.145\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [a]->[a,b] -->\n", - "<g id=\"edge18\" class=\"edge\"><title>[a]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M412.655,-179.614C399.432,-166.391 381.073,-148.032 366.389,-133.348\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"368.637,-130.647 359.091,-126.05 363.688,-135.596 368.637,-130.647\"/>\n", - "<text text-anchor=\"middle\" x=\"410.145\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [a]->[a] -->\n", - "<g id=\"edge20\" class=\"edge\"><title>[a]->[a]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M457.282,-206.242C467.065,-206.419 475.041,-203.672 475.041,-198 475.041,-194.544 472.079,-192.173 467.551,-190.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"467.605,-187.374 457.282,-189.758 466.838,-194.332 467.605,-187.374\"/>\n", - "<text text-anchor=\"middle\" x=\"492.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- [] -->\n", - "<g id=\"node17\" class=\"node\"><title>[]</title>\n", - "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"212.041,-306 158.041,-306 158.041,-270 212.041,-270 212.041,-306\"/>\n", - "<text text-anchor=\"middle\" x=\"185.041\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\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", "</g>\n", "<!-- []->[a,b,c] -->\n", - "<g id=\"edge22\" class=\"edge\"><title>[]->[a,b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M157.63,-282.904C99.3364,-272.892 -28.8745,-243.23 6.04098,-180 67.136,-69.3606 230.704,-33.8217 304.731,-23.1954\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"305.543,-26.6173 314.981,-21.8024 304.6,-19.6811 305.543,-26.6173\"/>\n", - "<text text-anchor=\"middle\" x=\"47.1455\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- []->[c] -->\n", - "<g id=\"edge24\" class=\"edge\"><title>[]->[c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M157.781,-276.366C142.874,-270.09 124.341,-261.523 108.832,-252 94.8927,-243.441 80.5428,-232.396 68.734,-222.606\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"70.899,-219.854 61.0008,-216.075 66.3823,-225.202 70.899,-219.854\"/>\n", - "<text text-anchor=\"middle\" x=\"126.145\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- []->[b,c] -->\n", - "<g id=\"edge26\" class=\"edge\"><title>[]->[b,c]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M178.998,-269.755C174.353,-255.537 168.321,-234.734 165.832,-216 163.724,-200.139 163.724,-195.861 165.832,-180 167.796,-165.218 171.966,-149.147 175.92,-136.04\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"179.339,-136.834 178.998,-126.245 172.661,-134.735 179.339,-136.834\"/>\n", - "<text text-anchor=\"middle\" x=\"183.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- []->[b] -->\n", - "<g id=\"edge28\" class=\"edge\"><title>[]->[b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M195.117,-269.614C202.499,-256.876 212.643,-239.372 220.985,-224.979\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"224.173,-226.457 226.159,-216.05 218.117,-222.947 224.173,-226.457\"/>\n", - "<text text-anchor=\"middle\" x=\"232.145\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- []->[a,b] -->\n", - "<g id=\"edge30\" class=\"edge\"><title>[]->[a,b]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M212.058,-281C244.137,-272.383 296.724,-253.261 324.041,-216 340.867,-193.049 344.103,-159.922 343.928,-136.623\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"347.419,-136.266 343.629,-126.373 340.422,-136.47 347.419,-136.266\"/>\n", - "<text text-anchor=\"middle\" x=\"356.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- []->[a] -->\n", - "<g id=\"edge32\" class=\"edge\"><title>[]->[a]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M212.234,-285.824C248.626,-283.354 314.445,-275.699 365.041,-252 380.147,-244.924 394.75,-233.568 406.275,-223.178\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"408.818,-225.592 413.731,-216.205 404.036,-220.48 408.818,-225.592\"/>\n", - "<text text-anchor=\"middle\" x=\"409.145\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "<!-- []->[] -->\n", - "<g id=\"edge34\" class=\"edge\"><title>[]->[]</title>\n", - "<path fill=\"none\" stroke=\"firebrick\" d=\"M212.282,-296.242C222.065,-296.419 230.041,-293.672 230.041,-288 230.041,-284.544 227.079,-282.173 222.551,-280.889\"/>\n", - "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"222.605,-277.374 212.282,-279.758 221.838,-284.332 222.605,-277.374\"/>\n", - "<text text-anchor=\"middle\" x=\"247.145\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\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", "</g>\n", "</g>\n", "</svg>" @@ -1676,7 +1729,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": 144, + "execution_count": 53, "metadata": {}, "output_type": "execute_result" } @@ -1687,7 +1740,7 @@ }, { "cell_type": "code", - "execution_count": 145, + "execution_count": 54, "metadata": {}, "outputs": [], "source": [ @@ -1696,10 +1749,157 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 63, "metadata": {}, - "outputs": [], - "source": [] + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: FormaleSprachen" + ] + }, + "execution_count": 63, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "MACHINE FormaleSprachen\n", + "/* 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", + "ABSTRACT_CONSTANTS\n", + " kat, Worte, Sprachen, kleene, sp, teilwort, praefix\n", + "CONSTANTS\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", + "ASSERTIONS\n", + " card(L1L2) = 4\n", + "END" + ] + }, + { + "cell_type": "code", + "execution_count": 66, + "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" + ] + } + ], + "source": [ + ":init" + ] + }, + { + "cell_type": "code", + "execution_count": 67, + "metadata": {}, + "outputs": [ + { + "ename": "CommandExecutionException", + "evalue": ":eval: NOT-INITIALISED", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[31m:eval: NOT-INITIALISED\u001b[0m" + ] + } + ], + "source": [ + "kleene(L1, 2)" + ] } ], "metadata": {