Demo notebook associated the metamath primer presentation

demo.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [],
   "source": [
    "import metamathpy as mm\n",
    "import metamathpy.database as md\n",
    "import metamathpy.proof as mp\n",
    "from metamathpy.environment import Environment"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [],
   "source": [
    "set_db = md.parse('../set.mm/set.mm', last_rule='a1i')\n",
    "demo_db = md.parse('../set.mm/demo0.mm')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Proof of th1 in demo0.mm"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "['tt',\n",
       " 'tze',\n",
       " 'tpl',\n",
       " 'tt',\n",
       " 'weq',\n",
       " 'tt',\n",
       " 'tt',\n",
       " 'weq',\n",
       " 'tt',\n",
       " 'a2',\n",
       " 'tt',\n",
       " 'tze',\n",
       " 'tpl',\n",
       " 'tt',\n",
       " 'weq',\n",
       " 'tt',\n",
       " 'tze',\n",
       " 'tpl',\n",
       " 'tt',\n",
       " 'weq',\n",
       " 'tt',\n",
       " 'tt',\n",
       " 'weq',\n",
       " 'wim',\n",
       " 'tt',\n",
       " 'a2',\n",
       " 'tt',\n",
       " 'tze',\n",
       " 'tpl',\n",
       " 'tt',\n",
       " 'tt',\n",
       " 'a1',\n",
       " 'mp',\n",
       " 'mp']"
      ]
     },
     "execution_count": 60,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "th1_proof = demo_db.rules['th1'].consequent.proof\n",
    "th1_proof"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "34"
      ]
     },
     "execution_count": 61,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "len(th1_proof)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Example: verifying th1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 62,
   "metadata": {},
   "outputs": [],
   "source": [
    "demo_env = Environment(demo_db)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(<metamathpy.database.Rule at 0x104acb1c0>, [], [])"
      ]
     },
     "execution_count": 66,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "claim, proof, stack = demo_env.reset(demo_db.rules['th1'])\n",
    "claim, proof, stack"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "th1 $p |- t = t $.\n",
      "disjoint variable sets: set()\n",
      "  tt $f term t $.\n",
      "\n"
     ]
    }
   ],
   "source": [
    "print(claim)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "tt [ProofStep(conclusion=[tt] term t)]\n",
      "tze [ProofStep(conclusion=[tt] term t), ProofStep(conclusion=[tze] term 0)]\n",
      "tpl [ProofStep(conclusion=[tpl] term ( t + 0 ))]\n",
      "tt [ProofStep(conclusion=[tpl] term ( t + 0 )), ProofStep(conclusion=[tt] term t)]\n",
      "weq [ProofStep(conclusion=[weq] wff ( t + 0 ) = t)]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[tt] term t)]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[tt] term t), ProofStep(conclusion=[tt] term t)]\n",
      "weq [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t)]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[tt] term t)]\n",
      "a2 [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t)]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[tt] term t)]\n",
      "tze [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[tt] term t), ProofStep(conclusion=[tze] term 0)]\n",
      "tpl [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[tpl] term ( t + 0 ))]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[tpl] term ( t + 0 )), ProofStep(conclusion=[tt] term t)]\n",
      "weq [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t)]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[tt] term t)]\n",
      "tze [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[tt] term t), ProofStep(conclusion=[tze] term 0)]\n",
      "tpl [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[tpl] term ( t + 0 ))]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[tpl] term ( t + 0 )), ProofStep(conclusion=[tt] term t)]\n",
      "weq [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t)]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[tt] term t)]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[tt] term t), ProofStep(conclusion=[tt] term t)]\n",
      "weq [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t)]\n",
      "wim [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[wim] wff ( ( t + 0 ) = t -> t = t ))]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[wim] wff ( ( t + 0 ) = t -> t = t )), ProofStep(conclusion=[tt] term t)]\n",
      "a2 [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[wim] wff ( ( t + 0 ) = t -> t = t )), ProofStep(conclusion=[a2] |- ( t + 0 ) = t)]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[wim] wff ( ( t + 0 ) = t -> t = t )), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[tt] term t)]\n",
      "tze [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[wim] wff ( ( t + 0 ) = t -> t = t )), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[tt] term t), ProofStep(conclusion=[tze] term 0)]\n",
      "tpl [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[wim] wff ( ( t + 0 ) = t -> t = t )), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[tpl] term ( t + 0 ))]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[wim] wff ( ( t + 0 ) = t -> t = t )), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[tpl] term ( t + 0 )), ProofStep(conclusion=[tt] term t)]\n",
      "tt [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[wim] wff ( ( t + 0 ) = t -> t = t )), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[tpl] term ( t + 0 )), ProofStep(conclusion=[tt] term t), ProofStep(conclusion=[tt] term t)]\n",
      "a1 [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[wim] wff ( ( t + 0 ) = t -> t = t )), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[a1] |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ))]\n",
      "mp [ProofStep(conclusion=[weq] wff ( t + 0 ) = t), ProofStep(conclusion=[weq] wff t = t), ProofStep(conclusion=[a2] |- ( t + 0 ) = t), ProofStep(conclusion=[mp] |- ( ( t + 0 ) = t -> t = t ))]\n",
      "mp [ProofStep(conclusion=[mp] |- t = t)]\n"
     ]
    }
   ],
   "source": [
    "# RPN and stack\n",
    "for thm in th1_proof:\n",
    "    state, msg = demo_env.step(thm)\n",
    "    claim, proof, stack = state\n",
    "    print(thm, stack)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(('|-', 't', '=', 't'),\n",
       " Statement(label='th1', tag='$p', tokens=['|-', 't', '=', 't'], proof=['tt', 'tze', 'tpl', 'tt', 'weq', 'tt', 'tt', 'weq', 'tt', 'a2', 'tt', 'tze', 'tpl', 'tt', 'weq', 'tt', 'tze', 'tpl', 'tt', 'weq', 'tt', 'tt', 'weq', 'wim', 'tt', 'a2', 'tt', 'tze', 'tpl', 'tt', 'tt', 'a1', 'mp', 'mp']))"
      ]
     },
     "execution_count": 68,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "stack[0].conclusion, claim.consequent"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 69,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(claim.consequent.tokens) == stack[0].conclusion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Example: verifying a1i"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {},
   "outputs": [],
   "source": [
    "set_env = Environment(set_db)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(<metamathpy.database.Rule at 0x104acb610>, [], [])"
      ]
     },
     "execution_count": 71,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "claim, proof, stack = set_env.reset(set_db.rules['a1i'])\n",
    "claim, proof, stack"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "a1i $p |- ( ps -> ph ) $.\n",
      "disjoint variable sets: set()\n",
      "  wph $f wff ph $.\n",
      "  wps $f wff ps $.\n",
      "  a1i.1 $e |- ph $.\n",
      "\n"
     ]
    }
   ],
   "source": [
    "print(claim)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[ProofStep(conclusion=[wph] wff ph)]\n",
      "[ProofStep(conclusion=[wph] wff ph), ProofStep(conclusion=[wps] wff ps)]\n",
      "[ProofStep(conclusion=[wph] wff ph), ProofStep(conclusion=[wps] wff ps), ProofStep(conclusion=[wph] wff ph)]\n",
      "[ProofStep(conclusion=[wph] wff ph), ProofStep(conclusion=[wi] wff ( ps -> ph ))]\n",
      "[ProofStep(conclusion=[wph] wff ph), ProofStep(conclusion=[wi] wff ( ps -> ph )), ProofStep(conclusion=[a1i.1] |- ph)]\n",
      "[ProofStep(conclusion=[wph] wff ph), ProofStep(conclusion=[wi] wff ( ps -> ph )), ProofStep(conclusion=[a1i.1] |- ph), ProofStep(conclusion=[wph] wff ph)]\n",
      "[ProofStep(conclusion=[wph] wff ph), ProofStep(conclusion=[wi] wff ( ps -> ph )), ProofStep(conclusion=[a1i.1] |- ph), ProofStep(conclusion=[wph] wff ph), ProofStep(conclusion=[wps] wff ps)]\n",
      "[ProofStep(conclusion=[wph] wff ph), ProofStep(conclusion=[wi] wff ( ps -> ph )), ProofStep(conclusion=[a1i.1] |- ph), ProofStep(conclusion=[ax-1] |- ( ph -> ( ps -> ph ) ))]\n",
      "[ProofStep(conclusion=[ax-mp] |- ( ps -> ph ))]\n"
     ]
    }
   ],
   "source": [
    "# RPN and stack\n",
    "for thm in ('wph', 'wps', 'wph', 'wi', 'a1i.1', 'wph', 'wps', 'ax-1', 'ax-mp'):\n",
    "    state, msg = set_env.step(thm)\n",
    "    claim, proof, stack = state\n",
    "    print(stack)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(('|-', '(', 'ps', '->', 'ph', ')'),\n",
       " Statement(label='a1i', tag='$p', tokens=['|-', '(', 'ps', '->', 'ph', ')'], proof=['(', 'wi', 'ax-1', 'ax-mp', ')', 'ABADCABEF']))"
      ]
     },
     "execution_count": 74,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "stack[0].conclusion, claim.consequent"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 75,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 75,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "stack[0].conclusion == tuple(claim.consequent.tokens)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Representing proofs as trees"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[ <= ax-mp] |- ( ps -> ph ) {'ph': 'ph', 'ps': '( ps -> ph )'}\n",
      " [wph <= wph] wff ph {}\n",
      " [wps <= wi] wff ( ps -> ph ) {'ph': 'ps', 'ps': 'ph'}\n",
      "  [wph <= wps] wff ps {}\n",
      "  [wps <= wph] wff ph {}\n",
      " [min <= a1i.1] |- ph {}\n",
      " [maj <= ax-1] |- ( ph -> ( ps -> ph ) ) {'ph': 'ph', 'ps': 'ps'}\n",
      "  [wph <= wph] wff ph {}\n",
      "  [wps <= wps] wff ps {}\n",
      "\n"
     ]
    }
   ],
   "source": [
    "root, steps = mp.verify_proof(set_db, set_db.rules['a1i'])\n",
    "print(root.tree_string())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "a1i_proof = root.normal_proof()\n",
    "a1i_proof"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 77,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[ <= mp] |- t = t {'P': '( t + 0 ) = t', 'Q': 't = t'}\n",
      " [wp <= weq] wff ( t + 0 ) = t {'t': '( t + 0 )', 'r': 't'}\n",
      "  [tt <= tpl] term ( t + 0 ) {'t': 't', 'r': '0'}\n",
      "   [tt <= tt] term t {}\n",
      "   [tr <= tze] term 0 {}\n",
      "  [tr <= tt] term t {}\n",
      " [wq <= weq] wff t = t {'t': 't', 'r': 't'}\n",
      "  [tt <= tt] term t {}\n",
      "  [tr <= tt] term t {}\n",
      " [min <= a2] |- ( t + 0 ) = t {'t': 't'}\n",
      "  [tt <= tt] term t {}\n",
      " [maj <= mp] |- ( ( t + 0 ) = t -> t = t ) {'P': '( t + 0 ) = t', 'Q': '( ( t + 0 ) = t -> t = t )'}\n",
      "  [wp <= weq] wff ( t + 0 ) = t {'t': '( t + 0 )', 'r': 't'}\n",
      "   [tt <= tpl] term ( t + 0 ) {'t': 't', 'r': '0'}\n",
      "    [tt <= tt] term t {}\n",
      "    [tr <= tze] term 0 {}\n",
      "   [tr <= tt] term t {}\n",
      "  [wq <= wim] wff ( ( t + 0 ) = t -> t = t ) {'P': '( t + 0 ) = t', 'Q': 't = t'}\n",
      "   [wp <= weq] wff ( t + 0 ) = t {'t': '( t + 0 )', 'r': 't'}\n",
      "    [tt <= tpl] term ( t + 0 ) {'t': 't', 'r': '0'}\n",
      "     [tt <= tt] term t {}\n",
      "     [tr <= tze] term 0 {}\n",
      "    [tr <= tt] term t {}\n",
      "   [wq <= weq] wff t = t {'t': 't', 'r': 't'}\n",
      "    [tt <= tt] term t {}\n",
      "    [tr <= tt] term t {}\n",
      "  [min <= a2] |- ( t + 0 ) = t {'t': 't'}\n",
      "   [tt <= tt] term t {}\n",
      "  [maj <= a1] |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) {'t': '( t + 0 )', 'r': 't', 's': 't'}\n",
      "   [tt <= tpl] term ( t + 0 ) {'t': 't', 'r': '0'}\n",
      "    [tt <= tt] term t {}\n",
      "    [tr <= tze] term 0 {}\n",
      "   [tr <= tt] term t {}\n",
      "   [ts <= tt] term t {}\n",
      "\n"
     ]
    }
   ],
   "source": [
    "root, steps = mp.verify_proof(demo_db, demo_db.rules['th1'])\n",
    "print(root.tree_string())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "lab",
   "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.10.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}