From 413c189a67370ef17f7fb8ade301f0b723ded5d6 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 5 Apr 2023 14:40:22 +0200
Subject: [PATCH] Extract relevant parts of chapter 0 notebooks into syntax
overview
---
...tax-\303\234bersicht ProB-Notebooks.ipynb" | 1157 +++++++++++++++++
info4/kapitel-1/img/prob_logo.png | Bin 0 -> 10416 bytes
2 files changed, 1157 insertions(+)
create mode 100644 "info4/kapitel-1/Syntax-\303\234bersicht ProB-Notebooks.ipynb"
create mode 100644 info4/kapitel-1/img/prob_logo.png
diff --git "a/info4/kapitel-1/Syntax-\303\234bersicht ProB-Notebooks.ipynb" "b/info4/kapitel-1/Syntax-\303\234bersicht ProB-Notebooks.ipynb"
new file mode 100644
index 0000000..acddcee
--- /dev/null
+++ "b/info4/kapitel-1/Syntax-\303\234bersicht ProB-Notebooks.ipynb"
@@ -0,0 +1,1157 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "c8417dbc",
+ "metadata": {},
+ "source": [
+ "# Jupyter-Notebooks mit ProB\n",
+ "\n",
+ "Einige Begleitmaterialien zur Vorlesung werden hier als [Jupyter](https://jupyter.org/)-Notebooks mit interaktiv ausführbaren Code-Abschnitten bereitgestellt.\n",
+ "Jupyter ist Ihnen evtl. bereits aus anderen Veranstaltungen bekannt oder wird Ihnen dort noch begegnen.\n",
+ "\n",
+ "Üblicherweise werden Jupyter-Notebooks mit Python programmiert.\n",
+ "Die Notebooks zu dieser Vorlesung verwenden stattdessen das Werkzeug [ProB](https://prob.hhu.de/w/),\n",
+ "welches mit der Sprache B arbeitet.\n",
+ "\n",
+ "[](https://prob.hhu.de/w/)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "4f3ac800",
+ "metadata": {},
+ "source": [
+ "## Verwendung\n",
+ "\n",
+ "Sie können die Notebooks in Ihrem Browser mit Binder betrachten und ausführen (der erste Start dauert evtl. etwas länger):\n",
+ "\n",
+ "[](https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob-teaching-notebooks.git/HEAD?urlpath=%2Ftree%2Finfo4%2F)\n",
+ "\n",
+ "Sofern Sie Jupyter auf Ihrem System installiert haben,\n",
+ "können Sie auch den [Jupyter-Kernel für ProB](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel#downloads) lokal installieren und mit [dem Notebook-Repository](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) verwenden:\n",
+ "\n",
+ "```sh\n",
+ "$ java -jar prob2-jupyter-kernel-1.3.0-all.jar install --user\n",
+ "$ git clone https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks.git\n",
+ "$ cd prob-teaching-notebooks\n",
+ "$ cd info4\n",
+ "$ jupyter notebook\n",
+ "```"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "b190c072",
+ "metadata": {},
+ "source": [
+ "## Syntax"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "2f86ef55",
+ "metadata": {},
+ "source": [
+ "Die B-Sprache,\n",
+ "die in diesen Notebooks verwendet wird,\n",
+ "unterstützt mathematische Syntax und basiert auf Prädikatenlogik und Mengenlehre.\n",
+ "In den meisten Fällen ist die Syntax identisch zu den Schreibweisen aus der Vorlesung und dem Skript,\n",
+ "aber in manchen Aspekten unterscheidet sich die B-Syntax.\n",
+ "Diese Unterschiede werden hier kurz zusammengefasst."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "752872b2",
+ "metadata": {},
+ "source": [
+ "Eingaben werden standardmäßig als mathematischer Ausdruck oder als Prädikat ausgewertet:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "8444c3f8",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$7$"
+ ],
+ "text/plain": [
+ "7"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1 + 2*3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "8c3d850e",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2*3 < 4"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "c40a8fbb",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{2*3, 5} ⊆ 3..6"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "9272586e",
+ "metadata": {},
+ "source": [
+ "An manchen Stellen verwenden die Notebooks spezielle Kommandos für ProB,\n",
+ "die mit `:` anfangen,\n",
+ "z. B. `:pref`.\n",
+ "Diese Zeilen können Sie ignorieren."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "234c4b5b",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: OPTIMIZE_AST = FALSE\n"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref OPTIMIZE_AST=FALSE"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "624691a7",
+ "metadata": {},
+ "source": [
+ "### Variablen"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "7ec9cf6c",
+ "metadata": {},
+ "source": [
+ "Wenn ProB ein Prädikat auswertet,\n",
+ "wird automatisch nach einer Lösung für alle offenen Variablen gesucht,\n",
+ "sodass das Prädikat wahr ist.\n",
+ "Z. B. wird $x<5$ interpretiert als $\\exists x . x<5$:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "a824b43d",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = 0$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 0"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x<5"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "26577070",
+ "metadata": {},
+ "source": [
+ "Die gefundenen Lösungswerte werden nicht über Eingaben hinweg gespeichert,\n",
+ "sondern jedes Mal neu belegt:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "e010e8ea",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = 1$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 1"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x=1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "2787f25a",
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":eval: Computation not completed: Unknown identifier \"x\"",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"x\"\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ "x"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "4357082f",
+ "metadata": {},
+ "source": [
+ "Mit dem Befehl `:let` können Variablenwerte dauerhaft zugewiesen werden:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "4b978071",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1$"
+ ],
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":let x 1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "id": "20d3e677",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x = 1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "80cd003c",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x = 2"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "0eb8b0df",
+ "metadata": {},
+ "source": [
+ "`:unlet` entfernt eine gespeicherte Variable wieder:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "id": "5b52c450",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ ":unlet x"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "68631aff",
+ "metadata": {},
+ "source": [
+ "### Prädikate"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "9461e3b3",
+ "metadata": {},
+ "source": [
+ "Das Argument vom Negationsoperator $\\lnot$ muss immer explizit geklammert werden:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "ce29cca1",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "¬(1<2)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ec281282",
+ "metadata": {},
+ "source": [
+ "ProB unterstützt keine aussagenlogischen Variablen -\n",
+ "der Wahrheitswert eines Prädikats kann also nicht direkt einer Variable zugewiesen werden:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "id": "847538f9",
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "EvaluationException",
+ "evalue": "expecting: 'symbolic', ')', ',', ';', double vertical bar",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31mde.prob.animator.domainobjects.EvaluationException: expecting: 'symbolic', ')', ',', ';', double vertical bar\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ "a=(1<2) ∧ a"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "8514048e",
+ "metadata": {},
+ "source": [
+ "Wenn ein Wahrheitswert als Variable behandelt werden soll,\n",
+ "muss er explizit mit dem Operator `bool` zu einem Boole'schen Datenwert konvertiert werden.\n",
+ "Solche Variablen können wiederum nicht direkt in Prädikaten verwendet werden,\n",
+ "sondern müssen explizit mit `TRUE` verglichen werden:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "id": "d89387e9",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{a} = \\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\ta = TRUE"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "a=bool(1<2) ∧ a=TRUE"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a3a5d616",
+ "metadata": {},
+ "source": [
+ "### Mengen"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "f1096c22",
+ "metadata": {},
+ "source": [
+ "ProB erfordert, dass alle Mengen homogen sind.\n",
+ "Zwei Elemente derselben Menge dürfen keine unterschiedlichen Typen haben:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "id": "b9ddcb78",
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":eval: Computation not completed: Type mismatch: Expected INTEGER, but was POW(INTEGER) in '{1}'",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:eval: Computation not completed: Type mismatch: Expected INTEGER, but was POW(INTEGER) in '{1}'\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ "{1, {1}}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "988f2ef1",
+ "metadata": {},
+ "source": [
+ "Die Kardinalität einer Menge, $|A|$, wird in B als $\\mathrm{card}(A)$ geschrieben:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "id": "db9fc40c",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "card(∅)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "id": "7197e767",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1$"
+ ],
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "card({0})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "id": "24045156",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2$"
+ ],
+ "text/plain": [
+ "2"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "card({3,5})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "d661f927",
+ "metadata": {},
+ "source": [
+ "Die Potenzmenge einer Menge wird $\\mathbb{P}(A)$ geschrieben:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "id": "d7c9f328",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\{\\emptyset,\\{1\\},\\{1,2\\},\\{2\\}\\}$"
+ ],
+ "text/plain": [
+ "{∅,{1},{1,2},{2}}"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "ℙ({1,2})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "66b4d0d2",
+ "metadata": {},
+ "source": [
+ "### Paare und Abbildungen"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "c9220354",
+ "metadata": {},
+ "source": [
+ "Paare werden in B oft als $x \\mapsto y$ anstatt $(x, y)$ dargestellt.\n",
+ "Beide Schreibweisen haben die gleiche Bedeutung."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "id": "f16024de",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$(1\\mapsto 2)$"
+ ],
+ "text/plain": [
+ "(1↦2)"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(1, 2)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "567f0f79",
+ "metadata": {},
+ "source": [
+ "Funktionen werden in B als Relationen, bzw. Mengen von Paaren, dargestellt:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "id": "8890cb60",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(2\\mapsto 1),(4\\mapsto 2),(6\\mapsto 3),(8\\mapsto 4),(10\\mapsto 5)\\}$"
+ ],
+ "text/plain": [
+ "{(2↦1),(4↦2),(6↦3),(8↦4),(10↦5)}"
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":let halb {a,b | a∈1..10 ∧ b∈1..10 & b*2=a}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "id": "3ae95bab",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2$"
+ ],
+ "text/plain": [
+ "2"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "halb(4)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "cb5d4125",
+ "metadata": {},
+ "source": [
+ "Der Definitionsbereich (englisch \"domain\") wird geschrieben als $\\mathrm{dom}(f)$,\n",
+ "der Wertebereich (Bildmenge, englisch \"range\") als $\\mathrm{ran}(f)$:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "id": "0e09a84a",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{2,4,6,8,10\\}$"
+ ],
+ "text/plain": [
+ "{2,4,6,8,10}"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "dom(halb)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "id": "0af4cfe7",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,2,3,4,5\\}$"
+ ],
+ "text/plain": [
+ "{1,2,3,4,5}"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "ran(halb)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "77ad83ef",
+ "metadata": {},
+ "source": [
+ "Die Verkettung/Komposition von Funktionen wird $f ; g$ geschrieben anstatt $g \\circ f$.\n",
+ "Achtung: Die Reihenfolge der beiden Funktionen ist hier umgekehrt!"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "id": "5a54d02e",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto 2),(2\\mapsto 3),(3\\mapsto 4),(4\\mapsto 5),(5\\mapsto 6),(6\\mapsto 7),(7\\mapsto 8),(8\\mapsto 9),(9\\mapsto 10)\\}$"
+ ],
+ "text/plain": [
+ "{(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦10)}"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":let inc {x,y | x∈1..10 ∧ y∈1..10 ∧ y=x+1}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "id": "1241d6d8",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(halb ; inc)(4) = inc(halb(4))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "id": "a99755aa",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(inc ; halb)(1) = halb(inc(1))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "f21c0259",
+ "metadata": {},
+ "source": [
+ "$f^n$ wird $\\mathrm{iterate}(f, n)$ geschrieben:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "id": "db7ef9ce",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "iterate(halb, 2)(8) = halb(halb(8))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "fcc7511f",
+ "metadata": {},
+ "source": [
+ "### Alphabete, Wörter, Sprachen"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a4b9c92e",
+ "metadata": {},
+ "source": [
+ "Manche Definitionen geben wir in einem `MACHINE`-Block vor,\n",
+ "z. B. die Symbole eines Alphabets.\n",
+ "Sie müssen diese Syntax nicht näher verstehen."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "id": "e647c198",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Alphabet"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE Alphabet\n",
+ "SETS Σ = {a,b,c}\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "id": "cdbc267f",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: PP_SEQUENCES = TRUE\n"
+ ]
+ },
+ "execution_count": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref PP_SEQUENCES=TRUE"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "56267c5e",
+ "metadata": {},
+ "source": [
+ "Wörter werden hier explizit als Sequenz von Symbolen geschrieben,\n",
+ "z. B. $[c,b,a]$ anstatt $cba$.\n",
+ "Die Menge aller Wörter über ein Alphabet wird $\\mathrm{seq}(\\Sigma)$ anstatt $\\Sigma^*$ geschrieben:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "id": "f54776db",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "[a,a] ∈ seq(Σ)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "d21cc56b",
+ "metadata": {},
+ "source": [
+ "Das leere Wort wird als $[]$ dargestellt (da $\\lambda$ in B bereits eine andere Bedeutung hat):"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "id": "4590adc6",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "[] ∈ seq(Σ)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "cefb7b6c",
+ "metadata": {},
+ "source": [
+ "B behandelt Sequenzen intern als Mengen von Paaren $\\mathit{index} \\mapsto \\mathit{value}$,\n",
+ "wie in Kapitel 1 der Vorlesung vorgestellt.\n",
+ "Diese Darstellung ist in den Notebooks allerdings normalerweise nicht sichtbar."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "id": "2252b6db",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$[\\mathit{a},\\mathit{b}]$"
+ ],
+ "text/plain": [
+ "[a,b]"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{1↦a, 2↦b}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "47111cf0",
+ "metadata": {},
+ "source": [
+ "Konkatenation erfolgt explizit mit dem Operator `^`:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "id": "d96e0212",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{w} = [\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c}]$\n",
+ "* $\\mathit{x} = [\\mathit{a},\\mathit{a}]$\n",
+ "* $\\mathit{y} = [\\mathit{b},\\mathit{c}]$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tw = [a,a,b,c]\n",
+ "\tx = [a,a]\n",
+ "\ty = [b,c]"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x = [a,a] & y = [b,c] & w = x ^ y"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "03143769",
+ "metadata": {},
+ "source": [
+ "Die Spiegelbildoperation wird $\\mathrm{rev}(u)$ anstatt $\\mathrm{sp}(u)$ geschrieben:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "id": "21e51f7f",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$[\\mathit{c},\\mathit{b},\\mathit{a}]$"
+ ],
+ "text/plain": [
+ "[c,b,a]"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "rev([a,b,c])"
+ ]
+ }
+ ],
+ "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": 5
+}
diff --git a/info4/kapitel-1/img/prob_logo.png b/info4/kapitel-1/img/prob_logo.png
new file mode 100644
index 0000000000000000000000000000000000000000..bf684448b3fbeb72ecd3ad43d8f6f2fd67eed9f8
GIT binary patch
literal 10416
zcmeAS@N?(olHy`uVBq!ia0y~yU}RumU<lw~V_;zT*1cMlfq{W7$=lt9;Xep2*t>i(
z0|NtRfk$L91B0Fd2s2)lk&|X%U|=ut^mS#w&&<xuVVe1Tn<E2*0)wZEV@SoVw{y!&
zWUg1fsQ-R0$5Ee!LrB4+X>Y?`@3hGtnjs5UrJkOabGj@^UUl1Knde8(d%m&g{QRi+
zPm=xq8--tTBD-=+PYS69wuYK$ep72=)nV`uStPJGclOTr{gFD1IR}~Uv@&Gb%gA`m
zxI1&_{l8VanHE%h-OHr-jQKv}JC;oz4)q2N+y~A#rh9+O$@Gu=6S=EzufR8M+w0xe
zbEX~8c~E^omh(^B(R|GhA|GZ?vW>nqN!;G+`o`zVkHlXb+{inF;|{+M(-V)FCF?u`
z5-zg_vFu;8^1#!ti$c!GuWhh;;JaW;%6YNyPmhiZ9L;_w?ldDlv@4#Ws)=uL)8hln
zy}#w`G!dA{B(nbIpC$1HDhgIN)LHuH{YvmoRr&KRMmuh^rSuQ?2hz&5iJoTCK?fFD
z25ah^aMm;~@b&6F^(yL{oPB%O`|LexEcflc9-LMb%Ta9ifm>1Nj6FvL%b#5pXaCOj
z`et)qc9O+(8?WmZpU>Q0_BriAI_DH#t~}N{&O5z4>rd?Nvpv6O>+H!5^{o5Mq{Obh
z{hD-HW%F|JjdgFmrWi3@Z@F+|Teke}{yDCfS)7i%HI-vAdbalNAIq2KzlG1(S43#F
zRBk`|W<Iytxy6iYzv?=8FIat?Z|cQ=_d@r4`zIRfUMGK#HR4NTL*?SupSo)7jR(@D
zW-MzoI{SM6sRM7nDM-xt$=-OpVE=aQCu*^Z?|mjbouI%vgMZJZ(l0wNEc<`!cejX$
zN`Ps~4Hg-m@<Oj&-aT%=LIro+UY4z(%O=mZ!&hB!!Y)CNzDK)k8<!~_o}po9Tp41p
zcjbncliplWnNucx(vSVGZ0%A7Q&U!-HtiP6Q1yEc+x&MNoZYbFad_Vg^N@t=CSvF3
zp1CtKSVLmId(fojIcs=y{NC@LQ<!}Gi_+{Jm-}@e{#I9D{P^)(px4CNv(7B$&q+Ah
zbn^xCrrDl}b#i90kC<Kl#0ROeI4}tbus^%rkb3m;k6+W}oVMR=-dZbhp`^Fz4v*HW
z*@8y@lpNH|v>7=&_9j2tl3DX|^Y<TH_et)3A<(p_^Kszeh5uU}`qMWVF60o}@mJ+h
zxJJh7Z-If8Q-6L=i$1nD)4~5@{{)W2qwE0(4=t?tW>O|^mu<;d7?*U2)x&`)={@6u
z+bsL*617>a?NYKXvOGIG@7R`=!XGPZO}1_+eDJ~Z+1a^{7neNH`M8AhvE=;8Zn?$o
zcj8SI8H6S@SnOoveJg9SrSwB!q-b=RoYSwXJDKj-HP71Rw(sAO!;bf5XHP!*#q;MC
zv$_5ISrvrRUR^McJZgV-`i=P$U)8$o)IXF|k#8Ry?_p85Os4;I>)n@cPERSb=6-hW
z$&sC0RyOx`tWy?b=}{KsP|W*b&iL`@`+~RL7i^a-IQ%s6`n|;+|NiowO8NO{r;pTh
z;c^)-$4AfI>hkWy`usT}ynkcy>&F|+G;eJDuHnS8y~`u^`99z5jXz6E_I#MVfx#|q
zk>`OI0`m;7@9{ERU7$0+`h%agv%r)1S!d=NH(%{eU)b|w=d4bJ1STPaGZUU|*_e1$
zN$$oT#RG2^9x&Ns^YKP)%(``toz9w?=zjZUmB^@~z<8L2t5uKX`~8oaa(nWdkN(Jd
zptMlG?pxlm^yNvjw7}tY&}i=U^hcj0n*V*R;N4><eApo0;_>2u8Foi^E!})`N1f=Y
zo_$suGJ+WS?{A&gBf_qAjMs@%T!GQt)FRg`OlRh~BTa?PS~4O|7w%m03ih@>yY_9&
z%G@Q3ZyT2|E@0WL{`6C;ySe+)ufGqk66G$awz2vC%WoG?{Fz5WoQwiaLE_I+H&(r@
znRaHrYnq$X+T6J^)}?)W+wC8D<pwW0Sw7{>;>&4|>;K$TJ~PK~>-iUJUr1cD-@81#
zW#6V%ZT#QlpFY`HBsI(WgM?d%+7_qAg*);u?@C~fX*mCQ;g=*<{XP5Uw!e!ze~5K+
zb4!bn@3r-jotG1zx9VDFX1rGu+v~*1c!8VeaLTVE8*9Ex#~+zFMP|kQb7xPcU2eO&
zCeCht{okMOcLd#@;&6?Feg49TjU`sb={`qI+QNJmi>!$2wPF2PY4h!6b>)iHlVz*<
zH-G=2sTXSgaD%HDGgITF57&Ozr`(&9SyEbd`O-DV=xX+_*JoJ<N4cFm>J?=bYxDO}
z*uK2WGp)<3Cd^KdiVM?=cknAy)6c(o@MhO)38P;j^Bh=q3REeHUgbW>#dW;@=);mP
z%2L9Y4Lp6%t0|jGIu>8y@IUauiT|9hFxRId=jAu5GVdE`&7L4zb7~QD`{8r3(qWrx
z5)Iey-#+{M_vsT%9M<oj&~!<g_s`}2`rhjw9({~5Y}4D`?l)arlXcdVEhW1v-+j%k
z(ba7|bm-57X$P)ow*EOf-|o=1x$G6`=LN0ysu_7XUYM_Dzfr8=)9JFC+=gbco1VXj
zoTfMD@S#VNwW=E?ys@sBvFTMC%k*A@G=BDzC;KMUzkl^=*}EuXEuWBBkApMT@Laka
zq$DuG^V|%cc|XqBE?K^0L+bZL6Tx|`OXok+yBfp2YuVRTEFv81OtyUZb?t7=(~ZA9
z{QS5o_g|TkBDdqa*|mGSTJG=NGFABb`UD=v_W2r&2@5<5Z%Iy`cjijx&nGGA3A4I(
zW&2JEy;`_-sqp;s59<GZQhnxoHvQU_&Lzv2UbuGeWa}p{uTxn9PHI8wi&;!owx=AO
zoUZrjO85IqPd~L8{?$D=Vcw&JvOvb|I@)Om*Q``o&eGp-#iZB$-ED{BY-#y<I|L?w
zmzzB8%&OGSo_>Cb3nH0r-ju9)ee!(q$49C6Zf>03HOuYR?${kRY+Rx<v=v@te^}AL
zutRc9h^Xx6=c!9KRvuovW_PKfQ%2)~2?A1f{j<%t{hhdWH@|X&ajI!e$;M~9mP}cY
zy*Oi6`Jvw(3KAxB%49DaC_g&?*3_bETT^oS>6zBL^LOX}7wLX>_SlEYUtgI$<mxMg
zr)R%fxh8+FBI`oVgU#i4PJLR+y{Io%<8sQYE1osQzeKXuUkfUFr!+NmtBJ|h%U7;B
zwx4z_-_GBEzCB1`>5<Io95V`vBNze&b}wUj9j=$~R=0bt<eR-Js}H$kO=5o^b^ht9
zsJ{6t9j<ScHt!em`C<5OH;27}OM?UN4*Q^nE4pQNwJWF1`nA1c!OGU&>~Pkj9YI0C
z6;JNn{&_KYeZuv2H71_mjWy>|uC0j^Yx=3`B($&Yfc$(3>oT70PoFj!y?pUv$=bc#
z(@*!_etb0jhk<YFGS8q%lPmtdjb)uLA%1`*XP2BIyLL;OE0ds#+OK;&(-v|$b2d*u
zw@WSKebMJn*X)hTeAGTaJM+TX`;<wfNxs@<wf@J4rrxrvtG#mROnSldU!jWeyI1XM
zOIAN$cz$m71m>wMzwc|CnjV!hmh;+?X*P$?+Uk+o_l&Dwd+%@it|6@6vv`Gp{PN3w
z3PNjqV)Xds<t$Il{It66tRVMS+cP_SBV_)nR-MVe`S#PNXWwei%(3F!eOF8+|JvFa
z=Vxw;GWq@B+r5ykJ8MLi`OcPEvZN+X{{3641M3byzwz}U=ezq`W<BkGK55F6JrBR$
zsS#@k`r*@>s8!;-AX_SKJ-@T#*R6bYe^!S_niLBOb01?<TC;ZT+bN;figvAGyKK<(
zd$TZ)rIV!1Av@0Egg^YAKQ*<oXIm8So6~yKxXI-Gp+_@c+%oh2%;UtMc{t(Wntf;V
zm$=MSTfcAXTxNCsMK331$I8vCOO^i3KmXB2|NorAT*p*d4wTBDa=N!^=j55jxkfi5
zB{PB^eEhXy->n0ko5goV+&s`Y$y>&vlymmF$jebRY)%me7tS!OXR>?t!C}sl^#WT;
zcdcBPoswAiA+`OkUtXF~Z|=H-p|3PG<`~>N|3$&H_p!RyjgQ9<Pni;X^uu&DFGjD-
zD<<16-F?fae`Ar3`Myk+hD@zvY0EzK>f0VT(qyw_O0Ck?Wr?32+<je9{kv}7{ax(7
zlV{YWd-MMY;oM)pWX7$H47z=45#HY1ZHWuMp62oN37R~4$F*y=8o~jWOXI4t`Tg4G
zX1cci`Q9D9Ga|PC^oQ&3z8=~b&=ooPvooJaZdTUPg)3*yysQ>|Naf6v#MjfzFGdtB
zkA436d;Wrqq`Dak+K)c@es5>nvuk1Z?iDlbj{WaqbWHsSOUH?Nr;dg1`vn-YjXfrE
zcfJwiYJO$clqWo|>Y;6k?<2#tO)A;4weJ^aHWems-e~!zb`w+3=8yN*)$ZB)n#HgE
z+z!K+J||A6J^T}SXH!z*{PR+F{CV52mlxmI&1DoM`y^$ld!nX<$oV-<UK+n=AO6Jg
zUHZ5}Po~zSxt=Ek-Yp7Z>H8tqbs=b0n|R}eL-RQwY{=|6dy;EW;!++j{jf!rIX_yS
zeA*iJZJyTSoXp4zHw?Gm?!NM5>1<~Pj*OhQkB-djo>*J)zmX@pT-N2f@V<X%^O=sg
zpSu0lYUj?IiS5m1+e%wS_%?2csgk++@33RblsC8QdtPO~WjyV8*`&l*S=q&N^X1Ir
z%d*eS*wpybFmF5Oo_&86dVO_k9zOJ)R=MPtR`==ftRH7jzYhqzEHV9~mpSvDkO<Dh
z3#R?FKQdKIV)ooqOPcmfn7;m6?Bd0zn-2@xf4^iPn&*H2Cd*sh+&4F>MdCSROtx=h
zzq@$#X72UZGp^*DJ-S)>LuPm16r=1Qy-LeS3mG#j>)4PhF^f0t<BZMnn3%B4zfV-)
z@n1oM<VO`<YN9NmPdPPjRzFd3I#zyb-AWO?>FNc0BHYu(&+pkXmHVo1M%4ZE*-io1
z1@7#<b>)&<cKG)4kTgc0HTP-{hukRToqfNru(D>xsarQTi<ZvOTkovdDiF4MX|2iC
zPwEPJOl2z`@7>epdGSY%+|8Qm6O&>NzkYo9vG|79AD0?m4hgw_Ex2%Jmtmx&&Hr1w
z-~3;}GyAaElW!g(TXkjUSXR%AG+xeT#57%N)y|m9E$iGOw|1=*S(a&(AH`^_=C7cx
z&fV_I&U#mlKRjF7B0SFb<x{ISX0|EpR|*_e?r@2uUD*-dd6UWc6NAf<{rqj;V&&v7
za~J>kl|1|82@ig+wVr2>6|djxT0LDlc5>nJt<LFs!EtvT+_H?8PUXEJYo&E&mQ}1B
zpWM$ALJSSZA3v-(S-Fe%{)<)220pHNX-58b`(_^cn7r|JuH)<+DK)+6-G`T-`+Vt|
zZAodhM5mMAb<;^QW^7*W8cPd)^H}ZLd#%%`!B==ii^C2>8JF5k(+?$Ugq@pxNVq>o
zN!ixaV!fV9`uX@rhlQV4U!8K~Hka6yt!2U2Z{<Gyt^CNdaN(-HwqMy#dQUIjxU#YT
zT=>H5Zx@vrL?+Chd4_-g-=`g>7lJ0MELYk5ZrafsrE}B&ZD8Jh-2Bls<N8}H`@W|4
zFTQf1S*`Vgfp2q{_Ej1C(s|0N;u#rl4?H&XIB-FS+4oe#Yl%<BK?;H?=}R_c-Zcta
zA0e@A!Lqe$=Z0^qD{yvpeyppp{@V7>o8$MoOuFnB?QXtoN`qw;OT&4C$lWz^e#@12
zxz1MGzAoa(Y-|3Y;<dRRlOrByoz-AaUiI;U?b_3m)x`o#RyMT1yL;f_W7R#s4=U<~
znMKU{@Hpl^N3I5Uc)M}sp^A5Vb5+{}qZ+b;Cd`_1<jA2y5wRzWLw?j|<z+tpzJBld
zo1d&oa-T${woQr2d*!s!ZwbRgeQ`P0yA5IcKR@743z3(f*jAk;kv4UfZj*L`VB+}&
zr&PJqjMIOq%&UDW%QsKUz0*J8oZ_Kb$`?V+DYJF4avKBAYb{j$6u_rgS^r(}o811E
z!<q6Q&&F@6|GId>;^RygOy|b7d+qoe?Cp8pLptCwr{>Ll&l!5x&Rv{T`&Ksg&!g@6
zEMF&P&r-SiG9fFF@pYKqMz)Y2{!=`?iavckF2CU4^7BDqlV^m;bg?PT=rE7tUFGxc
zRsr|TWTVR3+jUmEY^SBkx*BA$GzeU{_41*${XgFL$_i!f=YF4!J?>BGPL$YjSFWtK
zqDj}9|KYb;%Kk>&k|I~XSL~UyE1-8-X07SuO*u1c)%8BKfB*jZ=kL7aql<1{H=Q$~
z=I2D;KX?7>=4aSS@Vs|B`1fMO?97!Xb7D5nX)Rv%dGq}}Ua7UOUkEWU&vdjqtZ*_>
z`Q}39rJ_BrihjTNCh;QZ$lMpd!atYp-1FzRarBI+35VA#V&eLA{Lz-%fezK_;#aSh
z&e2=FXw^Q^_Pb_PRi9c#E4U6V->(uQJn5PqzyIDJdVITkU5{R7j><?%WGwDF78E2_
zCv;Xl(4yt?(NbPt8OzYF^Vu#1(yTWlU*0I0J4J>4=FFEp^44sUS*xZPojiN;(fs{?
zQ~$lcyuRQ|%+nX!8Scb2AKECXGskr1p{Bx=C2GmrZ-1z$*|MdyVCk-D%F9n@WW4N=
z@a=V1IG%TTXUy$GOJBM9h|IdOW@g4eB?aHh1y(uAW*nvyK5>4x_2t;pcCt9SY*WU)
zGYpEemK~h*bF)R^!e#zaUYfs3)_N+w)Rp%U-qU7(KvgBEA#>J^Tr;J}^UFLF_RSGB
znH&}nJX3*n*ObGP__{T&wD8PU(^<df>DRaIFG?!c-fVbyZRMJ<k0R~8XTGEyd!Axc
z|IOsu{Y@4Io~!C(o}b_ULjhE#^7q9inDk7$a5(qFtk%nwKi-w5q%Tu6o%?U<zh!}E
z_Db)re73aQqF@(OyRO|;|F)F|zO6xN^97FwUEc6=@7bq;Ay1dLd0dHLi7Z|_xBF@M
zj4%^J0sa}*wM7$BPWo&$wo{kB>_4Y>?cA8`mo6M1DtJE?8%LOxYZ)*1O?fjzXFqr9
zrz@ZH10(MX1r=1*u>G`LsWZcJ=1W)Mljlz#TX#Fap*Wj;x?XtUs~F34tydS8{E3*U
z5OZ?-I!_rh+4+L8&yGAbU6Gsf{MFX7b5lY$|Igs8|MkN5$+HwT`{2nn-}c?k%*lOT
z68W}c`yMB*hD_mOA6nbrzbMsclq_2KGE=kWvo`<bUz_h2E!@PY+vfT$sNry4^0g<0
zKJ#YyJKmEBnmqYMS#?HE-qJT-ywCMQFJF6kD7|mfy*R<RY}e&KSyHEG&#+5PYIwfc
z=u(qL-K`}x`+h!kXIlPv&!=a6ad#_Q-fT&kSMecuP3%?;jlHU-(wd2{bS?$Ywb@Z9
z`Z`Sai}a1!{nmE*JjH1~NuTGgUb#O1(aY)gpXU6$+TY8W<SN=&(9O_)ev99apFiLK
ze64Tq5%}=Og7fOjmwY&J_w~>F{`=jkr&pJ7GH9{{a~+>JYnt5En4+a3+T!OP<+#pG
z?P@nHUaZP=x#iFvo-o}xXYWdfDVoln%Jf>C`^C$AyOKREvcLNZH*S(!fBsL(k6lg=
zxB~B7k^Vm|bQROHl|k3$9O2wKv*!0|{)y&h>IuL2RTlUNKNIPFd{Y08dsWq{_>7qU
zdHm<9mz~$RtYWS{`Td`t&ny1kwcWG%xkcXk{39oBN{9Ig-LkUz^J2RG=e6qZ(!YH<
z>G;m!;uEK9>ouNzm34RDqP>9K+t)RGyY{QgA*})?Ten2(P2BYCwW3P0(Ik&js|zNH
znQyP@-HBtKy{y%><97Cjns+I3^##g1EiGrXnJ*D|Rh#kn66@wjt9mv4yqhQcnpLlT
zc4y|l&k(4=8u@Z%ZOfv}9|k<a(JgJu-<&bAtG{3M>DV)c7E_T&Pi`8mGu`^Y*ymEv
z<cJ`f#ph2~)^v#$tAF}>{N3TaauyvnMOAnId5hO9n&lU6zH8ZJ^D>^(;%AhUmCvq<
zH1K`5yO`H3_W9KB-<gw6^jb8#e_$y7pC1tHk-3v?e^sIO{eQ2POWNyg?-wxO)#uNN
zI^HP!d}Vf){KhWN>3_GdoqAFd$-CV9^i1Q$8lPlpHCOJ4IlRt!`NUbJw@%I7ekS?m
zp_?g7mM!?%+`MdI!A{#bTDr;48~a!6yw<n*e&?#TrayB`_I;YU+r!(p@1INf|KGL0
z-j#-2H7)uT^tFTYPrJWzYZ}wb|K}RsujkR`zL1^2>XnqE#_Ai&M?SX-+}X87V)^05
zDN_0SwztQ!+aG#r`r+5s%~wqB-Kw0BH=SRTWm%9&@A)T}%h!MJKd@~}U3Rwg|DU^c
zLrk|kDEs|Ek}ZfM$84^w{JaMTt?iF)Vl`&|U3~rR_JXCm<}s_LI)<G(u9(_>%lSgR
zeQU$AZFzBZ)#msAd~#OY|5-hI`ll<WZ+mPyZl<A|q|VTEa>L%!hxO-G&t^BjcW9UB
z=f68d9G5-)y_^5zt8L6P)I|KxK0kT<ovN;><(tE5Po8gjxh-_hk7H%`{(o3(*D7@?
z-C%i!Q^fybg$p@Wm(`yZ|0{~UQJH&KpCQGgH97NQ-I10r%NbK$avvJ|gq@q6B>Urn
zGDFLg#ha&Z$gW~ouIP4h;+#1x6DGy~{a5;J?hb(vjpQFZQP#Z<J?`R@Qa`7CxtOP`
zyY|l)^YwwD_oXcC9KUbhFSX3m*;{>o%|qLuNpsK4w9`~z+4t?n-kL9e;~#wVPw4ZV
zqw%L#g-P((t$=^QjZYS&eQWh!KP}WeplIEkN0F|Mr(RAwT3k{1I?g68-lwZ2DcAFb
z(GhP?-aB&g=l>*%=fAf*($o1^V)ks;Nq0TBA9szdHGaN6X6eec((QUP4fJN)*Vh=Y
z)btF@d~-f$AMgD0$LB46&eUP5x?}G>yQZ`a35t;hL0+2<r@H(4wr$~CqOhj=iu38o
zpNuO1EVORY*}Qo9=?yox*k$v7WGSn!=vkbuzxXxt^@h}?){&cw93MosC2mN)ZKw4*
z>hSWPEvg*<UjHorv3>u~paq5A9=*KU-8VlSEL>e%9UvAgq1HbkOJtVVK3R!Ik)#L0
zWs6#-m5GaMt(sw7Ty(*B>6ICln*IHHA%bTux*qb0zj!F&=d5h$xp?pC(+iD7H8vlr
zzqZ1`D?8DzowqUJ-4>@ymoG0izulU0anDQ{{k=}@_1ku?%bugT|J2h}R$XdO-LI-#
zmcDh{T2psDU(P=d4()D(XX{LQCoH-Xpmd^Clxa?xwB^i9AAOnQ$4tFX`uM*+%3`+d
zt)+vrx4VOI{QtcB|KGoO^CaS=>mEDhuE$FkDCkc&ym_;+Ha8>Z>5Bh%j(D8OnmoyG
zdi(Ty{~FZoiu=FTrfy0*>U8gZJd@LrzjstUmsB!L`!?NB>-JTX6?<+qoPNspD&*>t
zgg-Y7=j^H|t++d1<1c$Gck_~Y44c$`%Wb~1zrcy(LW%CH1&RHl3M~$om&8j&dwh}V
z`d?M2-G9Gc`sn86?&<+8N8T2F{NnvSAoPCI2l;sd{1R)D1*dtM*mhJHUz+^$`2Gr&
z8|Op*-DLFSGrAn~+i2Z{m{mIteXCX9__FH4uHTo-lY_OVemxtu^CQD0A5O=QJtu3w
zeLeEhyJVNmjofXFXG7Y3pXWrH#`S9lteZRO&4Pj)v8lXgo#kgqwl=s%gyk%`F?GtJ
zqMdmGBAOynQod{FD!%4w5qXl5{^PustmLxHe5;FxO?@&Fl`kA@DPFfnYWr!~lCUTh
zi`sp2zWJGNx_&!@>DI10f1ZDSzbWHcrrfS<TgjIv74JK8G@gH*{QKVHoZIzHdE3{Y
z-}|U{#|x#SN^30jn`YH*nPB<UqhRT(Y3cEI{i3H^KiRxQpjKkX%B^#^_2sR0sbV-J
z&XMM;`DSY7ggNV1I9=cR;)4!L-28(#y{C$tpTl&@<+91Krzt@<F9->zaXfeX`bRp<
zLF07ORTmy3Hz%cl9edf*I97*pI8HJ?`Tkz-frBPR8>9sveKsvU`{&)(w|6!tiY6Bu
zDa-k$NU&LdpPTT0<0XfO6C{~3*Ur_mk>j86M*W+W*Xh*-)wLxhB|*0@I7OB+%gt|G
zc5;K1tLuf5!tdMv?0EHG#(0jI0Q3A`x2|6GEsj=q_tx9+I)PJey=bF3rybww@(Z4t
zN4G9BGl}hf^(4w!^Vsv$?_4HMwZYP}ma#Ua+n#c8*`SpDI$C4i&E&kSl(Z#EEix7i
z;;gZ5v)-(6l{#}%SW#5z$?oqOGa7B|ZoalRk^Hwnu+{0*hrHk|=M5h_9Iwh*GU>sI
zou^}Ra}v`ovUI8SDchUR-f|_Sg=PJ91!Y}UMV7er2c>uSC1|w<U8`7a_)>F;isgpa
zVFfw2o-pObZ*5reB<1y-&*$>us-E}9tjKZT614d3D9rS{VfpWt`1vcHvcE=%inZmQ
zF$@)0TVWH&H&=(Zu6*f-S#0m}_;ugDjmdtwVA;Nz%eLvg`So?BS(J#)mA4-iTuY>4
zoRv(Y<;~YDzMVVudsky&^<V3|wPzkqxsvkVvd6H1Q7J0kNGF|RO{c@dMW38kX83xR
zwZ%*h>Ux(a9@HjS)f{l(V~4_vji0<_%zE3Nl}XJyU-ZUDvMhFUlWSe>rh+iR?{~H_
zEx&xO_Vx6lFK1N6&d)sc<s_?$>dnF%Z!%`7PGnx`vj1CV?)xQ+mI=1|c4zL~sK)mF
zdq(HKU$rhXUYI%_xqkKSv#Yu67oAf$d=4Km;N`h&r4YnCY0(U8`BVF+8d=3(5j%AL
zyHvvU#qs+;l=pw@Suf`FBUw~Qt@Dk?-+xL?=XIB~{*UneV90yowAXPtrQHjCT#K{Y
zU2kvtZ`rh0Y2V?{v-kMb54Jj(f3UONURKE)^EXP@-lAw)=49>}#<fb)*L4yPzd9QD
zyOH&A(U0Hi@(+LN?q0bjKkbTx1-C-a%{#&S1zydXAl00^Yl<U_-d}YE{x#lCk&b0|
zm68lO*sd-W>rmEMYQUSCd04{bh_WX0X@&`koRJ*$0tRlU{Ii-CdHz&PPH0=X<5mJ|
zT(hpep~zmL$q^?T91le7?@yGNv%8@6=4Gz6S=$|z>SOZ6>i;h1|M+NHtc+do!}ZDH
zwaVGbJcnlP^osPkU|+n*Q&RZy4);smE&%~S9D<=NaWm5vbgp0z3J!Yls?4>vWtXq;
zk}s=x1D7qj{dnUhfufAZdwy{r{qX(8#dQz;j!g~ZJk)s4h4Hab@J!pS22V=2A9qfT
zHQrU$oG#j45bnZrrfoy!ff+{ogM8*rI4zq!{mz6dq03IDo2_@>(9Q23d+1v9qP_!3
zuM75VTj{dF{>6D;Zq4LP8<_-;qy%v+5pmi4ylsk!>DEber-~IE|FkJsbNxpF-Lo0H
zdhe|1vAeZl@nUJs)F;&)86TxBIV9c*hUs?86lrZT=heQP68W*@*wd#iGUEHbpOD;R
zmmE-hreZw<1BW4KEr8^vh$9Y*`Wbngvy?oqM_Qyu-T!n|T7XG9T>oKCCGT84|2svi
zH)cd}e$R`Ns8nTQG%I|3E3jjMMYHRVsF17EW;K0!WwmLuF;jI|h{e23ua3QbdW?Bb
zw;HQ)7uPQyz09oK?Mhz^R~+iz!lV6SnQKY&?-%_CH%;EKDm6dWptpCmc<Ykv`PWbH
zd;GlMMsD-&-4b?!3%q^%cmK@Ue)ELvWWmiBubS<43#;Oqn-}lH<@M+}Q;V8|am!Dw
z4U3M<5>@Q!ZF|u#eO9Zk^VI*af_-adE&ZI%aw7TR9L+x;BQigf+?>#DqA4}sIcSq{
zz}1&uC9jxmjZQsb7?HeW?{=ozhmR9xmE9GU>Js|+izhGIvj6OMeg5v>;`i=!9#3am
zs_lMB(|?!9NAvl<!51&S?2C{$u+V0Ri8Ef+wT<!bDvNWM`Il#=N(fDuW%eVk!yua@
zoiQV*dzZq}Rr@6SZ+D-yf1By!CbhZyljhzS>A>GwODD{F^6vJu@0u^|3fIZ>Uq2wX
z_+{Wkugawcfl7;-O?Ege2@1P9f7!%olaB0qS{$*lpe*8-<)@34UhA*0@~)ND>zJnh
z<)McE7fH3HsZ(`k+5SA{Yp-Zo`jE?at?Y|gWslPWWR6>S3+}V<{HD%Rul;_)tILOZ
zzP{MM^-_G9?Av+eyKQ7FODBeU>o}ELy<HP;*uQI8*e$CV#jkBaVQUf(ulo7qS<2VM
z3C!wxQO`|}bv#kx^j17Py+wQJhnZThCMJ~4c8dxUx+!_mN9#oL(WaRxDNEW?|7|)I
zwe7uqYv!yB`P(x-yqK_te>!LFKQCEp{y9mHU%58teR-K1HrFEf;JLrcFXV2UaplkP
z(peEZc)Gc4JCAF{O>7o0Xue&ixW*)IOZB_puF20&%`h)cT5!2I$x(0q%@XbWcUC^B
zvD#*5FD>J0U8!(0Gx_c&%R9TC>?#up`gE=D@Rlv*$4VkHR1#Nu>gMny6dkm9cYgzu
z>4dM#b)NYb-SYJHQZlx+445N!>D8o3+^L~^w*6IjJ9piW9m@^HG=6RPsm%3FPJijY
zC~p4zU8x>{7t8G}jy;^z{i8;0<EgkKn@c0OZ*wnTHGiid7!-9s(D3mDh3D6$EQC@O
z1Xt|4c8uNqT*3ESs*U^owIohY?$2Aa<&oBMZ|#itZw}>co@j5^o_aL+_qJAUPtQzN
zb#MLT%gNO|t}59<Z7a6DY5cN9W!jm!MkW7^d6Mf2HnhxT_jXwM!^gF+dF#4t!@9u9
z7er^+*4x)F?UT3vtJeKYWMjd%luMK5zA)qUjamQ6c<Lboo;`NV{pTONS(?Q+f0sjW
z^zx_Qvll=9GIhhwJmVPU?hdQtb_&G|QT4np`uBZ59=}9A>%hOq;+{no5qne06yy|4
zPrg~ndS+gj#6(BEDdC^*-JATwNAz>r43Bj^Qzm^{Rkh6LRDbrI<F8G3T)TAaTdn$z
z7y6;$%{A8(+v9#OI4$vA<1|NoxJJo;o}Yi!^^0CyQ7tkGI&sQFO;wX~_T9cCT^q_u
zcV}d7KNhijPh8F{vjpi^9?ctC9hmBiJH#Aj++Fr_c1ns5%iaU`^K?z7*vl<=Z8d4%
zQMZc`%$|O|ciYbg-M(<BtM&5Cs2SyVMR+IvX3NORdz_NV>h68&MNxHf_ydvNhNG*Z
zY>JlkL<V!uFt9V<)~T0z>Bb$u&|Kx|>tdE}Su{<rU%c931K+}n**m5L?GL})zPVvp
z`;8Wc_Pb6V-pgk%;|q@v4&i9LoY#NxbNlwFfVTB63%6}-eSYtT=!~2B5?r%=<v&@s
z%_<I$yng2W{TreR|EBfnz4^9q=0m>Sy_;UKWl2Y$JnN%cAHyg7Y14^w9tShGC(r2G
z)~A;x9knCqwnJ^O_1WCmI>#lvUJrOo*)Fi(6|#w&JpKON^J_GPPn`7PXJKGpJ$3DZ
zg`VZxXJ6Z<cgxD^#f!4bw;mpQ{dr-g(DUPK=CqwU_RHhM;`?i!-*TJ9c>S%J#`;Vi
zMT54myArP^>#cV@dUe?YhsV4Px3dGTUhq1*)vRxxn8zR0n{~&G{-#TQo3l#z-`gYy
zbLKU!94|_KTGV|j^6@En`aa=prlB}T&aV@;japWW3N7|3YdsE3aFUx?c5F&>(96Xy
z1DF$KZN)Nn2tK@XMmo__nTy-o_4FR|Gl8~iUmV`y|55MC)mDL2r;f~xHGMx%PE_S(
z7I<N*=<+=y@{GfgWo?lTnn!<XNNjaIcBNNV(y7A2rg&+_g{30@`H%EF@JK829=_D}
zSkc#Oqx6Gy@Asd(CVxl%OXKtUf9HAU|3CJfpY!0IhgZ%letM2M)OJ?e&!i=<b1l6?
z(jI^0Z+WoZZL)!Eo}<*m3Agx<KCb`SoRcu$;fz<rmu5l3SN3(kFTbx>zVo%ZZbR$#
zefwt~-}m!xjN(&Qh1wTA=2bDx5gB^>=l|`!|L@E1|AsFg$`}2dx}W>^&GUbce*d&Y
zB)=iTQ0bb!``NfqP1Sdz4Do+f*U#d9RGFZb;J=~V<?<osS2xq^KkZ%5X!BwH`w#8!
z^SFLK{9V6e>h=Hc^!EJ-|8EkiS;paLmmtmay1%APeB-hF?Ln{pGu+RX-+ku$t^a=}
zZ;-$D=Y0Ogr}FO}e%$}(pwxry2af!>9d6#*ePNAA{pb7kfA6h7df2{de)zv{eEYs!
z|38VzhHs6C(=u1}m1q5hK1)x#60+Xr_vHE?A1>D4Z$19_;nnwdBtLrd|Gizk=hs~8
zpSSM+JMrvW)qbuuEJ5yO!Tj}cZjoOfhBsWF_w)Py`{HNI-~E3W)*|rd;qKWLfAs4O
zycPCovq(4E)MqIzYbsMn6hANaNy2e+P?r9O$LaN-_^ai9ZU6q`|IWm)w|uTF6`%!)
Mp00i_>zopr0KVf_$^ZZW
literal 0
HcmV?d00001
--
GitLab