From b285d3f1525287049be32b91bc3eeb9a1419579d Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Mon, 17 Oct 2022 10:53:09 +0200
Subject: [PATCH] add notebooks
---
mathematical/Induction_in_B.ipynb | 434 ++++++
mathematical/WolframGraphRewriting.ipynb | 1653 ++++++++++++++++++++++
2 files changed, 2087 insertions(+)
create mode 100644 mathematical/Induction_in_B.ipynb
create mode 100644 mathematical/WolframGraphRewriting.ipynb
diff --git a/mathematical/Induction_in_B.ipynb b/mathematical/Induction_in_B.ipynb
new file mode 100644
index 0000000..5907be8
--- /dev/null
+++ b/mathematical/Induction_in_B.ipynb
@@ -0,0 +1,434 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Induction in B\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Let us try and encode natural numbers using predicate logic:\n",
+ "* zero is a natural number\n",
+ "* if x is a natural number then its successor is a natural number\n",
+ "Nothing else is a natural number.\n",
+ "\n",
+ "We encode the set of natural numbers using the variable *nat* which is a subset of some domain $D$. The successor function is a total function over the domain *D*.\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{zero} = \\mathit{FALSE}$\n",
+ "* $\\mathit{nat} = \\{\\mathit{FALSE}\\}$\n",
+ "* $\\mathit{s} = \\{(\\mathit{FALSE}\\mapsto \\mathit{FALSE}),(\\mathit{TRUE}\\mapsto \\mathit{FALSE})\\}$\n",
+ "* $\\mathit{D} = \\{\\mathit{FALSE},\\mathit{TRUE}\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tzero = FALSE\n",
+ "\tnat = {FALSE}\n",
+ "\ts = {(FALSE↦FALSE),(TRUE↦FALSE)}\n",
+ "\tD = {FALSE,TRUE}"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ " D=BOOL ∧ // just pick one domain here for the notebook\n",
+ " s∈D-->D & zero:D & nat ⊆ D ∧ \n",
+ " zero ∈ nat ∧\n",
+ " ∀x.(x∈nat ⇒ s(x):nat)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "This always allows nat=D as solution. One can try and improve the encoding by using an equivalence:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{zero} = \\mathit{TRUE}$\n",
+ "* $\\mathit{nat} = \\{\\mathit{TRUE},\\mathit{FALSE}\\}$\n",
+ "* $\\mathit{s} = \\{(\\mathit{FALSE}\\mapsto \\mathit{FALSE}),(\\mathit{TRUE}\\mapsto \\mathit{FALSE})\\}$\n",
+ "* $\\mathit{D} = \\{\\mathit{FALSE},\\mathit{TRUE}\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tzero = TRUE\n",
+ "\tnat = {TRUE,FALSE}\n",
+ "\ts = {(FALSE↦FALSE),(TRUE↦FALSE)}\n",
+ "\tD = {FALSE,TRUE}"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "D=BOOL ∧ s∈D-->D ∧ zero:D ∧ nat ⊆ D ∧ \n",
+ "∀x.(x∈D ⇒ (x∈nat ⇔ (x=zero ∨ (∃y.(x=s(y) ∧ y∈nat)))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Does the induction principle hold in this axiomatisation of the natural numbers?\n",
+ "Let's try it out.\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{zero} = \\mathit{FALSE}$\n",
+ "* $\\mathit{nat} = \\{\\mathit{FALSE}\\}$\n",
+ "* $\\mathit{P} = \\{\\mathit{FALSE}\\}$\n",
+ "* $\\mathit{s} = \\{(\\mathit{FALSE}\\mapsto \\mathit{FALSE}),(\\mathit{TRUE}\\mapsto \\mathit{FALSE})\\}$\n",
+ "* $\\mathit{D} = \\{\\mathit{FALSE},\\mathit{TRUE}\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tzero = FALSE\n",
+ "\tnat = {FALSE}\n",
+ "\tP = {FALSE}\n",
+ "\ts = {(FALSE↦FALSE),(TRUE↦FALSE)}\n",
+ "\tD = {FALSE,TRUE}"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "D=BOOL ∧ s∈D-->D ∧ zero:D ∧ nat ⊆ D ∧ \n",
+ "∀x.(x∈D ⇒ (x∈nat ⇔ (x=zero ∨ (∃y.(x=s(y) ∧ y∈nat))))) &\n",
+ "P ⊆ D ∧ // P is our property, we wish to prove that nat ⊆ P\n",
+ "zero∈P ∧ // induction base\n",
+ "∀z.(z∈P ⇒ s(z)∈P) // induction step"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{zero} = \\mathit{FALSE}$\n",
+ "* $\\mathit{nat} = \\{\\mathit{FALSE},\\mathit{TRUE}\\}$\n",
+ "* $\\mathit{P} = \\{\\mathit{FALSE}\\}$\n",
+ "* $\\mathit{s} = \\{(\\mathit{FALSE}\\mapsto \\mathit{FALSE}),(\\mathit{TRUE}\\mapsto \\mathit{TRUE})\\}$\n",
+ "* $\\mathit{D} = \\{\\mathit{FALSE},\\mathit{TRUE}\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tzero = FALSE\n",
+ "\tnat = {FALSE,TRUE}\n",
+ "\tP = {FALSE}\n",
+ "\ts = {(FALSE↦FALSE),(TRUE↦TRUE)}\n",
+ "\tD = {FALSE,TRUE}"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "D=BOOL ∧ s∈D-->D ∧ zero:D ∧ nat ⊆ D ∧ \n",
+ "∀x.(x∈D ⇒\n",
+ " (x∈nat ⇔\n",
+ " (x=zero ∨ (∃y.(x=s(y) ∧ y∈nat))))) ∧ // axiomatisation of natural numbers\n",
+ "P ⊆ D ∧ // P is our property, we wish to prove that nat ⊆ P\n",
+ "zero∈P ∧ // induction base\n",
+ "∀z.(z∈P ⇒ s(z)∈P) ∧ // induction step\n",
+ "\n",
+ "¬(nat ⊆ P)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Visualise"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Visualise\n",
+ "SETS D\n",
+ "CONSTANTS zero, nat, P, s\n",
+ "PROPERTIES\n",
+ " s∈D-->D ∧ zero:D ∧ nat ⊆ D ∧ \n",
+ " ∀x.(x∈D ⇒ (x∈nat ⇔ (x=zero ∨ (∃y.(x=s(y) ∧ y∈nat))))) &\n",
+ " P ⊆ D ∧ // P is our property, we wish to prove that nat ⊆ P\n",
+ " zero∈P ∧ // induction base\n",
+ " ∀z.(z∈P ⇒ s(z)∈P) ∧ // induction step\n",
+ "\n",
+ " ¬(nat ⊆ P) // the induction does not hold\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{zero}\\mapsto \\mathit{zero}),(\\mathit{D2}\\mapsto \\mathit{D2})\\}$"
+ ],
+ "text/plain": [
+ "{(zero↦zero),(D2↦D2)}"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "s"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{zero},\\mathit{D2}\\}$"
+ ],
+ "text/plain": [
+ "{zero,D2}"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "nat"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{zero}\\}$"
+ ],
+ "text/plain": [
+ "{zero}"
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "P"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?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",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"212pt\" height=\"172pt\"\n",
+ " viewBox=\"0.00 0.00 212.00 172.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 168)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-168 209,-168 209,5 -4,5\"/>\n",
+ "<g id=\"graph2\" class=\"cluster\"><title>cluster_D</title>\n",
+ "<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-82 8,-156 196,-156 196,-82 8,-82\"/>\n",
+ "<text text-anchor=\"middle\" x=\"102\" y=\"-141.2\" font-family=\"Times,serif\" font-size=\"12.00\">D</text>\n",
+ "</g>\n",
+ "<!-- D2 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>D2</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-126 16,-126 16,-90 70,-90 70,-126\"/>\n",
+ "<text text-anchor=\"middle\" x=\"43\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">D2</text>\n",
+ "</g>\n",
+ "<!-- D2->D2 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>D2->D2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M70.2408,-116.242C80.0239,-116.419 88,-113.672 88,-108 88,-104.544 85.0382,-102.173 80.5105,-100.889\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.5639,-97.3739 70.2408,-99.7581 79.7975,-104.332 80.5639,-97.3739\"/>\n",
+ "<text text-anchor=\"middle\" x=\"90.7223\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">s</text>\n",
+ "</g>\n",
+ "<!-- ROOT-NODE -->\n",
+ "<g id=\"node6\" class=\"node\"><title>ROOT-NODE</title>\n",
+ "<polygon fill=\"lightblue\" stroke=\"lightblue\" points=\"107,-36 11.6349,-18 107,-3.55271e-15 202.365,-18 107,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"107\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">ROOT-NODE</text>\n",
+ "</g>\n",
+ "<!-- D2->ROOT-NODE -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>D2->ROOT-NODE</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M55.6443,-89.614C65.5109,-76.0476 79.3097,-57.0741 90.1196,-42.2105\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"93.0354,-44.1519 96.0866,-34.0059 87.3743,-40.0347 93.0354,-44.1519\"/>\n",
+ "<text text-anchor=\"middle\" x=\"89.5526\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">nat</text>\n",
+ "</g>\n",
+ "<!-- zero -->\n",
+ "<g id=\"node3\" class=\"node\"><title>zero</title>\n",
+ "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"165,-126 111,-126 111,-90 165,-90 165,-126\"/>\n",
+ "<text text-anchor=\"middle\" x=\"138\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">zero</text>\n",
+ "</g>\n",
+ "<!-- zero->zero -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>zero->zero</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M165.241,-116.242C175.024,-116.419 183,-113.672 183,-108 183,-104.544 180.038,-102.173 175.51,-100.889\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"175.564,-97.3739 165.241,-99.7581 174.797,-104.332 175.564,-97.3739\"/>\n",
+ "<text text-anchor=\"middle\" x=\"185.722\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">s</text>\n",
+ "</g>\n",
+ "<!-- zero->ROOT-NODE -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>zero->ROOT-NODE</title>\n",
+ "<path fill=\"none\" stroke=\"sienna\" d=\"M120.275,-89.9192C115.862,-84.6237 111.689,-78.467 109.217,-72 106.12,-63.8947 105.002,-54.5764 104.826,-46.036\"/>\n",
+ "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"108.331,-45.8513 105.029,-35.7839 101.332,-45.7126 108.331,-45.8513\"/>\n",
+ "<text text-anchor=\"middle\" x=\"113.891\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">P</text>\n",
+ "</g>\n",
+ "<!-- zero->ROOT-NODE -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>zero->ROOT-NODE</title>\n",
+ "<path fill=\"none\" stroke=\"#473c8b\" d=\"M131.875,-89.614C127.389,-76.8772 121.223,-59.3744 116.152,-44.9812\"/>\n",
+ "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"119.318,-43.4319 112.694,-35.163 112.715,-45.7578 119.318,-43.4319\"/>\n",
+ "<text text-anchor=\"middle\" x=\"133.553\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">nat</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: state_as_graph []>"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot state_as_graph"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
+ "Comment: One can go even further and introduce Clark's Equality Theory to stipulate that s(x) is different from zero,... But this does not solve the problem. It cannot be solved in pure predicate logic."
+ ]
+ },
+ {
+ "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
+}
diff --git a/mathematical/WolframGraphRewriting.ipynb b/mathematical/WolframGraphRewriting.ipynb
new file mode 100644
index 0000000..8bb7ae0
--- /dev/null
+++ b/mathematical/WolframGraphRewriting.ipynb
@@ -0,0 +1,1653 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Wolfram Graph Rewriting\n",
+ "\n",
+ "Inspired by [article about graph rewriting, complexity and physics](https://writings.stephenwolfram.com/2020/04/finally-we-may-have-a-path-to-the-fundamental-theory-of-physics-and-its-beautiful/)\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: WolframGraphRewriting"
+ ]
+ },
+ "execution_count": 36,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE WolframGraphRewriting\n",
+ "DEFINITIONS\n",
+ " NODES == 1..50;\n",
+ " CUSTOM_GRAPH_NODES == ((dom(g)/\\ran(g))*{\"green\"}) \\/\n",
+ " ((ran(g)\\dom(g))*{\"blue\"})\\/\n",
+ " ((dom(g)\\ran(g))*{\"gray\"});\n",
+ " CUSTOM_GRAPH_EDGES == g;\n",
+ "VARIABLES g\n",
+ "INVARIANT\n",
+ " g : NODES <-> NODES\n",
+ "INITIALISATION\n",
+ " g := {(1 |-> 2), (2 |-> 3), (3 |-> 4), (2 |-> 4)}\n",
+ "OPERATIONS\n",
+ " Rewrite(x,y,z,w) = PRE x|->y : g & x|->z : g & y/=z & \n",
+ " w = min(NODES\\(dom(g)\\/ran(g))) THEN\n",
+ " g := (g \\ {x|->y}) \\/ {x|->w, z|->w, y|->w}\n",
+ " END\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 37,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 0: $initialise_machine()"
+ ]
+ },
+ "execution_count": 37,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 38,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?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",
+ " -->\n",
+ "<!-- Title: prob_graph Pages: 1 -->\n",
+ "<svg width=\"540pt\" height=\"717pt\"\n",
+ " viewBox=\"0.00 0.00 540.00 717.37\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(0.985401 0.985401) rotate(0) translate(4 724)\">\n",
+ "<title>prob_graph</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-724 545,-724 545,5 -4,5\"/>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>0</title>\n",
+ "<polygon fill=\"gray\" stroke=\"gray\" points=\"422.911,-694 368.911,-694 368.911,-658 422.911,-658 422.911,-694\"/>\n",
+ "<text text-anchor=\"middle\" x=\"395.911\" y=\"-672.4\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node2\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"422.911,-483 368.911,-483 368.911,-447 422.911,-447 422.911,-483\"/>\n",
+ "<text text-anchor=\"middle\" x=\"395.911\" y=\"-461.4\" font-family=\"Times,serif\" font-size=\"12.00\">2</text>\n",
+ "</g>\n",
+ "<!-- 0->1 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>0->1</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M395.911,-657.897C395.911,-621.677 395.911,-536.983 395.911,-493.233\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"399.411,-493.047 395.911,-483.047 392.411,-493.047 399.411,-493.047\"/>\n",
+ "<text text-anchor=\"middle\" x=\"398.911\" y=\"-567.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"170.911,-273 116.911,-273 116.911,-237 170.911,-237 170.911,-273\"/>\n",
+ "<text text-anchor=\"middle\" x=\"143.911\" y=\"-251.4\" font-family=\"Times,serif\" font-size=\"12.00\">3</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M375.289,-446.978C330.434,-409.955 223.919,-322.039 172.568,-279.654\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"174.758,-276.923 164.818,-273.257 170.302,-282.322 174.758,-276.923\"/>\n",
+ "<text text-anchor=\"middle\" x=\"280.911\" y=\"-356.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node4\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"395.911,-62 341.911,-62 341.911,-26 395.911,-26 395.911,-62\"/>\n",
+ "<text text-anchor=\"middle\" x=\"368.911\" y=\"-40.4\" font-family=\"Times,serif\" font-size=\"12.00\">4</text>\n",
+ "</g>\n",
+ "<!-- 1->3 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>1->3</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M394.802,-446.794C390.623,-381.933 375.798,-151.88 370.671,-72.3142\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"374.15,-71.8729 370.014,-62.1187 367.164,-72.3231 374.15,-71.8729\"/>\n",
+ "<text text-anchor=\"middle\" x=\"385.911\" y=\"-251.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M162.324,-236.897C202.307,-199.756 297.163,-111.646 343.098,-68.9769\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"345.615,-71.4167 350.559,-62.0466 340.851,-66.288 345.615,-71.4167\"/>\n",
+ "<text text-anchor=\"middle\" x=\"266.911\" y=\"-145.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: custom_graph []>"
+ ]
+ },
+ "execution_count": 38,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot custom_graph"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 39,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,4,3,5)"
+ ]
+ },
+ "execution_count": 39,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 40,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?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",
+ " -->\n",
+ "<!-- Title: prob_graph Pages: 1 -->\n",
+ "<svg width=\"540pt\" height=\"717pt\"\n",
+ " viewBox=\"0.00 0.00 540.00 717.37\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(0.985401 0.985401) rotate(0) translate(4 724)\">\n",
+ "<title>prob_graph</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-724 545,-724 545,5 -4,5\"/>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>0</title>\n",
+ "<polygon fill=\"gray\" stroke=\"gray\" points=\"456.273,-704 402.273,-704 402.273,-668 456.273,-668 456.273,-704\"/>\n",
+ "<text text-anchor=\"middle\" x=\"429.273\" y=\"-682.4\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node2\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"456.273,-541 402.273,-541 402.273,-505 456.273,-505 456.273,-541\"/>\n",
+ "<text text-anchor=\"middle\" x=\"429.273\" y=\"-519.4\" font-family=\"Times,serif\" font-size=\"12.00\">2</text>\n",
+ "</g>\n",
+ "<!-- 0->1 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>0->1</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M429.273,-667.77C429.273,-639.929 429.273,-584.813 429.273,-551.498\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"432.773,-551.106 429.273,-541.106 425.773,-551.106 432.773,-551.106\"/>\n",
+ "<text text-anchor=\"middle\" x=\"432.273\" y=\"-600.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"309.273,-378 255.273,-378 255.273,-342 309.273,-342 309.273,-378\"/>\n",
+ "<text text-anchor=\"middle\" x=\"282.273\" y=\"-356.4\" font-family=\"Times,serif\" font-size=\"12.00\">3</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M413.541,-504.77C387.348,-476.082 334.712,-418.433 304.658,-385.518\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"307.219,-383.131 297.891,-378.106 302.049,-387.851 307.219,-383.131\"/>\n",
+ "<text text-anchor=\"middle\" x=\"362.273\" y=\"-437.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node5\" class=\"node\"><title>4</title>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"395.273,-52 341.273,-52 341.273,-16 395.273,-16 395.273,-52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"368.273\" y=\"-30.4\" font-family=\"Times,serif\" font-size=\"12.00\">5</text>\n",
+ "</g>\n",
+ "<!-- 1->4 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>1->4</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M427.137,-504.953C418.089,-432.713 382.861,-151.467 371.691,-62.2883\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"375.138,-61.6485 370.422,-52.1611 368.192,-62.5186 375.138,-61.6485\"/>\n",
+ "<text text-anchor=\"middle\" x=\"402.273\" y=\"-275.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node4\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"137.273,-215 83.2727,-215 83.2727,-179 137.273,-179 137.273,-215\"/>\n",
+ "<text text-anchor=\"middle\" x=\"110.273\" y=\"-193.4\" font-family=\"Times,serif\" font-size=\"12.00\">4</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M263.866,-341.77C233.088,-312.961 171.109,-254.946 136.022,-222.102\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"138.24,-219.384 128.547,-215.106 133.456,-224.495 138.24,-219.384\"/>\n",
+ "<text text-anchor=\"middle\" x=\"205.273\" y=\"-275.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2->4 -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>2->4</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M286.896,-341.58C301.074,-288.165 344.011,-126.406 361.122,-61.9392\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"364.548,-62.6758 363.731,-52.1126 357.782,-60.8799 364.548,-62.6758\"/>\n",
+ "<text text-anchor=\"middle\" x=\"332.273\" y=\"-193.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->4 -->\n",
+ "<g id=\"edge12\" class=\"edge\"><title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M137.396,-179.074C184.237,-149.844 280.28,-89.91 332.518,-57.3121\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"334.495,-60.2037 341.126,-51.9403 330.789,-54.2652 334.495,-60.2037\"/>\n",
+ "<text text-anchor=\"middle\" x=\"250.273\" y=\"-112.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: custom_graph []>"
+ ]
+ },
+ "execution_count": 40,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot custom_graph"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 41,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,5,3,6)"
+ ]
+ },
+ "execution_count": 41,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 42,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,6,3,7)"
+ ]
+ },
+ "execution_count": 42,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 43,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,7,3,8)"
+ ]
+ },
+ "execution_count": 43,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 44,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?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",
+ " -->\n",
+ "<!-- Title: prob_graph Pages: 1 -->\n",
+ "<svg width=\"540pt\" height=\"680pt\"\n",
+ " viewBox=\"0.00 0.00 540.00 679.75\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph1\" class=\"graph\" transform=\"scale(0.933718 0.933718) rotate(0) translate(4 724)\">\n",
+ "<title>prob_graph</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-724 575.333,-724 575.333,5 -4,5\"/>\n",
+ "<!-- 0 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>0</title>\n",
+ "<polygon fill=\"gray\" stroke=\"gray\" points=\"507.333,-718 453.333,-718 453.333,-682 507.333,-682 507.333,-718\"/>\n",
+ "<text text-anchor=\"middle\" x=\"480.333\" y=\"-696.4\" font-family=\"Times,serif\" font-size=\"12.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node2\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"507.333,-621 453.333,-621 453.333,-585 507.333,-585 507.333,-621\"/>\n",
+ "<text text-anchor=\"middle\" x=\"480.333\" y=\"-599.4\" font-family=\"Times,serif\" font-size=\"12.00\">2</text>\n",
+ "</g>\n",
+ "<!-- 0->1 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>0->1</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M480.333,-681.576C480.333,-667.648 480.333,-647.861 480.333,-631.757\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"483.833,-631.314 480.333,-621.314 476.833,-631.314 483.833,-631.314\"/>\n",
+ "<text text-anchor=\"middle\" x=\"483.333\" y=\"-647.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"353.333,-524 299.333,-524 299.333,-488 353.333,-488 353.333,-524\"/>\n",
+ "<text text-anchor=\"middle\" x=\"326.333\" y=\"-502.4\" font-family=\"Times,serif\" font-size=\"12.00\">3</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M453.156,-585.235C427.833,-569.613 389.912,-546.221 362.132,-529.084\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"363.846,-526.029 353.498,-523.757 360.171,-531.986 363.846,-526.029\"/>\n",
+ "<text text-anchor=\"middle\" x=\"415.333\" y=\"-550.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 7 -->\n",
+ "<g id=\"node8\" class=\"node\"><title>7</title>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"489.333,-38 435.333,-38 435.333,-2 489.333,-2 489.333,-38\"/>\n",
+ "<text text-anchor=\"middle\" x=\"462.333\" y=\"-16.4\" font-family=\"Times,serif\" font-size=\"12.00\">8</text>\n",
+ "</g>\n",
+ "<!-- 1->7 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>1->7</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M507.374,-586.496C531.93,-570.174 564.333,-542.005 564.333,-507 564.333,-507 564.333,-507 564.333,-116 564.333,-78.9878 527.925,-52.2916 498.612,-36.7961\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"499.906,-33.5289 489.4,-32.1598 496.759,-39.7817 499.906,-33.5289\"/>\n",
+ "<text text-anchor=\"middle\" x=\"567.333\" y=\"-307.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node4\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"87.3333,-427 33.3333,-427 33.3333,-391 87.3333,-391 87.3333,-427\"/>\n",
+ "<text text-anchor=\"middle\" x=\"60.3333\" y=\"-405.4\" font-family=\"Times,serif\" font-size=\"12.00\">4</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M299.313,-498.696C269.718,-491.496 221.042,-478.782 180.333,-464 151.646,-453.583 120.22,-439.333 96.7266,-428.086\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"98.0223,-424.825 87.4955,-423.627 94.9774,-431.129 98.0223,-424.825\"/>\n",
+ "<text text-anchor=\"middle\" x=\"183.333\" y=\"-453.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node5\" class=\"node\"><title>4</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"180.333,-329 126.333,-329 126.333,-293 180.333,-293 180.333,-329\"/>\n",
+ "<text text-anchor=\"middle\" x=\"153.333\" y=\"-307.4\" font-family=\"Times,serif\" font-size=\"12.00\">5</text>\n",
+ "</g>\n",
+ "<!-- 2->4 -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>2->4</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M299.041,-490.986C286.726,-483.892 272.477,-474.547 261.333,-464 220.889,-425.722 186.034,-370.255 167.518,-337.983\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"170.49,-336.127 162.523,-329.143 164.395,-339.571 170.49,-336.127\"/>\n",
+ "<text text-anchor=\"middle\" x=\"229.333\" y=\"-405.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node6\" class=\"node\"><title>5</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"282.333,-232 228.333,-232 228.333,-196 282.333,-196 282.333,-232\"/>\n",
+ "<text text-anchor=\"middle\" x=\"255.333\" y=\"-210.4\" font-family=\"Times,serif\" font-size=\"12.00\">6</text>\n",
+ "</g>\n",
+ "<!-- 2->5 -->\n",
+ "<g id=\"edge12\" class=\"edge\"><title>2->5</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M322.105,-487.728C310.216,-439.171 276.43,-301.168 261.999,-242.228\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"265.318,-241.063 259.54,-232.182 258.518,-242.727 265.318,-241.063\"/>\n",
+ "<text text-anchor=\"middle\" x=\"295.333\" y=\"-356.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 6 -->\n",
+ "<g id=\"node7\" class=\"node\"><title>6</title>\n",
+ "<polygon fill=\"green\" stroke=\"green\" points=\"367.333,-135 313.333,-135 313.333,-99 367.333,-99 367.333,-135\"/>\n",
+ "<text text-anchor=\"middle\" x=\"340.333\" y=\"-113.4\" font-family=\"Times,serif\" font-size=\"12.00\">7</text>\n",
+ "</g>\n",
+ "<!-- 2->6 -->\n",
+ "<g id=\"edge14\" class=\"edge\"><title>2->6</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M342.19,-487.913C357.162,-469.943 377.333,-440.138 377.333,-410 377.333,-410 377.333,-410 377.333,-213 377.333,-188.319 366.356,-162.34 356.359,-143.799\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"359.4,-142.066 351.435,-135.081 353.306,-145.509 359.4,-142.066\"/>\n",
+ "<text text-anchor=\"middle\" x=\"380.333\" y=\"-307.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2->7 -->\n",
+ "<g id=\"edge16\" class=\"edge\"><title>2->7</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M353.528,-499.002C393.216,-488.462 462.333,-462.562 462.333,-410 462.333,-410 462.333,-410 462.333,-116 462.333,-93.1449 462.333,-67.1969 462.333,-48.2012\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"465.833,-48.162 462.333,-38.162 458.833,-48.162 465.833,-48.162\"/>\n",
+ "<text text-anchor=\"middle\" x=\"465.333\" y=\"-259.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->4 -->\n",
+ "<g id=\"edge18\" class=\"edge\"><title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M76.9599,-390.837C91.6394,-375.684 113.207,-353.421 129.682,-336.414\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"132.407,-338.632 136.851,-329.014 127.379,-333.761 132.407,-338.632\"/>\n",
+ "<text text-anchor=\"middle\" x=\"116.333\" y=\"-356.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 4->5 -->\n",
+ "<g id=\"edge20\" class=\"edge\"><title>4->5</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M172.042,-292.576C188.001,-277.711 211.129,-256.171 228.965,-239.558\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"231.811,-241.691 236.744,-232.314 227.04,-236.568 231.811,-241.691\"/>\n",
+ "<text text-anchor=\"middle\" x=\"213.333\" y=\"-259.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 5->6 -->\n",
+ "<g id=\"edge22\" class=\"edge\"><title>5->6</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M270.924,-195.576C284.104,-180.845 303.149,-159.559 317.957,-143.009\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"320.782,-145.1 324.842,-135.314 315.566,-140.433 320.782,-145.1\"/>\n",
+ "<text text-anchor=\"middle\" x=\"305.333\" y=\"-162.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 6->7 -->\n",
+ "<g id=\"edge24\" class=\"edge\"><title>6->7</title>\n",
+ "<path fill=\"none\" stroke=\"blue\" d=\"M362.427,-98.7962C382.032,-83.5294 410.841,-61.0964 432.491,-44.2376\"/>\n",
+ "<polygon fill=\"blue\" stroke=\"blue\" points=\"434.665,-46.9812 440.404,-38.0758 430.364,-41.4582 434.665,-46.9812\"/>\n",
+ "<text text-anchor=\"middle\" x=\"411.333\" y=\"-65.4\" font-family=\"Times,serif\" font-size=\"12.00\">g</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: custom_graph []>"
+ ]
+ },
+ "execution_count": 44,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot custom_graph"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Preference changed: DOT_ENGINE = sfdp\n"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":pref DOT_ENGINE=sfdp"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?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",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"644pt\" height=\"384pt\"\n",
+ " viewBox=\"0.00 0.00 643.97 383.75\" 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 379.752)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-379.752 640.968,-379.752 640.968,5 -4,5\"/>\n",
+ "<!-- 7 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>7</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"187.299,-36 133.299,-36 133.299,-0 187.299,-0 187.299,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"160.299\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">7</text>\n",
+ "</g>\n",
+ "<!-- 8 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>8</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"337.364,-82.007 283.364,-82.007 283.364,-46.007 337.364,-46.007 337.364,-82.007\"/>\n",
+ "<text text-anchor=\"middle\" x=\"310.364\" y=\"-59.807\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+ "</g>\n",
+ "<!-- 7->8 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>7->8</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M187.475,-26.3315C211.516,-33.702 246.806,-44.5215 273.409,-52.6772\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"272.55,-56.0749 283.137,-55.6598 274.602,-49.3823 272.55,-56.0749\"/>\n",
+ "<text text-anchor=\"middle\" x=\"227.442\" y=\"-44.3044\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 6 -->\n",
+ "<g id=\"node4\" class=\"node\"><title>6</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"63.3681,-122.991 9.36812,-122.991 9.36812,-86.9914 63.3681,-86.9914 63.3681,-122.991\"/>\n",
+ "<text text-anchor=\"middle\" x=\"36.3681\" y=\"-100.791\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+ "</g>\n",
+ "<!-- 6->7 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>6->7</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M62.0468,-86.9667C80.6577,-73.9031 106.011,-56.1064 126.302,-41.8638\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"128.48,-44.6116 134.654,-36.0016 124.458,-38.8822 128.48,-44.6116\"/>\n",
+ "<text text-anchor=\"middle\" x=\"89.1744\" y=\"-52.2153\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node6\" class=\"node\"><title>5</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-271.029 0,-271.029 0,-235.029 54,-235.029 54,-271.029\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-248.829\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+ "</g>\n",
+ "<!-- 5->6 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>5->6</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M28.1487,-234.877C29.7501,-209.572 32.6693,-163.441 34.5631,-133.515\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"38.0714,-133.493 35.21,-123.292 31.0853,-133.051 38.0714,-133.493\"/>\n",
+ "<text text-anchor=\"middle\" x=\"26.3559\" y=\"-179.996\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node8\" class=\"node\"><title>4</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"143.326,-375.752 89.3259,-375.752 89.3259,-339.752 143.326,-339.752 143.326,-375.752\"/>\n",
+ "<text text-anchor=\"middle\" x=\"116.326\" y=\"-353.552\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+ "</g>\n",
+ "<!-- 4->5 -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>4->5</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M100.767,-339.511C86.4208,-322.692 64.9796,-297.555 48.9052,-278.71\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"51.5336,-276.399 42.3811,-271.062 46.2079,-280.941 51.5336,-276.399\"/>\n",
+ "<text text-anchor=\"middle\" x=\"67.8359\" y=\"-310.911\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node10\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"219.602,-198.598 165.602,-198.598 165.602,-162.598 219.602,-162.598 219.602,-198.598\"/>\n",
+ "<text text-anchor=\"middle\" x=\"192.602\" y=\"-176.398\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+ "</g>\n",
+ "<!-- 3->7 -->\n",
+ "<g id=\"edge12\" class=\"edge\"><title>3->7</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M189.021,-162.576C183.419,-134.374 172.534,-79.5842 165.891,-46.1478\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"169.277,-45.2291 163.896,-36.1028 162.411,-46.5932 169.277,-45.2291\"/>\n",
+ "<text text-anchor=\"middle\" x=\"171.456\" y=\"-101.162\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->8 -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>3->8</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M211.002,-162.381C230.879,-142.702 262.684,-111.213 284.941,-89.1765\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"287.449,-91.6193 292.092,-82.0964 282.524,-86.6449 287.449,-91.6193\"/>\n",
+ "<text text-anchor=\"middle\" x=\"241.972\" y=\"-115.579\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->6 -->\n",
+ "<g id=\"edge14\" class=\"edge\"><title>3->6</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M165.388,-167.429C139.703,-154.999 101.014,-136.276 72.7018,-122.575\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"74.0577,-119.342 63.5317,-118.137 71.0085,-125.643 74.0577,-119.342\"/>\n",
+ "<text text-anchor=\"middle\" x=\"115.045\" y=\"-149.802\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->5 -->\n",
+ "<g id=\"edge16\" class=\"edge\"><title>3->5</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M165.256,-192.559C137.486,-204.705 94.3147,-223.587 63.6076,-237.018\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"61.8705,-233.957 54.1111,-241.171 64.6757,-240.371 61.8705,-233.957\"/>\n",
+ "<text text-anchor=\"middle\" x=\"110.432\" y=\"-201.588\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->4 -->\n",
+ "<g id=\"edge18\" class=\"edge\"><title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M184.726,-198.89C171.331,-230 144.036,-293.395 128.277,-329.996\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"124.899,-328.991 124.159,-339.56 131.328,-331.76 124.899,-328.991\"/>\n",
+ "<text text-anchor=\"middle\" x=\"149.501\" y=\"-257.243\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node16\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"447.416,-197.032 393.416,-197.032 393.416,-161.032 447.416,-161.032 447.416,-197.032\"/>\n",
+ "<text text-anchor=\"middle\" x=\"420.416\" y=\"-174.832\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "</g>\n",
+ "<!-- 2->8 -->\n",
+ "<g id=\"edge20\" class=\"edge\"><title>2->8</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M402.978,-160.806C384.544,-141.539 355.33,-111.006 334.648,-89.3889\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"337.162,-86.9537 327.72,-82.1478 332.104,-91.793 337.162,-86.9537\"/>\n",
+ "<text text-anchor=\"middle\" x=\"375.813\" y=\"-114.897\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge22\" class=\"edge\"><title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M393.388,-179.218C352.821,-179.497 276.058,-180.025 230.097,-180.34\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"229.924,-176.841 219.949,-180.41 229.973,-183.841 229.924,-176.841\"/>\n",
+ "<text text-anchor=\"middle\" x=\"311.742\" y=\"-184.579\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node19\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"635.968,-246.886 581.968,-246.886 581.968,-210.886 635.968,-210.886 635.968,-246.886\"/>\n",
+ "<text text-anchor=\"middle\" x=\"608.968\" y=\"-224.686\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge24\" class=\"edge\"><title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M581.953,-221.744C549.282,-213.105 494.126,-198.522 457.493,-188.836\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"458.249,-185.415 447.686,-186.243 456.459,-192.183 458.249,-185.415\"/>\n",
+ "<text text-anchor=\"middle\" x=\"517.723\" y=\"-210.09\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [g]>"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph g"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,8,3,9)"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,9,3,10)"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,10,3,11)"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,11,3,12)"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?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",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"748pt\" height=\"454pt\"\n",
+ " viewBox=\"0.00 0.00 748.24 453.52\" 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 449.52)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-449.52 745.24,-449.52 745.24,5 -4,5\"/>\n",
+ "<!-- 11 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>11</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"391.579,-126.561 337.579,-126.561 337.579,-90.5607 391.579,-90.5607 391.579,-126.561\"/>\n",
+ "<text text-anchor=\"middle\" x=\"364.579\" y=\"-104.361\" font-family=\"Times,serif\" font-size=\"14.00\">11</text>\n",
+ "</g>\n",
+ "<!-- 12 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>12</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"362.907,-258.993 308.907,-258.993 308.907,-222.993 362.907,-222.993 362.907,-258.993\"/>\n",
+ "<text text-anchor=\"middle\" x=\"335.907\" y=\"-236.793\" font-family=\"Times,serif\" font-size=\"14.00\">12</text>\n",
+ "</g>\n",
+ "<!-- 11->12 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>11->12</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M360.652,-126.697C355.854,-148.862 347.679,-186.621 342.046,-212.637\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"338.574,-212.136 339.878,-222.65 345.415,-213.617 338.574,-212.136\"/>\n",
+ "<text text-anchor=\"middle\" x=\"345.349\" y=\"-164.467\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 10 -->\n",
+ "<g id=\"node4\" class=\"node\"><title>10</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"476.704,-39.2407 422.704,-39.2407 422.704,-3.24072 476.704,-3.24072 476.704,-39.2407\"/>\n",
+ "<text text-anchor=\"middle\" x=\"449.704\" y=\"-17.0407\" font-family=\"Times,serif\" font-size=\"14.00\">10</text>\n",
+ "</g>\n",
+ "<!-- 10->11 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>10->11</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M432.066,-39.3335C419.739,-51.9782 403.106,-69.0404 389.437,-83.0617\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"386.669,-80.8874 382.194,-90.4911 391.681,-85.7738 386.669,-80.8874\"/>\n",
+ "<text text-anchor=\"middle\" x=\"403.751\" y=\"-50.9976\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 9 -->\n",
+ "<g id=\"node6\" class=\"node\"><title>9</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"599.259,-36 545.259,-36 545.259,-0 599.259,-0 599.259,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"572.259\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">9</text>\n",
+ "</g>\n",
+ "<!-- 9->10 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>9->10</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M545.06,-18.7192C528.003,-19.1703 505.781,-19.7579 487.081,-20.2524\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"486.731,-16.7603 476.827,-20.5235 486.916,-23.7579 486.731,-16.7603\"/>\n",
+ "<text text-anchor=\"middle\" x=\"516.07\" y=\"-6.28579\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 8 -->\n",
+ "<g id=\"node8\" class=\"node\"><title>8</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"699.153,-106.786 645.153,-106.786 645.153,-70.7859 699.153,-70.7859 699.153,-106.786\"/>\n",
+ "<text text-anchor=\"middle\" x=\"672.153\" y=\"-84.5859\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+ "</g>\n",
+ "<!-- 8->9 -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>8->9</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M646.687,-70.7405C634.358,-62.0043 619.386,-51.3946 606.112,-41.9882\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"607.861,-38.9385 597.678,-36.0125 603.814,-44.6499 607.861,-38.9385\"/>\n",
+ "<text text-anchor=\"middle\" x=\"621.399\" y=\"-60.1644\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 7 -->\n",
+ "<g id=\"node10\" class=\"node\"><title>7</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"740.24,-220.327 686.24,-220.327 686.24,-184.327 740.24,-184.327 740.24,-220.327\"/>\n",
+ "<text text-anchor=\"middle\" x=\"713.24\" y=\"-198.127\" font-family=\"Times,serif\" font-size=\"14.00\">7</text>\n",
+ "</g>\n",
+ "<!-- 7->8 -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>7->8</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M706.639,-184.084C700.05,-165.876 689.838,-137.655 682.234,-116.643\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"685.432,-115.195 678.738,-106.983 678.85,-117.577 685.432,-115.195\"/>\n",
+ "<text text-anchor=\"middle\" x=\"700.437\" y=\"-144.164\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 6 -->\n",
+ "<g id=\"node12\" class=\"node\"><title>6</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"710.868,-337.667 656.868,-337.667 656.868,-301.667 710.868,-301.667 710.868,-337.667\"/>\n",
+ "<text text-anchor=\"middle\" x=\"683.868\" y=\"-315.467\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+ "</g>\n",
+ "<!-- 6->7 -->\n",
+ "<g id=\"edge12\" class=\"edge\"><title>6->7</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M688.393,-301.59C693.144,-282.61 700.678,-252.512 706.206,-230.43\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"709.629,-231.168 708.662,-220.618 702.838,-229.469 709.629,-231.168\"/>\n",
+ "<text text-anchor=\"middle\" x=\"691.299\" y=\"-260.81\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node14\" class=\"node\"><title>5</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"623.671,-418.361 569.671,-418.361 569.671,-382.361 623.671,-382.361 623.671,-418.361\"/>\n",
+ "<text text-anchor=\"middle\" x=\"596.671\" y=\"-396.161\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+ "</g>\n",
+ "<!-- 5->6 -->\n",
+ "<g id=\"edge14\" class=\"edge\"><title>5->6</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M616.457,-382.05C628.386,-371.011 643.746,-356.796 656.791,-344.725\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"659.197,-347.266 664.16,-337.906 654.443,-342.129 659.197,-347.266\"/>\n",
+ "<text text-anchor=\"middle\" x=\"642.624\" y=\"-366.188\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node16\" class=\"node\"><title>4</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"515.745,-445.52 461.745,-445.52 461.745,-409.52 515.745,-409.52 515.745,-445.52\"/>\n",
+ "<text text-anchor=\"middle\" x=\"488.745\" y=\"-423.32\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+ "</g>\n",
+ "<!-- 4->5 -->\n",
+ "<g id=\"edge16\" class=\"edge\"><title>4->5</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M515.98,-420.667C529.145,-417.354 545.15,-413.326 559.423,-409.734\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"560.602,-413.047 569.446,-407.212 558.894,-406.258 560.602,-413.047\"/>\n",
+ "<text text-anchor=\"middle\" x=\"535.702\" y=\"-402\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node18\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"533.731,-231.177 479.731,-231.177 479.731,-195.177 533.731,-195.177 533.731,-231.177\"/>\n",
+ "<text text-anchor=\"middle\" x=\"506.731\" y=\"-208.977\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+ "</g>\n",
+ "<!-- 3->11 -->\n",
+ "<g id=\"edge20\" class=\"edge\"><title>3->11</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M481.97,-194.955C458.529,-177.703 423.183,-151.69 397.402,-132.717\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"399.185,-129.683 389.056,-126.575 395.036,-135.321 399.185,-129.683\"/>\n",
+ "<text text-anchor=\"middle\" x=\"433.686\" y=\"-167.636\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->12 -->\n",
+ "<g id=\"edge18\" class=\"edge\"><title>3->12</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M479.663,-217.585C450.886,-222.271 405.181,-229.713 373.048,-234.945\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"372.438,-231.498 363.131,-236.56 373.563,-238.407 372.438,-231.498\"/>\n",
+ "<text text-anchor=\"middle\" x=\"427.356\" y=\"-231.065\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->10 -->\n",
+ "<g id=\"edge22\" class=\"edge\"><title>3->10</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M501.366,-195.12C491.367,-161.468 469.826,-88.9648 457.961,-49.0307\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"461.299,-47.9785 455.096,-39.3895 454.589,-49.9722 461.299,-47.9785\"/>\n",
+ "<text text-anchor=\"middle\" x=\"473.663\" y=\"-118.876\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->9 -->\n",
+ "<g id=\"edge24\" class=\"edge\"><title>3->9</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M512.778,-195.165C524.257,-160.975 549.274,-86.4626 562.921,-45.8123\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"566.266,-46.8462 566.131,-36.2522 559.63,-44.6182 566.266,-46.8462\"/>\n",
+ "<text text-anchor=\"middle\" x=\"543.85\" y=\"-118.289\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->8 -->\n",
+ "<g id=\"edge26\" class=\"edge\"><title>3->8</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M530.785,-195.09C559.575,-173.441 607.9,-137.102 639.907,-113.034\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"642.181,-115.703 648.07,-106.895 637.974,-110.108 642.181,-115.703\"/>\n",
+ "<text text-anchor=\"middle\" x=\"579.346\" y=\"-141.862\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->7 -->\n",
+ "<g id=\"edge28\" class=\"edge\"><title>3->7</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M534.154,-211.737C570.59,-209.822 635.102,-206.432 675.94,-204.286\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"676.23,-207.776 686.033,-203.756 675.863,-200.786 676.23,-207.776\"/>\n",
+ "<text text-anchor=\"middle\" x=\"605.047\" y=\"-194.811\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->6 -->\n",
+ "<g id=\"edge30\" class=\"edge\"><title>3->6</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M534.02,-229.583C564.666,-248.007 614.511,-277.972 648.214,-298.234\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"646.464,-301.265 656.838,-303.418 650.071,-295.266 646.464,-301.265\"/>\n",
+ "<text text-anchor=\"middle\" x=\"596.117\" y=\"-251.708\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->5 -->\n",
+ "<g id=\"edge32\" class=\"edge\"><title>3->5</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M515.519,-231.466C531.41,-264.54 565,-334.446 583.595,-373.147\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"580.494,-374.775 587.98,-382.273 586.804,-371.744 580.494,-374.775\"/>\n",
+ "<text text-anchor=\"middle\" x=\"556.557\" y=\"-295.107\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->4 -->\n",
+ "<g id=\"edge34\" class=\"edge\"><title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M505.197,-231.452C502.058,-268.863 494.88,-354.406 491.129,-399.115\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"487.623,-399.034 490.275,-409.292 494.599,-399.62 487.623,-399.034\"/>\n",
+ "<text text-anchor=\"middle\" x=\"503.163\" y=\"-311.084\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node28\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"254.91,-259.091 200.91,-259.091 200.91,-223.091 254.91,-223.091 254.91,-259.091\"/>\n",
+ "<text text-anchor=\"middle\" x=\"227.91\" y=\"-236.891\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "</g>\n",
+ "<!-- 2->12 -->\n",
+ "<g id=\"edge36\" class=\"edge\"><title>2->12</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M255.162,-241.066C268.336,-241.054 284.352,-241.04 298.635,-241.027\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"298.667,-244.527 308.664,-241.018 298.66,-237.527 298.667,-244.527\"/>\n",
+ "<text text-anchor=\"middle\" x=\"276.898\" y=\"-227.846\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge38\" class=\"edge\"><title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M255.152,-238.364C305.333,-233.34 412.433,-222.618 469.358,-216.919\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"469.777,-220.395 479.378,-215.916 469.079,-213.429 469.777,-220.395\"/>\n",
+ "<text text-anchor=\"middle\" x=\"362.255\" y=\"-214.441\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node31\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-247.411 0,-247.411 0,-211.411 54,-211.411 54,-247.411\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-225.211\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge40\" class=\"edge\"><title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M54.0956,-230.986C89.2951,-233.032 150.917,-236.615 190.541,-238.918\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"190.415,-242.417 200.602,-239.503 190.822,-235.429 190.415,-242.417\"/>\n",
+ "<text text-anchor=\"middle\" x=\"122.318\" y=\"-239.752\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [g]>"
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph g"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,12,3,13)"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,13,3,14)"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,14,3,15)"
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,15,3,16)"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,16,3,17)"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,17,3,18)"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,18,3,19)"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,19,3,20)"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,20,3,21)"
+ ]
+ },
+ "execution_count": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,21,3,22)"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,22,3,23)"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,23,3,24)"
+ ]
+ },
+ "execution_count": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: Rewrite(2,24,3,25)"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Rewrite"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?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",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"824pt\" height=\"518pt\"\n",
+ " viewBox=\"0.00 0.00 823.51 517.73\" 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 513.729)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-513.729 820.508,-513.729 820.508,5 -4,5\"/>\n",
+ "<!-- 24 -->\n",
+ "<g id=\"node1\" class=\"node\"><title>24</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"398.261,-192.608 344.261,-192.608 344.261,-156.608 398.261,-156.608 398.261,-192.608\"/>\n",
+ "<text text-anchor=\"middle\" x=\"371.261\" y=\"-170.408\" font-family=\"Times,serif\" font-size=\"14.00\">24</text>\n",
+ "</g>\n",
+ "<!-- 25 -->\n",
+ "<g id=\"node3\" class=\"node\"><title>25</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"353.554,-255.293 299.554,-255.293 299.554,-219.293 353.554,-219.293 353.554,-255.293\"/>\n",
+ "<text text-anchor=\"middle\" x=\"326.554\" y=\"-233.093\" font-family=\"Times,serif\" font-size=\"14.00\">25</text>\n",
+ "</g>\n",
+ "<!-- 24->25 -->\n",
+ "<g id=\"edge2\" class=\"edge\"><title>24->25</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M358.33,-192.739C354.379,-198.278 349.948,-204.491 345.678,-210.479\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"342.568,-208.812 339.611,-218.985 348.267,-212.876 342.568,-208.812\"/>\n",
+ "<text text-anchor=\"middle\" x=\"345.004\" y=\"-192.409\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 23 -->\n",
+ "<g id=\"node4\" class=\"node\"><title>23</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"404.272,-119.12 350.272,-119.12 350.272,-83.1199 404.272,-83.1199 404.272,-119.12\"/>\n",
+ "<text text-anchor=\"middle\" x=\"377.272\" y=\"-96.9199\" font-family=\"Times,serif\" font-size=\"14.00\">23</text>\n",
+ "</g>\n",
+ "<!-- 23->24 -->\n",
+ "<g id=\"edge4\" class=\"edge\"><title>23->24</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M375.786,-119.285C375.121,-127.412 374.322,-137.183 373.581,-146.238\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"370.077,-146.144 372.75,-156.396 377.054,-146.715 370.077,-146.144\"/>\n",
+ "<text text-anchor=\"middle\" x=\"369.684\" y=\"-128.562\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 22 -->\n",
+ "<g id=\"node6\" class=\"node\"><title>22</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"457.36,-68.2059 403.36,-68.2059 403.36,-32.2059 457.36,-32.2059 457.36,-68.2059\"/>\n",
+ "<text text-anchor=\"middle\" x=\"430.36\" y=\"-46.0059\" font-family=\"Times,serif\" font-size=\"14.00\">22</text>\n",
+ "</g>\n",
+ "<!-- 22->23 -->\n",
+ "<g id=\"edge6\" class=\"edge\"><title>22->23</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M411.494,-68.2997C408.834,-70.8506 406.061,-73.5095 403.296,-76.1612\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"400.872,-73.6366 396.077,-83.0845 405.717,-78.6887 400.872,-73.6366\"/>\n",
+ "<text text-anchor=\"middle\" x=\"413.395\" y=\"-75.0304\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 21 -->\n",
+ "<g id=\"node8\" class=\"node\"><title>21</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"526.37,-93.9983 472.37,-93.9983 472.37,-57.9983 526.37,-57.9983 526.37,-93.9983\"/>\n",
+ "<text text-anchor=\"middle\" x=\"499.37\" y=\"-71.7983\" font-family=\"Times,serif\" font-size=\"14.00\">21</text>\n",
+ "</g>\n",
+ "<!-- 21->22 -->\n",
+ "<g id=\"edge8\" class=\"edge\"><title>21->22</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M472.095,-65.8044C470.438,-65.1849 468.757,-64.5566 467.069,-63.9257\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"468.029,-60.5482 457.436,-60.3257 465.578,-67.1052 468.029,-60.5482\"/>\n",
+ "<text text-anchor=\"middle\" x=\"468.582\" y=\"-69.6651\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 20 -->\n",
+ "<g id=\"node10\" class=\"node\"><title>20</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"570.082,-36 516.082,-36 516.082,-0 570.082,-0 570.082,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"543.082\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">20</text>\n",
+ "</g>\n",
+ "<!-- 20->21 -->\n",
+ "<g id=\"edge10\" class=\"edge\"><title>20->21</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M529.491,-36.0331C526.233,-40.356 522.688,-45.0601 519.211,-49.6733\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"516.327,-47.6841 513.103,-57.7766 521.917,-51.8973 516.327,-47.6841\"/>\n",
+ "<text text-anchor=\"middle\" x=\"517.351\" y=\"-33.6532\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 19 -->\n",
+ "<g id=\"node12\" class=\"node\"><title>19</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"638.022,-57.8219 584.022,-57.8219 584.022,-21.8219 638.022,-21.8219 638.022,-57.8219\"/>\n",
+ "<text text-anchor=\"middle\" x=\"611.022\" y=\"-35.6219\" font-family=\"Times,serif\" font-size=\"14.00\">19</text>\n",
+ "</g>\n",
+ "<!-- 19->20 -->\n",
+ "<g id=\"edge12\" class=\"edge\"><title>19->20</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M583.78,-31.0719C582.534,-30.6717 581.275,-30.2674 580.011,-29.8614\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"580.922,-26.4779 570.331,-26.752 578.781,-33.1425 580.922,-26.4779\"/>\n",
+ "<text text-anchor=\"middle\" x=\"584.896\" y=\"-17.2666\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 18 -->\n",
+ "<g id=\"node14\" class=\"node\"><title>18</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"705.908,-78.8593 651.908,-78.8593 651.908,-42.8593 705.908,-42.8593 705.908,-78.8593\"/>\n",
+ "<text text-anchor=\"middle\" x=\"678.908\" y=\"-56.6593\" font-family=\"Times,serif\" font-size=\"14.00\">18</text>\n",
+ "</g>\n",
+ "<!-- 18->19 -->\n",
+ "<g id=\"edge14\" class=\"edge\"><title>18->19</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M651.688,-52.4238C650.443,-52.038 649.185,-51.6483 647.922,-51.2569\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"648.837,-47.8763 638.249,-48.2593 646.765,-54.5626 648.837,-47.8763\"/>\n",
+ "<text text-anchor=\"middle\" x=\"646.805\" y=\"-56.6404\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 17 -->\n",
+ "<g id=\"node16\" class=\"node\"><title>17</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"763.472,-127.922 709.472,-127.922 709.472,-91.9222 763.472,-91.9222 763.472,-127.922\"/>\n",
+ "<text text-anchor=\"middle\" x=\"736.472\" y=\"-105.722\" font-family=\"Times,serif\" font-size=\"14.00\">17</text>\n",
+ "</g>\n",
+ "<!-- 17->18 -->\n",
+ "<g id=\"edge16\" class=\"edge\"><title>17->18</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M715.037,-91.653C712.76,-89.7118 710.417,-87.7145 708.07,-85.7144\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"710.05,-82.8035 700.169,-78.9804 705.509,-88.1309 710.05,-82.8035\"/>\n",
+ "<text text-anchor=\"middle\" x=\"717.554\" y=\"-77.4837\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 16 -->\n",
+ "<g id=\"node18\" class=\"node\"><title>16</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"715.62,-185.102 661.62,-185.102 661.62,-149.102 715.62,-149.102 715.62,-185.102\"/>\n",
+ "<text text-anchor=\"middle\" x=\"688.62\" y=\"-162.902\" font-family=\"Times,serif\" font-size=\"14.00\">16</text>\n",
+ "</g>\n",
+ "<!-- 16->17 -->\n",
+ "<g id=\"edge18\" class=\"edge\"><title>16->17</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M703.761,-149.01C707.252,-144.839 711.033,-140.321 714.743,-135.888\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"717.532,-138.008 721.266,-128.093 712.164,-133.516 717.532,-138.008\"/>\n",
+ "<text text-anchor=\"middle\" x=\"716.252\" y=\"-143.249\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 15 -->\n",
+ "<g id=\"node20\" class=\"node\"><title>15</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"763.408,-238.802 709.408,-238.802 709.408,-202.802 763.408,-202.802 763.408,-238.802\"/>\n",
+ "<text text-anchor=\"middle\" x=\"736.408\" y=\"-216.602\" font-family=\"Times,serif\" font-size=\"14.00\">15</text>\n",
+ "</g>\n",
+ "<!-- 15->16 -->\n",
+ "<g id=\"edge20\" class=\"edge\"><title>15->16</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M720.229,-202.621C717.427,-199.472 714.465,-196.145 711.524,-192.84\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"714.045,-190.407 704.782,-185.264 708.816,-195.061 714.045,-190.407\"/>\n",
+ "<text text-anchor=\"middle\" x=\"722.877\" y=\"-187.531\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 14 -->\n",
+ "<g id=\"node22\" class=\"node\"><title>14</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"815.508,-281.744 761.508,-281.744 761.508,-245.744 815.508,-245.744 815.508,-281.744\"/>\n",
+ "<text text-anchor=\"middle\" x=\"788.508\" y=\"-259.544\" font-family=\"Times,serif\" font-size=\"14.00\">14</text>\n",
+ "</g>\n",
+ "<!-- 14->15 -->\n",
+ "<g id=\"edge22\" class=\"edge\"><title>14->15</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M766.413,-245.533C766.329,-245.464 766.246,-245.395 766.163,-245.327\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"768.313,-242.564 758.371,-238.904 763.861,-247.965 768.313,-242.564\"/>\n",
+ "<text text-anchor=\"middle\" x=\"766.288\" y=\"-232.23\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 13 -->\n",
+ "<g id=\"node24\" class=\"node\"><title>13</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"791.584,-350.733 737.584,-350.733 737.584,-314.733 791.584,-314.733 791.584,-350.733\"/>\n",
+ "<text text-anchor=\"middle\" x=\"764.584\" y=\"-328.533\" font-family=\"Times,serif\" font-size=\"14.00\">13</text>\n",
+ "</g>\n",
+ "<!-- 13->14 -->\n",
+ "<g id=\"edge24\" class=\"edge\"><title>13->14</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M770.87,-314.607C773.323,-307.534 776.19,-299.264 778.892,-291.474\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"782.211,-292.584 782.181,-281.989 775.598,-290.29 782.211,-292.584\"/>\n",
+ "<text text-anchor=\"middle\" x=\"780.881\" y=\"-300.841\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 12 -->\n",
+ "<g id=\"node26\" class=\"node\"><title>12</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"739.499,-395.735 685.499,-395.735 685.499,-359.735 739.499,-359.735 739.499,-395.735\"/>\n",
+ "<text text-anchor=\"middle\" x=\"712.499\" y=\"-373.535\" font-family=\"Times,serif\" font-size=\"14.00\">12</text>\n",
+ "</g>\n",
+ "<!-- 12->13 -->\n",
+ "<g id=\"edge26\" class=\"edge\"><title>12->13</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M733.384,-359.69C734.233,-358.957 735.09,-358.217 735.95,-357.473\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"738.416,-359.968 743.695,-350.782 733.84,-354.671 738.416,-359.968\"/>\n",
+ "<text text-anchor=\"middle\" x=\"740.667\" y=\"-360.382\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 11 -->\n",
+ "<g id=\"node28\" class=\"node\"><title>11</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"714.213,-460.436 660.213,-460.436 660.213,-424.436 714.213,-424.436 714.213,-460.436\"/>\n",
+ "<text text-anchor=\"middle\" x=\"687.213\" y=\"-438.236\" font-family=\"Times,serif\" font-size=\"14.00\">11</text>\n",
+ "</g>\n",
+ "<!-- 11->12 -->\n",
+ "<g id=\"edge28\" class=\"edge\"><title>11->12</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M694.257,-424.413C696.52,-418.622 699.083,-412.063 701.558,-405.731\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"704.938,-406.698 705.318,-396.11 698.418,-404.15 704.938,-406.698\"/>\n",
+ "<text text-anchor=\"middle\" x=\"704.907\" y=\"-412.872\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 10 -->\n",
+ "<g id=\"node30\" class=\"node\"><title>10</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"651.439,-499.97 597.439,-499.97 597.439,-463.97 651.439,-463.97 651.439,-499.97\"/>\n",
+ "<text text-anchor=\"middle\" x=\"624.439\" y=\"-477.77\" font-family=\"Times,serif\" font-size=\"14.00\">10</text>\n",
+ "</g>\n",
+ "<!-- 10->11 -->\n",
+ "<g id=\"edge30\" class=\"edge\"><title>10->11</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M651.79,-464.745C651.877,-464.69 651.964,-464.635 652.05,-464.581\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"653.559,-467.767 660.156,-459.476 649.829,-461.843 653.559,-467.767\"/>\n",
+ "<text text-anchor=\"middle\" x=\"651.92\" y=\"-451.463\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 9 -->\n",
+ "<g id=\"node32\" class=\"node\"><title>9</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"593.048,-458.922 539.048,-458.922 539.048,-422.922 593.048,-422.922 593.048,-458.922\"/>\n",
+ "<text text-anchor=\"middle\" x=\"566.048\" y=\"-436.722\" font-family=\"Times,serif\" font-size=\"14.00\">9</text>\n",
+ "</g>\n",
+ "<!-- 9->10 -->\n",
+ "<g id=\"edge32\" class=\"edge\"><title>9->10</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M591.829,-459.045C591.974,-459.147 592.119,-459.249 592.265,-459.352\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"588.629,-461.074 598.822,-463.962 592.654,-455.347 588.629,-461.074\"/>\n",
+ "<text text-anchor=\"middle\" x=\"592.047\" y=\"-445.998\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 8 -->\n",
+ "<g id=\"node34\" class=\"node\"><title>8</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"527.715,-407.071 473.715,-407.071 473.715,-371.071 527.715,-371.071 527.715,-407.071\"/>\n",
+ "<text text-anchor=\"middle\" x=\"500.715\" y=\"-384.871\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+ "</g>\n",
+ "<!-- 8->9 -->\n",
+ "<g id=\"edge34\" class=\"edge\"><title>8->9</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M523.565,-407.206C527.323,-410.188 531.272,-413.322 535.186,-416.429\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"533.091,-419.234 543.1,-422.709 537.443,-413.751 533.091,-419.234\"/>\n",
+ "<text text-anchor=\"middle\" x=\"523.376\" y=\"-414.617\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 7 -->\n",
+ "<g id=\"node36\" class=\"node\"><title>7</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"446.691,-359.113 392.691,-359.113 392.691,-323.113 446.691,-323.113 446.691,-359.113\"/>\n",
+ "<text text-anchor=\"middle\" x=\"419.691\" y=\"-336.913\" font-family=\"Times,serif\" font-size=\"14.00\">7</text>\n",
+ "</g>\n",
+ "<!-- 7->8 -->\n",
+ "<g id=\"edge36\" class=\"edge\"><title>7->8</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M447.122,-357.35C452.859,-360.745 458.989,-364.373 464.977,-367.918\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"463.199,-370.932 473.587,-373.014 466.765,-364.909 463.199,-370.932\"/>\n",
+ "<text text-anchor=\"middle\" x=\"451.05\" y=\"-366.434\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 6 -->\n",
+ "<g id=\"node38\" class=\"node\"><title>6</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"380.305,-396.758 326.305,-396.758 326.305,-360.758 380.305,-360.758 380.305,-396.758\"/>\n",
+ "<text text-anchor=\"middle\" x=\"353.305\" y=\"-374.558\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+ "</g>\n",
+ "<!-- 6->7 -->\n",
+ "<g id=\"edge38\" class=\"edge\"><title>6->7</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M380.307,-363.446C381.437,-362.805 382.578,-362.158 383.723,-361.509\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"385.525,-364.511 392.498,-356.533 382.072,-358.422 385.525,-364.511\"/>\n",
+ "<text text-anchor=\"middle\" x=\"379.015\" y=\"-349.278\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 5 -->\n",
+ "<g id=\"node40\" class=\"node\"><title>5</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"426.794,-465.926 372.794,-465.926 372.794,-429.926 426.794,-429.926 426.794,-465.926\"/>\n",
+ "<text text-anchor=\"middle\" x=\"399.794\" y=\"-443.726\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+ "</g>\n",
+ "<!-- 5->6 -->\n",
+ "<g id=\"edge40\" class=\"edge\"><title>5->6</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M387.58,-429.753C382.601,-422.345 376.743,-413.631 371.293,-405.521\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"374.082,-403.397 365.599,-397.05 368.273,-407.302 374.082,-403.397\"/>\n",
+ "<text text-anchor=\"middle\" x=\"372.436\" y=\"-417.437\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node42\" class=\"node\"><title>4</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"496.257,-509.729 442.257,-509.729 442.257,-473.729 496.257,-473.729 496.257,-509.729\"/>\n",
+ "<text text-anchor=\"middle\" x=\"469.257\" y=\"-487.529\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+ "</g>\n",
+ "<!-- 4->5 -->\n",
+ "<g id=\"edge42\" class=\"edge\"><title>4->5</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M442.202,-474.668C440.002,-473.281 437.759,-471.866 435.51,-470.448\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"437.215,-467.386 426.889,-465.012 433.481,-473.307 437.215,-467.386\"/>\n",
+ "<text text-anchor=\"middle\" x=\"433.856\" y=\"-476.358\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node44\" class=\"node\"><title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"569.862,-272.718 515.862,-272.718 515.862,-236.718 569.862,-236.718 569.862,-272.718\"/>\n",
+ "<text text-anchor=\"middle\" x=\"542.862\" y=\"-250.518\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+ "</g>\n",
+ "<!-- 3->24 -->\n",
+ "<g id=\"edge46\" class=\"edge\"><title>3->24</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M515.672,-242.024C486.426,-228.371 439.78,-206.595 407.45,-191.502\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"408.866,-188.301 398.324,-187.242 405.905,-194.644 408.866,-188.301\"/>\n",
+ "<text text-anchor=\"middle\" x=\"457.561\" y=\"-221.563\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->25 -->\n",
+ "<g id=\"edge44\" class=\"edge\"><title>3->25</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M515.467,-252.511C477.028,-249.415 406.97,-243.771 363.819,-240.295\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"363.976,-236.796 353.727,-239.482 363.414,-243.774 363.976,-236.796\"/>\n",
+ "<text text-anchor=\"middle\" x=\"439.643\" y=\"-233.203\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->23 -->\n",
+ "<g id=\"edge48\" class=\"edge\"><title>3->23</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M523.217,-236.495C493.713,-209.128 437.868,-157.328 404.467,-126.346\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"406.604,-123.554 396.892,-119.319 401.843,-128.686 406.604,-123.554\"/>\n",
+ "<text text-anchor=\"middle\" x=\"469.842\" y=\"-170.22\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->22 -->\n",
+ "<g id=\"edge50\" class=\"edge\"><title>3->22</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M532.878,-236.569C513.03,-200.488 468.524,-119.582 445.224,-77.2268\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"448.208,-75.3892 440.321,-68.3143 442.075,-78.7631 448.208,-75.3892\"/>\n",
+ "<text text-anchor=\"middle\" x=\"496.051\" y=\"-148.698\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->21 -->\n",
+ "<g id=\"edge52\" class=\"edge\"><title>3->21</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M538.453,-236.598C530.866,-205.421 515.289,-141.414 506.26,-104.31\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"509.557,-103.055 503.791,-94.1663 502.755,-104.71 509.557,-103.055\"/>\n",
+ "<text text-anchor=\"middle\" x=\"528.356\" y=\"-165.254\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->20 -->\n",
+ "<g id=\"edge54\" class=\"edge\"><title>3->20</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M542.879,-236.536C542.917,-195.571 543.01,-95.7984 543.056,-46.5126\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"546.556,-46.247 543.065,-36.2437 539.556,-46.2405 546.556,-46.247\"/>\n",
+ "<text text-anchor=\"middle\" x=\"538.968\" y=\"-137.324\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->19 -->\n",
+ "<g id=\"edge56\" class=\"edge\"><title>3->19</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M548.674,-236.396C560.62,-198.73 588.002,-112.399 602.169,-67.7339\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"605.538,-68.6877 605.225,-58.0975 598.866,-66.5713 605.538,-68.6877\"/>\n",
+ "<text text-anchor=\"middle\" x=\"581.421\" y=\"-149.865\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->18 -->\n",
+ "<g id=\"edge58\" class=\"edge\"><title>3->18</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M555.661,-236.48C579.88,-201.97 632.486,-127.008 660.495,-87.0969\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"663.363,-89.1034 666.243,-78.9074 657.633,-85.0823 663.363,-89.1034\"/>\n",
+ "<text text-anchor=\"middle\" x=\"601.078\" y=\"-152.589\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->17 -->\n",
+ "<g id=\"edge60\" class=\"edge\"><title>3->17</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M566.992,-236.672C601.578,-210.806 665.331,-163.126 704.019,-134.193\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"706.431,-136.759 712.343,-127.967 702.239,-131.154 706.431,-136.759\"/>\n",
+ "<text text-anchor=\"middle\" x=\"629.505\" y=\"-173.233\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->16 -->\n",
+ "<g id=\"edge62\" class=\"edge\"><title>3->16</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M569.937,-238.443C593.209,-224.455 626.96,-204.167 652.525,-188.799\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"654.429,-191.739 661.196,-183.587 650.822,-185.739 654.429,-191.739\"/>\n",
+ "<text text-anchor=\"middle\" x=\"616.231\" y=\"-217.421\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->15 -->\n",
+ "<g id=\"edge64\" class=\"edge\"><title>3->15</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M570.182,-249.93C603.899,-244.022 661.391,-233.947 699.14,-227.332\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"699.981,-230.738 709.227,-225.565 698.773,-223.843 699.981,-230.738\"/>\n",
+ "<text text-anchor=\"middle\" x=\"633.661\" y=\"-225.431\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->14 -->\n",
+ "<g id=\"edge66\" class=\"edge\"><title>3->14</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M570.089,-255.718C614.172,-257.338 701.251,-260.538 751.113,-262.37\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"751.037,-265.87 761.159,-262.739 751.294,-258.874 751.037,-265.87\"/>\n",
+ "<text text-anchor=\"middle\" x=\"660.601\" y=\"-263.844\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->13 -->\n",
+ "<g id=\"edge68\" class=\"edge\"><title>3->13</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M570.05,-264.284C609.72,-278.242 683.564,-304.225 727.977,-319.853\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"726.927,-323.193 737.522,-323.211 729.25,-316.59 726.927,-323.193\"/>\n",
+ "<text text-anchor=\"middle\" x=\"646.013\" y=\"-296.868\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->12 -->\n",
+ "<g id=\"edge70\" class=\"edge\"><title>3->12</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M567.893,-272.869C597.419,-294.281 646.613,-329.955 679.301,-353.66\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"677.492,-356.672 687.643,-359.709 681.602,-351.005 677.492,-356.672\"/>\n",
+ "<text text-anchor=\"middle\" x=\"628.597\" y=\"-301.065\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->11 -->\n",
+ "<g id=\"edge72\" class=\"edge\"><title>3->11</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M556.966,-273.059C582.688,-306.509 637.297,-377.524 666.981,-416.125\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"664.394,-418.503 673.265,-424.297 669.943,-414.236 664.394,-418.503\"/>\n",
+ "<text text-anchor=\"middle\" x=\"604.973\" y=\"-345.392\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->10 -->\n",
+ "<g id=\"edge74\" class=\"edge\"><title>3->10</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M549.4,-272.931C563.631,-312.573 597.49,-406.897 614.429,-454.084\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"611.197,-455.441 617.87,-463.67 617.786,-453.076 611.197,-455.441\"/>\n",
+ "<text text-anchor=\"middle\" x=\"575.915\" y=\"-361.308\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->9 -->\n",
+ "<g id=\"edge76\" class=\"edge\"><title>3->9</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M545.128,-272.911C549.179,-305.45 557.693,-373.824 562.517,-412.567\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"559.064,-413.164 563.773,-422.655 566.011,-412.299 559.064,-413.164\"/>\n",
+ "<text text-anchor=\"middle\" x=\"558.822\" y=\"-338.539\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->8 -->\n",
+ "<g id=\"edge78\" class=\"edge\"><title>3->8</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M537.178,-272.837C530.077,-295.475 517.849,-334.454 509.529,-360.974\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"506.098,-360.22 506.444,-370.809 512.777,-362.316 506.098,-360.22\"/>\n",
+ "<text text-anchor=\"middle\" x=\"529.354\" y=\"-314.706\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->7 -->\n",
+ "<g id=\"edge80\" class=\"edge\"><title>3->7</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M517.042,-272.829C498.648,-285.731 473.74,-303.202 453.723,-317.242\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"451.655,-314.418 445.478,-323.026 455.674,-320.149 451.655,-314.418\"/>\n",
+ "<text text-anchor=\"middle\" x=\"490.383\" y=\"-298.836\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->6 -->\n",
+ "<g id=\"edge82\" class=\"edge\"><title>3->6</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M515.703,-272.49C482.343,-294.32 425.661,-331.411 388.859,-355.493\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"386.864,-352.615 380.413,-361.019 390.697,-358.472 386.864,-352.615\"/>\n",
+ "<text text-anchor=\"middle\" x=\"447.281\" y=\"-301.791\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->5 -->\n",
+ "<g id=\"edge84\" class=\"edge\"><title>3->5</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M529.403,-272.894C503.999,-307.201 448.894,-381.619 419.383,-421.472\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"416.46,-419.537 413.322,-429.657 422.086,-423.703 416.46,-419.537\"/>\n",
+ "<text text-anchor=\"middle\" x=\"481.393\" y=\"-347.983\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 3->4 -->\n",
+ "<g id=\"edge86\" class=\"edge\"><title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M537.209,-272.922C524.418,-314.11 493.186,-414.675 477.93,-463.8\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"474.553,-462.874 474.929,-473.463 481.238,-464.951 474.553,-462.874\"/>\n",
+ "<text text-anchor=\"middle\" x=\"501.569\" y=\"-362.161\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node67\" class=\"node\"><title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"263.2,-264.863 209.2,-264.863 209.2,-228.863 263.2,-228.863 263.2,-264.863\"/>\n",
+ "<text text-anchor=\"middle\" x=\"236.2\" y=\"-242.663\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+ "</g>\n",
+ "<!-- 2->25 -->\n",
+ "<g id=\"edge88\" class=\"edge\"><title>2->25</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M263.309,-243.992C271.528,-243.121 280.703,-242.149 289.459,-241.222\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"289.888,-244.696 299.464,-240.162 289.151,-237.735 289.888,-244.696\"/>\n",
+ "<text text-anchor=\"middle\" x=\"276.384\" y=\"-247.407\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge90\" class=\"edge\"><title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M263.414,-247.56C318.426,-248.969 442.931,-252.158 505.498,-253.761\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"505.623,-257.265 515.709,-254.022 505.802,-250.267 505.623,-257.265\"/>\n",
+ "<text text-anchor=\"middle\" x=\"384.456\" y=\"-237.461\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node70\" class=\"node\"><title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-260.132 0,-260.132 0,-224.132 54,-224.132 54,-260.132\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-237.932\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge92\" class=\"edge\"><title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"firebrick\" d=\"M54.3492,-242.751C91.3335,-243.587 157.43,-245.082 198.932,-246.02\"/>\n",
+ "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"199.099,-249.525 209.175,-246.252 199.257,-242.527 199.099,-249.525\"/>\n",
+ "<text text-anchor=\"middle\" x=\"126.64\" y=\"-249.186\" font-family=\"Times,serif\" font-size=\"14.00\">g</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [g]>"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph g"
+ ]
+ },
+ {
+ "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
+}
--
GitLab