diff --git a/info4/kapitel-3/PDA_nach_kfG.ipynb b/info4/kapitel-3/PDA_nach_kfG.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..a93094d9c6be41f6df863c38cc7bcbab31d446dc
--- /dev/null
+++ b/info4/kapitel-3/PDA_nach_kfG.ipynb
@@ -0,0 +1,228 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# PDA nach kfG\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: PDA_to_CFG"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE PDA_to_CFG\n",
+ "/* Translating a PDA to a CFG */\n",
+ "SETS\n",
+ " STATES = {z0,z1, symbol};\n",
+ " SYMBOLS={a,b, A, BOT, lambda, S} /* BOT = # = bottom of stack*/\n",
+ "DEFINITIONS\n",
+ " CFG_Alphabet == (STATES*(SYMBOLS-{lambda})*STATES);\n",
+ " Σ == {a,b};\n",
+ " Γ == {A,BOT};\n",
+ " ANIMATION_FUNCTION1 == {r,c,i| r=1 ∧ c∈dom(cur) ∧ i=prj1(STATES,SYMBOLS)(prj1(STATES*SYMBOLS,STATES)(cur(c)))};\n",
+ " ANIMATION_FUNCTION2 == {r,c,i| r=2 ∧ c∈dom(cur) ∧ i=prj2(STATES,SYMBOLS)(prj1(STATES*SYMBOLS,STATES)(cur(c)))};\n",
+ " ANIMATION_FUNCTION3 == {r,c,i| r=3 ∧ c∈dom(cur) ∧ i=prj2(STATES*SYMBOLS,STATES)(cur(c))};\n",
+ " ANIMATION_STR_JUSTIFY_LEFT == TRUE;\n",
+ " SET_PREF_PP_SEQUENCES == TRUE;\n",
+ " PDA_STATES == (STATES-{symbol});\n",
+ "\n",
+ " SYMS(s) == IF (s=lambda) THEN [] ELSE [SYM(s)] END;\n",
+ " SYM(s) == (symbol,s,symbol);\n",
+ " TERMINALS == {x|∃t.(t∈Σ ∧ x=SYM(t))}\n",
+ "CONSTANTS delta, Productions\n",
+ "PROPERTIES\n",
+ " /* A PDA accepting {a^mb^m| m≥1} ; Beispiel von Info 4 (Folie 95ff) */\n",
+ " delta = { (z0,a,BOT) ↦ (z0,[A,BOT]),\n",
+ " (z0,a,A) ↦ (z0,[A,A]),\n",
+ " (z0,b,A) ↦ (z1,[]),\n",
+ " (z1,lambda,BOT) ↦ (z1,[]),\n",
+ " (z1,b,A) ↦ (z1,[]) } ∧\n",
+ "\n",
+ "\n",
+ " Productions = /* Punkt 1 Folie 109 */\n",
+ " { lhs,rhs | ∃z.(z∈PDA_STATES ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])}\n",
+ " ∪\n",
+ " /* Punkt 2 Folie 109 */\n",
+ " { lhs,rhs | ∃(z,a,A,z2).((z,a,A)↦(z2,[])∈delta ∧\n",
+ " lhs=(z,A,z2) ∧ rhs = SYMS(a)) }\n",
+ " ∪\n",
+ " /* Punkt 3 Folie 110 */\n",
+ " { lhs,rhs | ∃(z,a,A,B,z1,z2).((z,a,A)↦(z1,[B])∈delta ∧ z2∈PDA_STATES ∧\n",
+ " lhs=(z,A,z2) ∧ rhs = SYMS(a)^[(z1,B,z2)]) }\n",
+ " ∪\n",
+ " /* Punkt 4 Folie 110 */\n",
+ " { lhs,rhs | ∃(z,a,A,B,C,z1,z2,z3).((z,a,A)↦(z1,[B,C])∈delta ∧ \n",
+ " z2∈PDA_STATES ∧ z3∈PDA_STATES ∧\n",
+ " lhs=(z,A,z3) ∧ rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) }\n",
+ "VARIABLES cur\n",
+ "INVARIANT\n",
+ " cur ∈ seq(CFG_Alphabet)\n",
+ "INITIALISATION cur:=SYMS(S)\n",
+ "OPERATIONS\n",
+ " ApplyRule(LHS,RHS,pre,post) = PRE LHS↦RHS ∈ Productions ∧\n",
+ " cur = pre^[LHS]^post ∧\n",
+ " ran(pre) ⊆ TERMINALS /* Links Ableitung */\n",
+ " THEN\n",
+ " cur := pre^RHS^post\n",
+ " END\n",
+ "END\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">symbol</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">S</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">symbol</td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine: PDA_to_CFG\n",
+ "Sets: STATES, SYMBOLS\n",
+ "Constants: delta, Productions\n",
+ "Variables: cur\n",
+ "Operations: \n",
+ "ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[])\n",
+ "ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[])"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":browse"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[])"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec ApplyRule"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}