diff --git a/info4/kapitel-3/PDA-Kellerautomaten.ipynb b/info4/kapitel-3/PDA-Kellerautomaten.ipynb
index 2b8746cea8548a6ccf097377c821834e2c118497..d2f8a3452066adbea33a42fd926cb9de0dc380ce 100644
--- a/info4/kapitel-3/PDA-Kellerautomaten.ipynb
+++ b/info4/kapitel-3/PDA-Kellerautomaten.ipynb
@@ -31,7 +31,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 59,
+   "execution_count": 1,
    "metadata": {},
    "outputs": [
     {
@@ -40,7 +40,7 @@
        "Loaded machine: PDA"
       ]
      },
-     "execution_count": 59,
+     "execution_count": 1,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -53,16 +53,18 @@
     " Z = {z0,z1}; // die Zustände des Automaten, z0 ist der Startzustand\n",
     " SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/\n",
     "DEFINITIONS\n",
-    " Σ == {a,b};   // das Eingabe-Alphabet\n",
-    " Γ == {A,BOT}; // das Kelleralphabet\n",
     " \n",
     " ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};\n",
     " ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);\n",
     " ANIMATION_FUNCTION1 == {(1,0,\"z: \"),(2,0,\"α:\"),(3,0,\"γ:\")};\n",
     " ANIMATION_STR_JUSTIFY_LEFTx == TRUE;\n",
     " SET_PREF_PP_SEQUENCES == TRUE\n",
-    "CONSTANTS δ\n",
+    "CONSTANTS δ, Σ, Γ\n",
     "PROPERTIES\n",
+    " Σ = {a,b}    // das Eingabe-Alphabet\n",
+    " ∧\n",
+    " Γ = {A,BOT} // das Kelleralphabet\n",
+    " ∧\n",
     " /* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */\n",
     " δ = {     (z0,a,BOT)      ↦  (z0,[A,BOT]),\n",
     "           (z0,a,A)        ↦  (z0,[A,A]),\n",
@@ -104,7 +106,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 60,
+   "execution_count": 2,
    "metadata": {},
    "outputs": [
     {
@@ -113,7 +115,7 @@
        "Machine constants set up using operation 0: $setup_constants()"
       ]
      },
-     "execution_count": 60,
+     "execution_count": 2,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -124,7 +126,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 61,
+   "execution_count": 3,
    "metadata": {},
    "outputs": [
     {
@@ -133,7 +135,7 @@
        "Machine initialised using operation 1: $initialise_machine()"
       ]
      },
-     "execution_count": 61,
+     "execution_count": 3,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -144,7 +146,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 62,
+   "execution_count": 4,
    "metadata": {},
    "outputs": [
     {
@@ -178,7 +180,7 @@
        "<Animation function visualisation>"
       ]
      },
-     "execution_count": 62,
+     "execution_count": 4,
      "metadata": {},
      "output_type": "execute_result"
     }