counter-example.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "dccc231a",
   "metadata": {},
   "outputs": [],
   "source": [
    "from graphviz import Digraph\n",
    "from matplotlib import pyplot as plt\n",
    "from collections import defaultdict"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "3c4cf4b5",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((0, 8, 5), [(0, 9, 5), (0, 8, 6)])\n"
     ]
    },
    {
     "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.43.0 (0)\n",
       " -->\n",
       "<!-- Title: %3 Pages: 1 -->\n",
       "<svg width=\"446pt\" height=\"332pt\"\n",
       " viewBox=\"0.00 0.00 446.14 332.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 328)\">\n",
       "<title>%3</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-328 442.14,-328 442.14,4 -4,4\"/>\n",
       "<!-- 0, 8, 5 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>0, 8, 5</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"232.35\" cy=\"-306\" rx=\"33.6\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"232.35\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 8, 5</text>\n",
       "</g>\n",
       "<!-- 0, 9, 5 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0, 9, 5</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"189.35\" cy=\"-234\" rx=\"33.6\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"189.35\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 9, 5</text>\n",
       "</g>\n",
       "<!-- 0, 8, 5&#45;&gt;0, 9, 5 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>0, 8, 5&#45;&gt;0, 9, 5</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M222.37,-288.76C217.18,-280.32 210.72,-269.8 204.9,-260.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"207.78,-258.32 199.56,-251.63 201.82,-261.99 207.78,-258.32\"/>\n",
       "</g>\n",
       "<!-- 0, 8, 6 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>0, 8, 6</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"275.35\" cy=\"-234\" rx=\"33.6\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"275.35\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 8, 6</text>\n",
       "</g>\n",
       "<!-- 0, 8, 5&#45;&gt;0, 8, 6 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0, 8, 5&#45;&gt;0, 8, 6</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M242.32,-288.76C247.51,-280.32 253.97,-269.8 259.8,-260.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"262.88,-261.99 265.13,-251.63 256.91,-258.32 262.88,-261.99\"/>\n",
       "</g>\n",
       "<!-- 0, 10, 5 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>0, 10, 5</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"142.35\" cy=\"-162\" rx=\"38.19\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"142.35\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 10, 5</text>\n",
       "</g>\n",
       "<!-- 0, 9, 5&#45;&gt;0, 10, 5 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0, 9, 5&#45;&gt;0, 10, 5</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M178.45,-216.76C172.72,-208.23 165.57,-197.58 159.15,-188.02\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"161.99,-185.98 153.51,-179.63 156.18,-189.89 161.99,-185.98\"/>\n",
       "</g>\n",
       "<!-- 0, 9, 6 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>0, 9, 6</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"232.35\" cy=\"-162\" rx=\"33.6\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"232.35\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 9, 6</text>\n",
       "</g>\n",
       "<!-- 0, 9, 5&#45;&gt;0, 9, 6 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>0, 9, 5&#45;&gt;0, 9, 6</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M199.32,-216.76C204.51,-208.32 210.97,-197.8 216.8,-188.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"219.88,-189.99 222.13,-179.63 213.91,-186.32 219.88,-189.99\"/>\n",
       "</g>\n",
       "<!-- 0, 8, 6&#45;&gt;0, 9, 6 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>0, 8, 6&#45;&gt;0, 9, 6</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M265.37,-216.76C260.18,-208.32 253.72,-197.8 247.9,-188.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"250.78,-186.32 242.56,-179.63 244.82,-189.99 250.78,-186.32\"/>\n",
       "</g>\n",
       "<!-- 0, 8, 7 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>0, 8, 7</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"318.35\" cy=\"-162\" rx=\"33.6\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"318.35\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 8, 7</text>\n",
       "</g>\n",
       "<!-- 0, 8, 6&#45;&gt;0, 8, 7 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>0, 8, 6&#45;&gt;0, 8, 7</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M285.32,-216.76C290.51,-208.32 296.97,-197.8 302.8,-188.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"305.88,-189.99 308.13,-179.63 299.91,-186.32 305.88,-189.99\"/>\n",
       "</g>\n",
       "<!-- 0, 11, 5 -->\n",
       "<g id=\"node7\" class=\"node\">\n",
       "<title>0, 11, 5</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"90.35\" cy=\"-90\" rx=\"38.19\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"90.35\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 11, 5</text>\n",
       "</g>\n",
       "<!-- 0, 10, 5&#45;&gt;0, 11, 5 -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>0, 10, 5&#45;&gt;0, 11, 5</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M130.29,-144.76C123.79,-136.02 115.64,-125.05 108.4,-115.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"111.11,-113.09 102.34,-107.15 105.5,-117.26 111.11,-113.09\"/>\n",
       "</g>\n",
       "<!-- 0, 10, 6 -->\n",
       "<g id=\"node8\" class=\"node\">\n",
       "<title>0, 10, 6</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"185.35\" cy=\"-90\" rx=\"38.19\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"185.35\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 10, 6</text>\n",
       "</g>\n",
       "<!-- 0, 10, 5&#45;&gt;0, 10, 6 -->\n",
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>0, 10, 5&#45;&gt;0, 10, 6</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M152.54,-144.41C157.73,-135.95 164.16,-125.49 169.94,-116.08\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"172.98,-117.82 175.23,-107.47 167.01,-114.16 172.98,-117.82\"/>\n",
       "</g>\n",
       "<!-- 0, 9, 6&#45;&gt;0, 10, 6 -->\n",
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>0, 9, 6&#45;&gt;0, 10, 6</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M221.45,-144.76C215.72,-136.23 208.57,-125.58 202.15,-116.02\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"204.99,-113.98 196.51,-107.63 199.18,-117.89 204.99,-113.98\"/>\n",
       "</g>\n",
       "<!-- 0, 9, 7 -->\n",
       "<g id=\"node9\" class=\"node\">\n",
       "<title>0, 9, 7</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"275.35\" cy=\"-90\" rx=\"33.6\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"275.35\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 9, 7</text>\n",
       "</g>\n",
       "<!-- 0, 9, 6&#45;&gt;0, 9, 7 -->\n",
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>0, 9, 6&#45;&gt;0, 9, 7</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M242.32,-144.76C247.51,-136.32 253.97,-125.8 259.8,-116.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"262.88,-117.99 265.13,-107.63 256.91,-114.32 262.88,-117.99\"/>\n",
       "</g>\n",
       "<!-- 0, 8, 7&#45;&gt;0, 9, 7 -->\n",
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>0, 8, 7&#45;&gt;0, 9, 7</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M308.37,-144.76C303.18,-136.32 296.72,-125.8 290.9,-116.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"293.78,-114.32 285.56,-107.63 287.82,-117.99 293.78,-114.32\"/>\n",
       "</g>\n",
       "<!-- 0, 8, 8 -->\n",
       "<g id=\"node10\" class=\"node\">\n",
       "<title>0, 8, 8</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"361.35\" cy=\"-90\" rx=\"33.6\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"361.35\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 8, 8</text>\n",
       "</g>\n",
       "<!-- 0, 8, 7&#45;&gt;0, 8, 8 -->\n",
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>0, 8, 7&#45;&gt;0, 8, 8</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M328.32,-144.76C333.51,-136.32 339.97,-125.8 345.8,-116.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"348.88,-117.99 351.13,-107.63 342.91,-114.32 348.88,-117.99\"/>\n",
       "</g>\n",
       "<!-- 0, 12, 5 -->\n",
       "<g id=\"node11\" class=\"node\">\n",
       "<title>0, 12, 5</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" cx=\"38.35\" cy=\"-18\" rx=\"38.19\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"38.35\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 12, 5</text>\n",
       "</g>\n",
       "<!-- 0, 11, 5&#45;&gt;0, 12, 5 -->\n",
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>0, 11, 5&#45;&gt;0, 12, 5</title>\n",
       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M78.29,-72.76C71.79,-64.02 63.64,-53.05 56.4,-43.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"59.11,-41.09 50.34,-35.15 53.5,-45.26 59.11,-41.09\"/>\n",
       "</g>\n",
       "<!-- 0, 11, 6 -->\n",
       "<g id=\"node12\" class=\"node\">\n",
       "<title>0, 11, 6</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" cx=\"133.35\" cy=\"-18\" rx=\"38.19\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"133.35\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 11, 6</text>\n",
       "</g>\n",
       "<!-- 0, 11, 5&#45;&gt;0, 11, 6 -->\n",
       "<g id=\"edge14\" class=\"edge\">\n",
       "<title>0, 11, 5&#45;&gt;0, 11, 6</title>\n",
       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M100.54,-72.41C105.73,-63.95 112.16,-53.49 117.94,-44.08\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"120.98,-45.82 123.23,-35.47 115.01,-42.16 120.98,-45.82\"/>\n",
       "</g>\n",
       "<!-- 0, 10, 6&#45;&gt;0, 11, 6 -->\n",
       "<g id=\"edge15\" class=\"edge\">\n",
       "<title>0, 10, 6&#45;&gt;0, 11, 6</title>\n",
       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M173.29,-72.76C166.79,-64.02 158.64,-53.05 151.4,-43.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"154.11,-41.09 145.34,-35.15 148.5,-45.26 154.11,-41.09\"/>\n",
       "</g>\n",
       "<!-- 0, 10, 7 -->\n",
       "<g id=\"node13\" class=\"node\">\n",
       "<title>0, 10, 7</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" cx=\"228.35\" cy=\"-18\" rx=\"38.19\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"228.35\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 10, 7</text>\n",
       "</g>\n",
       "<!-- 0, 10, 6&#45;&gt;0, 10, 7 -->\n",
       "<g id=\"edge16\" class=\"edge\">\n",
       "<title>0, 10, 6&#45;&gt;0, 10, 7</title>\n",
       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M195.54,-72.41C200.73,-63.95 207.16,-53.49 212.94,-44.08\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"215.98,-45.82 218.23,-35.47 210.01,-42.16 215.98,-45.82\"/>\n",
       "</g>\n",
       "<!-- 0, 9, 7&#45;&gt;0, 10, 7 -->\n",
       "<g id=\"edge17\" class=\"edge\">\n",
       "<title>0, 9, 7&#45;&gt;0, 10, 7</title>\n",
       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M264.45,-72.76C258.72,-64.23 251.57,-53.58 245.15,-44.02\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"247.99,-41.98 239.51,-35.63 242.18,-45.89 247.99,-41.98\"/>\n",
       "</g>\n",
       "<!-- 0, 9, 8 -->\n",
       "<g id=\"node14\" class=\"node\">\n",
       "<title>0, 9, 8</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" cx=\"318.35\" cy=\"-18\" rx=\"33.6\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"318.35\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 9, 8</text>\n",
       "</g>\n",
       "<!-- 0, 9, 7&#45;&gt;0, 9, 8 -->\n",
       "<g id=\"edge18\" class=\"edge\">\n",
       "<title>0, 9, 7&#45;&gt;0, 9, 8</title>\n",
       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M285.32,-72.76C290.51,-64.32 296.97,-53.8 302.8,-44.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"305.88,-45.99 308.13,-35.63 299.91,-42.32 305.88,-45.99\"/>\n",
       "</g>\n",
       "<!-- 0, 8, 8&#45;&gt;0, 9, 8 -->\n",
       "<g id=\"edge19\" class=\"edge\">\n",
       "<title>0, 8, 8&#45;&gt;0, 9, 8</title>\n",
       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M351.37,-72.76C346.18,-64.32 339.72,-53.8 333.9,-44.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"336.78,-42.32 328.56,-35.63 330.82,-45.99 336.78,-42.32\"/>\n",
       "</g>\n",
       "<!-- 0, 8, 9 -->\n",
       "<g id=\"node15\" class=\"node\">\n",
       "<title>0, 8, 9</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" cx=\"404.35\" cy=\"-18\" rx=\"33.6\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"404.35\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">0, 8, 9</text>\n",
       "</g>\n",
       "<!-- 0, 8, 8&#45;&gt;0, 8, 9 -->\n",
       "<g id=\"edge20\" class=\"edge\">\n",
       "<title>0, 8, 8&#45;&gt;0, 8, 9</title>\n",
       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M371.32,-72.76C376.51,-64.32 382.97,-53.8 388.8,-44.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"391.88,-45.99 394.13,-35.63 385.91,-42.32 391.88,-45.99\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<graphviz.dot.Digraph at 0x7fbbc1da0dc0>"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "text/plain": [
       "<Figure size 432x288 with 0 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "graph = defaultdict(list)\n",
    "root = (0,8,5)\n",
    "graph[root] = []\n",
    "max_depth = sum(root) + 4\n",
    "for c in range(sum(root),max_depth):\n",
    "    for k in list(graph.keys()):\n",
    "        if sum(k) == c:\n",
    "            l = (0,k[1] + 1,k[2])\n",
    "            r = (0,k[1],k[2] + 1)\n",
    "            graph[k] = [l,r]\n",
    "            graph[l] = []\n",
    "            graph[r] = []\n",
    "print(list(graph.items())[0])\n",
    "items = list(sorted(graph.items(), key=lambda x: sum(x[0])))\n",
    "g = Digraph(format=\"eps\")\n",
    "added = set()\n",
    "plt.tight_layout()\n",
    "for (p, cs) in items:\n",
    "    node_str = str(p)[1:-1]\n",
    "    if not cs:\n",
    "        g.node(node_str,style=\"dotted\")\n",
    "    else:\n",
    "        g.node(node_str)\n",
    "    for c in cs:\n",
    "        child_str = str(c)[1:-1]\n",
    "        if not child_str in added:\n",
    "            added.add(child_str)\n",
    "        if sum(c) == max_depth:\n",
    "            g.edge(node_str, child_str,style=\"dotted\")\n",
    "        else:\n",
    "            g.edge(node_str, child_str)\n",
    "        \n",
    "g.render('counter-example-tree')\n",
    "g"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "id": "c802f26f",
   "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.43.0 (0)\n",
       " -->\n",
       "<!-- Title: %3 Pages: 1 -->\n",
       "<svg width=\"242pt\" height=\"188pt\"\n",
       " viewBox=\"0.00 0.00 242.29 188.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 184)\">\n",
       "<title>%3</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-184 238.29,-184 238.29,4 -4,4\"/>\n",
       "<!-- 10, 10 -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>10, 10</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"117.15\" cy=\"-162\" rx=\"33.29\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"117.15\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">10, 10</text>\n",
       "</g>\n",
       "<!-- 11, 10 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>11, 10</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"75.15\" cy=\"-90\" rx=\"33.29\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"75.15\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">11, 10</text>\n",
       "</g>\n",
       "<!-- 10, 10&#45;&gt;11, 10 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>10, 10&#45;&gt;11, 10</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M107.41,-144.76C102.34,-136.32 96.03,-125.8 90.33,-116.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"93.27,-114.41 85.13,-107.63 87.27,-118.01 93.27,-114.41\"/>\n",
       "</g>\n",
       "<!-- 10, 11 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>10, 11</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"159.15\" cy=\"-90\" rx=\"33.29\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"159.15\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">10, 11</text>\n",
       "</g>\n",
       "<!-- 10, 10&#45;&gt;10, 11 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>10, 10&#45;&gt;10, 11</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M126.89,-144.76C131.96,-136.32 138.27,-125.8 143.96,-116.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"147.02,-118.01 149.17,-107.63 141.02,-114.41 147.02,-118.01\"/>\n",
       "</g>\n",
       "<!-- 12, 10 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>12, 10</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"33.15\" cy=\"-18\" rx=\"33.29\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"33.15\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">12, 10</text>\n",
       "</g>\n",
       "<!-- 11, 10&#45;&gt;12, 10 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>11, 10&#45;&gt;12, 10</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M65.41,-72.76C60.34,-64.32 54.03,-53.8 48.33,-44.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"51.27,-42.41 43.13,-35.63 45.27,-46.01 51.27,-42.41\"/>\n",
       "</g>\n",
       "<!-- 11, 11 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>11, 11</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"117.15\" cy=\"-18\" rx=\"33.29\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"117.15\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">11, 11</text>\n",
       "</g>\n",
       "<!-- 11, 10&#45;&gt;11, 11 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>11, 10&#45;&gt;11, 11</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M84.89,-72.76C89.96,-64.32 96.27,-53.8 101.96,-44.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"105.02,-46.01 107.17,-35.63 99.02,-42.41 105.02,-46.01\"/>\n",
       "</g>\n",
       "<!-- 10, 11&#45;&gt;11, 11 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>10, 11&#45;&gt;11, 11</title>\n",
       "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"1,5\" d=\"M149.41,-72.76C144.34,-64.32 138.03,-53.8 132.33,-44.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"135.27,-42.41 127.13,-35.63 129.27,-46.01 135.27,-42.41\"/>\n",
       "</g>\n",
       "<!-- 10, 12 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>10, 12</title>\n",
       "<ellipse fill=\"none\" stroke=\"black\" cx=\"201.15\" cy=\"-18\" rx=\"33.29\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"201.15\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">10, 12</text>\n",
       "</g>\n",
       "<!-- 10, 11&#45;&gt;10, 12 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>10, 11&#45;&gt;10, 12</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M168.89,-72.76C173.96,-64.32 180.27,-53.8 185.96,-44.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"189.02,-46.01 191.17,-35.63 183.02,-42.41 189.02,-46.01\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<graphviz.dot.Digraph at 0x7fbbd9484730>"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "g = Digraph(format=\"eps\")\n",
    "# g.edges(['AL','AM','AR'])\n",
    "seen = set()\n",
    "for p in [(10,10),(11,10),(10,11)]:\n",
    "    node_str = str(p)[1:-1]\n",
    "    children = [(p[0]+1,p[1]),(p[0],p[1]+1)]\n",
    "    for c in children:\n",
    "        child_str = str(c)[1:-1]\n",
    "        if c not in seen:\n",
    "            g.edge(node_str, child_str)\n",
    "            seen.add(c)\n",
    "        else:\n",
    "            g.edge(node_str, child_str,style=\"dotted\")\n",
    "# g.edge('10, 10, 11','10, 11, 10',style=\"invis\")\n",
    "g.render('ict')\n",
    "g"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "a866aab9",
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "3afc3ead",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}