diff --git a/info4/kapitel-2/Abschlusseigenschaften.ipynb b/info4/kapitel-2/Abschlusseigenschaften.ipynb
index ec52f0e340d288eef230aa14b3a8f22b399894da..971401daafeae9593dc7b667acf3e2985416f5eb 100644
--- a/info4/kapitel-2/Abschlusseigenschaften.ipynb
+++ b/info4/kapitel-2/Abschlusseigenschaften.ipynb
@@ -97,8 +97,8 @@
" \n",
" \n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
- " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:F); // Endzustände\n",
- " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z\\F); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes∈F); // Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes∈Z\\F); // andere Zustände\n",
" CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
" CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,y|y∈δ(x,0) ∧ y∉δ(x,1)}); \n",
" CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,y|y∈δ(x,1) ∧ y∉δ(x,0)});\n",
@@ -332,12 +332,13 @@
" z_start ∈ Z ∧\n",
" F ⊆ Z\n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
- " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:Z\\F); // Endzustände von M2\n",
- " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:F); // andere Zustände von M2\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes∈Z\\F); // Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes∈F); // andere Zustände\n",
" CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
- " CUSTOM_GRAPH_EDGES1 == rec(color:\"red\",label:\"0\",edges:{a,b|(a,0)|->b:δ}); \n",
- " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{a,b|(a,1)|->b:δ});\n",
- " CUSTOM_GRAPH_EDGES3 == rec(color:\"black\",label:\"\",edges:{\"\" |-> z_start}) // Kante für den Startknoten\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,y|y=δ(x,0) ∧ y≠δ(x,1)}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,y|y=δ(x,1) ∧ y≠ δ(x,0)});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"0, 1\",edges:{x,y|y=δ(x,0) ∧ y=δ(x,1)});\n",
+ " CUSTOM_GRAPH_EDGES4 == rec(color:\"black\",label:\"\",edges:{\"\" ↦ z_start}) // Kante für den Startknoten\n",
"END"
]
},
@@ -396,101 +397,87 @@
" -->\n",
"<!-- Title: prob_graph Pages: 1 -->\n",
"<svg width=\"540pt\" height=\"716pt\"\n",
- " viewBox=\"0.00 0.00 540.00 716.05\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ " viewBox=\"0.00 0.00 540.00 715.65\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(0.98 0.98) rotate(0) translate(4 725.95)\">\n",
"<title>prob_graph</title>\n",
- "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-725.95 546.49,-725.95 546.49,4 -4,4\"/>\n",
+ "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-725.95 546.79,-725.95 546.79,4 -4,4\"/>\n",
"<!-- 0 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>0</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"189.65\" cy=\"-282\" rx=\"18.44\" ry=\"18.44\"/>\n",
- "<ellipse fill=\"none\" stroke=\"black\" cx=\"189.65\" cy=\"-282\" rx=\"22.44\" ry=\"22.44\"/>\n",
- "<text text-anchor=\"middle\" x=\"189.65\" y=\"-278.9\" font-family=\"Times,serif\" font-size=\"12.00\">z1</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"180.73\" cy=\"-282\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"180.73\" cy=\"-282\" rx=\"22.44\" ry=\"22.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"180.73\" y=\"-278.9\" font-family=\"Times,serif\" font-size=\"12.00\">z1</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"344.65\" cy=\"-54\" rx=\"18.44\" ry=\"18.44\"/>\n",
- "<ellipse fill=\"none\" stroke=\"black\" cx=\"344.65\" cy=\"-54\" rx=\"22.44\" ry=\"22.44\"/>\n",
- "<text text-anchor=\"middle\" x=\"344.65\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">z3</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"353.73\" cy=\"-54\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<ellipse fill=\"none\" stroke=\"black\" cx=\"353.73\" cy=\"-54\" rx=\"22.44\" ry=\"22.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"353.73\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">z3</text>\n",
"</g>\n",
"<!-- 0->1 -->\n",
- "<g id=\"edge6\" class=\"edge\">\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
"<title>0->1</title>\n",
- "<path fill=\"none\" stroke=\"red\" d=\"M202.07,-262.89C229.4,-223.03 294.85,-127.61 326.67,-81.22\"/>\n",
- "<polygon fill=\"red\" stroke=\"red\" points=\"329.61,-83.11 332.38,-72.89 323.84,-79.15 329.61,-83.11\"/>\n",
- "<text text-anchor=\"middle\" x=\"270.65\" y=\"-164.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M194.02,-263.64C224.34,-224.04 298.72,-126.87 334.24,-80.47\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"337.1,-82.49 340.4,-72.42 331.54,-78.23 337.1,-82.49\"/>\n",
+ "<text text-anchor=\"middle\" x=\"270.73\" y=\"-164.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>3</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"48.65\" cy=\"-54\" rx=\"18.44\" ry=\"18.44\"/>\n",
- "<text text-anchor=\"middle\" x=\"48.65\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">z2</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"54.73\" cy=\"-54\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"54.73\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">z2</text>\n",
"</g>\n",
"<!-- 0->3 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0->3</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M178.11,-262.51C152.63,-221.67 91.62,-123.87 63.41,-78.66\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"66.33,-76.73 58.07,-70.1 60.39,-80.44 66.33,-76.73\"/>\n",
- "<text text-anchor=\"middle\" x=\"122.65\" y=\"-164.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M170.21,-262.12C147.46,-221.31 93.72,-124.93 68.39,-79.5\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"71.36,-77.64 63.44,-70.61 65.25,-81.05 71.36,-77.64\"/>\n",
+ "<text text-anchor=\"middle\" x=\"121.73\" y=\"-164.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
"</g>\n",
"<!-- 1->1 -->\n",
- "<g id=\"edge4\" class=\"edge\">\n",
- "<title>1->1</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M365.05,-64.31C375.6,-65.9 385.12,-62.46 385.12,-54 385.12,-48.45 381.02,-45.06 375.22,-43.83\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"375.1,-40.33 365.05,-43.69 375,-47.33 375.1,-40.33\"/>\n",
- "<text text-anchor=\"middle\" x=\"389.12\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
- "</g>\n",
- "<!-- 1->1 -->\n",
- "<g id=\"edge8\" class=\"edge\">\n",
+ "<g id=\"edge7\" class=\"edge\">\n",
"<title>1->1</title>\n",
- "<path fill=\"none\" stroke=\"red\" d=\"M361.11,-69.52C380.5,-80.88 403.12,-75.71 403.12,-54 403.12,-35.68 387.01,-29.14 370.34,-34.37\"/>\n",
- "<polygon fill=\"red\" stroke=\"red\" points=\"368.82,-31.21 361.11,-38.48 371.67,-37.6 368.82,-31.21\"/>\n",
- "<text text-anchor=\"middle\" x=\"407.12\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M367.83,-71.57C380.56,-80.12 394.2,-74.26 394.2,-54 394.2,-38.8 386.53,-31.71 377.32,-32.72\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"375.87,-29.53 367.83,-36.43 378.42,-36.05 375.87,-29.53\"/>\n",
+ "<text text-anchor=\"middle\" x=\"405.7\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2</title>\n",
- "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"267.65\" cy=\"-500\" rx=\"18.44\" ry=\"18.44\"/>\n",
- "<text text-anchor=\"middle\" x=\"267.65\" y=\"-496.9\" font-family=\"Times,serif\" font-size=\"12.00\">z0</text>\n",
+ "<ellipse fill=\"lightgrey\" stroke=\"black\" cx=\"266.73\" cy=\"-500\" rx=\"18.44\" ry=\"18.44\"/>\n",
+ "<text text-anchor=\"middle\" x=\"266.73\" y=\"-496.9\" font-family=\"Times,serif\" font-size=\"12.00\">z0</text>\n",
"</g>\n",
"<!-- 2->0 -->\n",
- "<g id=\"edge5\" class=\"edge\">\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
"<title>2->0</title>\n",
- "<path fill=\"none\" stroke=\"red\" d=\"M261.66,-482.41C248.53,-446.06 217.07,-358.95 200.42,-312.82\"/>\n",
- "<polygon fill=\"red\" stroke=\"red\" points=\"203.69,-311.58 197,-303.37 197.11,-313.96 203.69,-311.58\"/>\n",
- "<text text-anchor=\"middle\" x=\"234.65\" y=\"-392.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M260.13,-482.41C245.62,-445.96 210.79,-358.5 192.47,-312.47\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"195.66,-311.04 188.71,-303.05 189.16,-313.63 195.66,-311.04\"/>\n",
+ "<text text-anchor=\"middle\" x=\"229.73\" y=\"-392.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
"</g>\n",
"<!-- 2->1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>2->1</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M270.67,-481.59C282.28,-414.64 324.16,-173.14 339.21,-86.34\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"342.69,-86.76 340.95,-76.31 335.79,-85.57 342.69,-86.76\"/>\n",
- "<text text-anchor=\"middle\" x=\"312.65\" y=\"-278.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
- "</g>\n",
- "<!-- 3->3 -->\n",
- "<g id=\"edge3\" class=\"edge\">\n",
- "<title>3->3</title>\n",
- "<path fill=\"none\" stroke=\"green\" d=\"M64.39,-63.75C74.89,-66.49 85.12,-63.24 85.12,-54 85.12,-47.94 80.71,-44.45 74.72,-43.55\"/>\n",
- "<polygon fill=\"green\" stroke=\"green\" points=\"74.13,-40.08 64.39,-44.25 74.61,-47.07 74.13,-40.08\"/>\n",
- "<text text-anchor=\"middle\" x=\"89.12\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M270.14,-481.59C283.26,-414.64 330.58,-173.14 347.59,-86.34\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"351.07,-86.8 349.56,-76.31 344.2,-85.45 351.07,-86.8\"/>\n",
+ "<text text-anchor=\"middle\" x=\"316.73\" y=\"-278.9\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
"</g>\n",
"<!-- 3->3 -->\n",
- "<g id=\"edge7\" class=\"edge\">\n",
+ "<g id=\"edge6\" class=\"edge\">\n",
"<title>3->3</title>\n",
- "<path fill=\"none\" stroke=\"red\" d=\"M61.23,-67.64C79.83,-81.37 103.12,-76.82 103.12,-54 103.12,-34.74 86.54,-28.5 70.19,-35.26\"/>\n",
- "<polygon fill=\"red\" stroke=\"red\" points=\"68.19,-32.37 61.23,-40.36 71.65,-38.46 68.19,-32.37\"/>\n",
- "<text text-anchor=\"middle\" x=\"107.12\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">0</text>\n",
+ "<path fill=\"none\" stroke=\"green\" d=\"M65.19,-69.69C77.24,-80.83 91.2,-75.6 91.2,-54 91.2,-37.46 83.02,-30.52 73.77,-33.17\"/>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"71.97,-30.17 65.19,-38.31 75.56,-36.18 71.97,-30.17\"/>\n",
+ "<text text-anchor=\"middle\" x=\"102.7\" y=\"-50.9\" font-family=\"Times,serif\" font-size=\"12.00\">0, 1</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>4</title>\n",
"</g>\n",
"<!-- 4->2 -->\n",
- "<g id=\"edge9\" class=\"edge\">\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
"<title>4->2</title>\n",
- "<path fill=\"none\" stroke=\"black\" d=\"M267.65,-659.8C267.65,-629.26 267.65,-565.3 267.65,-528.56\"/>\n",
- "<polygon fill=\"black\" stroke=\"black\" points=\"271.15,-528.53 267.65,-518.53 264.15,-528.53 271.15,-528.53\"/>\n",
+ "<path fill=\"none\" stroke=\"black\" d=\"M266.73,-659.8C266.73,-629.26 266.73,-565.3 266.73,-528.56\"/>\n",
+ "<polygon fill=\"black\" stroke=\"black\" points=\"270.23,-528.53 266.73,-518.53 263.23,-528.53 270.23,-528.53\"/>\n",
"</g>\n",
"</g>\n",
"</svg>"
@@ -579,8 +566,8 @@
" (zustand∈Z2 ∧ menge = δ2(zustand,symbol))))}\n",
" \n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
- " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:F); // Endzustände\n",
- " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z\\F); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes∈F); // Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes∈Z\\F); // andere Zustände\n",
" CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
" CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,y|y∈δ(x,0) ∧ y∉δ(x,1)}); \n",
" CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,y|y∈δ(x,1) ∧ y∉δ(x,0)});\n",
@@ -877,12 +864,12 @@
" (zustand∈Z2 ∧ menge = δ2(zustand,symbol) ∪ S2 ∧ δ2(zustand,symbol)∩F2 ≠ ∅)))}\n",
" \n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
- " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:F2); // Endzustände\n",
- " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z2\\F2); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes∈F2); // Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes∈Z2\\F2); // andere Zustände\n",
" CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
- " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,y|{(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∉δ(x,1)}); \n",
- " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,y|{(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,1) ∧ y∉δ(x,0)});\n",
- " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"0, 1\",edges:{x,y|{(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∈δ(x,1)});\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,y|{(x,0),(x,1)} ⊆dom(δ) ∧ y∈δ(x,0) ∧ y∉δ(x,1)}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,y|{(x,0),(x,1)} ⊆dom(δ) ∧ y∈δ(x,1) ∧ y∉δ(x,0)});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"0, 1\",edges:{x,y|{(x,0),(x,1)} ⊆dom(δ) ∧ y∈δ(x,0) ∧ y∈δ(x,1)});\n",
" CUSTOM_GRAPH_EDGES4 == rec(color:\"black\",label:\"\",edges:{\"\"}*S2) // Kanten für Startknoten\n",
"END"
]
@@ -1144,13 +1131,13 @@
"\n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
" \"LibraryStrings.def\";\n",
- " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:{x | ∃y.(x=TO_STRING(y) ∧ y:F)}); //Endzustände\n",
- " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:{x | ∃y.(x=TO_STRING(y) ∧ y:Z_gesamt\\F)}); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:{x | ∃y.(x=TO_STRING(y) ∧ y∈F)}); //Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:{x | ∃y.(x=TO_STRING(y) ∧ y∈Z_gesamt\\F)}); // andere Zustände\n",
" CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
- " CUSTOM_GRAPH_EDGES1 == rec(color:\"black\",label:\"\",edges:{\"\"}*{x | ∃y.(x=TO_STRING(y) ∧ y:S)}); // Kanten für Startknoten\n",
- " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"0\",edges:{a,b|∃x,y.({(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∉δ(x,1) ∧ a=TO_STRING(x) ∧ b=TO_STRING(y))}); \n",
- " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"1\",edges:{a,b|∃x,y.({(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,1) ∧ y∉δ(x,0) ∧ a=TO_STRING(x) ∧ b=TO_STRING(y))});\n",
- " CUSTOM_GRAPH_EDGES4 == rec(color:\"green\",label:\"0, 1\",edges:{a,b|∃x,y.({(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∈δ(x,1)∧ a=TO_STRING(x) ∧ b=TO_STRING(y))})\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"black\",label:\"\",edges:{\"\"}*{x | ∃y.(x=TO_STRING(y) ∧ y∈S)}); // Kanten für Startknoten\n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"0\",edges:{a,b|∃x,y.({(x,0),(x,1)} ⊆dom(δ) ∧ y∈δ(x,0) ∧ y∉δ(x,1) ∧ a=TO_STRING(x) ∧ b=TO_STRING(y))}); \n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"1\",edges:{a,b|∃x,y.({(x,0),(x,1)} ⊆dom(δ) ∧ y∈δ(x,1) ∧ y∉δ(x,0) ∧ a=TO_STRING(x) ∧ b=TO_STRING(y))});\n",
+ " CUSTOM_GRAPH_EDGES4 == rec(color:\"green\",label:\"0, 1\",edges:{a,b|∃x,y.({(x,0),(x,1)} ⊆dom(δ) ∧ y∈δ(x,0) ∧ y∈δ(x,1)∧ a=TO_STRING(x) ∧ b=TO_STRING(y))})\n",
"END"
]
},
@@ -1484,13 +1471,13 @@
" \n",
"DEFINITIONS // Für den Zustandsgraphen:\n",
" \"LibraryStrings.def\";\n",
- " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:{x | ∃y.(x=TO_STRING(y) ∧ y:F)}); //Endzustände\n",
- " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:{x | ∃y.(x=TO_STRING(y) ∧ y:Z_gesamt\\F)}); // andere Zustände\n",
+ " CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:{x | ∃y.(x=TO_STRING(y) ∧ y∈F)}); //Endzustände\n",
+ " CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:{x | ∃y.(x=TO_STRING(y) ∧ y∈Z_gesamt\\F)}); // andere Zustände\n",
" CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
- " CUSTOM_GRAPH_EDGES1 == rec(color:\"black\",label:\"\",edges:{\"\"}*{x | ∃y.(x=TO_STRING(y) ∧ y:S)}); // Kanten für Startknoten\n",
- " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"0\",edges:{a,b|∃x,y.({(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∉δ(x,1) ∧ a=TO_STRING(x) ∧ b=TO_STRING(y))}); \n",
- " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"1\",edges:{a,b|∃x,y.({(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,1) ∧ y∉δ(x,0) ∧ a=TO_STRING(x) ∧ b=TO_STRING(y))});\n",
- " CUSTOM_GRAPH_EDGES4 == rec(color:\"green\",label:\"0, 1\",edges:{a,b|∃x,y.({(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∈δ(x,1)∧ a=TO_STRING(x) ∧ b=TO_STRING(y))})\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"black\",label:\"\",edges:{\"\"}*{x | ∃y.(x=TO_STRING(y) ∧ y∈S)}); // Kanten für Startknoten\n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"0\",edges:{a,b|∃x,y.({(x,0),(x,1)} ⊆dom(δ) ∧ y∈δ(x,0) ∧ y∉δ(x,1) ∧ a=TO_STRING(x) ∧ b=TO_STRING(y))}); \n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"1\",edges:{a,b|∃x,y.({(x,0),(x,1)} ⊆dom(δ) ∧ y∈δ(x,1) ∧ y∉δ(x,0) ∧ a=TO_STRING(x) ∧ b=TO_STRING(y))});\n",
+ " CUSTOM_GRAPH_EDGES4 == rec(color:\"green\",label:\"0, 1\",edges:{a,b|∃x,y.({(x,0),(x,1)} ⊆dom(δ) ∧ y∈δ(x,0) ∧ y∈δ(x,1)∧ a=TO_STRING(x) ∧ b=TO_STRING(y))})\n",
"END"
]
},
@@ -1788,9 +1775,9 @@
" CUSTOM_GRAPH_NODES1 == rec(shape:\"doublecircle\",nodes:{z_start}); // Endzustände\n",
" CUSTOM_GRAPH_NODES2 == rec(shape:\"circle\",nodes:Z\\{z_start}); // andere Zustände\n",
" CUSTOM_GRAPH_NODES3 == rec(shape:\"none\",color:\"white\",style:\"none\",nodes:{\"\"});\n",
- " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∉δ2[{(x,1)}] ∧ z:y)}); \n",
- " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,z| ∃y.(y∈δ2[{(x,1)}] ∧ y∉δ2[{(x,0)}] ∧ z:y)});\n",
- " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"0, 1\",edges:{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∈δ2[{(x,1)}] ∧ z:y)});\n",
+ " CUSTOM_GRAPH_EDGES1 == rec(color:\"green\",label:\"0\",edges:{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∉δ2[{(x,1)}] ∧ z∈y)}); \n",
+ " CUSTOM_GRAPH_EDGES2 == rec(color:\"green\",label:\"1\",edges:{x,z| ∃y.(y∈δ2[{(x,1)}] ∧ y∉δ2[{(x,0)}] ∧ z∈y)});\n",
+ " CUSTOM_GRAPH_EDGES3 == rec(color:\"green\",label:\"0, 1\",edges:{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∈δ2[{(x,1)}] ∧ z∈y)});\n",
" CUSTOM_GRAPH_EDGES4 == rec(color:\"black\",label:\"\",edges:{\"\"}*F) // Kanten für Startknoten\n",
"END"
]
@@ -1963,7 +1950,7 @@
"source": [
"Mit Hilfe der Abschlusseigenschaften für reguläre Sprachen kann man zeigen, dass eine Sprache\n",
"1. regulär ist\n",
- "2. nicht regulär ist\n",
+ "2. nicht regulär ist (über Beweis mit Widerspruch)\n",
"\n",
"Um zu zeigen, dass eine Sprache regulär ist, findet man zwei (oder eine) reguläre Sprachen, die mit Hilfe einer oder mehrerer der oben angegebenen Operationen die gewünschte Sprache ergeben.\n",
"\n",
@@ -1971,7 +1958,7 @@
"\n",
"Dabei muss man allerdings beachten, dass $L_1$ und $L_2$ unabhängig voneinander sind. Man kann nicht $L_1=\\{0^n\\}$ und $L_2=\\{1^n\\}$ wählen und damit zeigen, dass $L_3=L_1L_2=\\{0^n1^n\\}$ regulär ist. Dabei wurde die Konkatenation falsch verwendet. In diesem Fall wäre $L_3=L_1L_2=\\{0^m1^n\\}=L$, was wie oben beschrieben regulär ist.\n",
"\n",
- "Um zu zeigen, dass eine Sprache $L$ nicht regulär ist, wählt man eine nicht reguläre Sprache $L_1$ und ggf. eine reguläre Sprache $L_2$ und führt diese mit Hilfe der Operationen auf $L$ zurück. Man zeigt also z.B. dass $L_2∩L=L_1$ gilt. Da $L_2$ regulär ist und die regulären Sprachen abgeschlossen bezüglich des Schnittes zweier Sprachen sind, müsste $L_1$ auch reulär sein, wenn $L$ regulär wäre. Da $L_1$ aber nach Voraussetzung nicht regulär ist, kann $L$ ebenfalls nicht regulär sein. Ein konkretes Beispiel hierfür ist $L=\\{x∈\\{0,1\\}^*|\\text{x hat gleich viele 0en und 1en}\\}$, $L_1=\\{0^n1^n\\}$ und $L_2=L(0^*1^*)$. Aus der Vorlesung ist bekannt, dass $L_1$ nicht regulär und $L_2$ regulär ist. Außerdem gilt $L_2∩L=L_1$. Daher kann L nicht regulär sein."
+ "Um zu zeigen, dass eine Sprache $L$ nicht regulär ist, nimmt man für einen Widerspruchsbeweis an, dass $L$ regulär sei. Dann wählt man eine nicht reguläre Sprache $L_1$ und ggf. eine reguläre Sprache $L_2$ und führt mit Hilfe der Operationen $L$ und ggf. $L_2$ auf $L_1$ zurück. Man zeigt also z.B. dass $L_2∩L=L_1$ gilt. Da $L_2$ regulär ist und die regulären Sprachen abgeschlossen bezüglich des Schnittes zweier Sprachen sind, müsste $L_1$ auch reulär sein, wenn $L$ regulär wäre. Da $L_1$ aber nach Voraussetzung nicht regulär ist, kann $L$ nicht regulär gewesen sein. Das ist ein Wiederspruch zur Annahme und somit ist $L$ nicht regulär. Ein konkretes Beispiel hierfür ist $L=\\{x∈\\{0,1\\}^*|\\text{x hat gleich viele 0en und 1en}\\}$, $L_1=\\{0^n1^n\\}$ und $L_2=L(0^*1^*)$. Aus der Vorlesung ist bekannt, dass $L_1$ nicht regulär und $L_2$ regulär ist. Außerdem gilt $L_2∩L=L_1$. Daher kann L nicht regulär sein."
]
}
],