proofs_propositional/search_ann_ex0.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "# type: ignore\n",
    "\n",
    "try:\n",
    "  import sys\n",
    "  sys.path.append('../')\n",
    "  from modules.search_prop import *\n",
    "except ImportError:\n",
    "  url = 'https://raw.githubusercontent.com/jhjeong314/Proofmood/main/modules'\n",
    "  import httpimport\n",
    "  with httpimport.remote_repo(url):\n",
    "    from search_prop import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'imp intro' rule successfully applied to line 6.\n",
      "'imp intro' rule successfully applied to line 5.\n",
      "'repeat' rule successfully applied to line 4.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. A\t .hyp\n",
      "│├─\n",
      "│││3. B\t .hyp\n",
      "││├─\n",
      "│││4. A\t\u001b[92m✓\u001b[39m repeat 2\n",
      "││5. B imp A\t\u001b[92m✓\u001b[39m imp intro 3-4\n",
      "│6. A imp B imp A\t\u001b[92m✓\u001b[39m imp intro 2-5\n"
     ]
    }
   ],
   "source": [
    "# Axiom 1 (Hilbert, Lukasiewicz)\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. A .hyp\n",
    "  proves\n",
    "    3. B .hyp\n",
    "    proves\n",
    "    4. A \n",
    "  5. B imp A \n",
    "6. A imp (B imp A) \n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'imp intro' rule successfully applied to line 10.\n",
      "'imp intro' rule successfully applied to line 9.\n",
      "'imp intro' rule successfully applied to line 8.\n",
      "'repeat' rule for line 7 failed.\n",
      "'bot elim' rule for line 7 failed.\n",
      "'not elim' rule for line 7 failed.\n",
      "'imp elim' rule successfully applied to line 7.\n",
      "'imp intro' rule for line 6 failed.\n",
      "'repeat' rule for line 6 failed.\n",
      "'bot elim' rule for line 6 failed.\n",
      "'not elim' rule for line 6 failed.\n",
      "'imp elim' rule successfully applied to line 6.\n",
      "'repeat' rule for line 5 failed.\n",
      "'bot elim' rule for line 5 failed.\n",
      "'not elim' rule for line 5 failed.\n",
      "'imp elim' rule successfully applied to line 5.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. A imp B imp C\t .hyp\n",
      "│├─\n",
      "│││3. A imp B\t .hyp\n",
      "││├─\n",
      "││││4. A\t .hyp\n",
      "│││├─\n",
      "││││5. B\t\u001b[92m✓\u001b[39m imp elim 3,4\n",
      "││││6. B imp C\t\u001b[92m✓\u001b[39m imp elim 2,4\n",
      "││││7. C\t\u001b[92m✓\u001b[39m imp elim 5,6\n",
      "│││8. A imp C\t\u001b[92m✓\u001b[39m imp intro 4-7\n",
      "││9. (A imp B) imp A imp C\t\u001b[92m✓\u001b[39m imp intro 3-8\n",
      "│10. (A imp B imp C) imp (A imp B) imp A imp C\t\u001b[92m✓\u001b[39m imp intro 2-9\n"
     ]
    }
   ],
   "source": [
    "# Axiom 2 (Hilbert, Lukasiewicz)\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. A imp (B imp C) .hyp\n",
    "  proves\n",
    "    3. A imp B .hyp\n",
    "    proves\n",
    "      4. A .hyp\n",
    "      proves\n",
    "      5. B\n",
    "      6. B imp C \n",
    "      7. C\n",
    "    8. A imp C\n",
    "  9. (A imp B) imp (A imp C)\n",
    "10. (A imp (B imp C)) imp ((A imp B) imp (A imp C))\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'imp intro' rule successfully applied to line 10.\n",
      "'imp intro' rule successfully applied to line 9.\n",
      "'imp intro' rule successfully applied to line 8.\n",
      "'repeat' rule for line 7 failed.\n",
      "'bot elim' rule for line 7 failed.\n",
      "'not elim' rule for line 7 failed.\n",
      "'imp elim' rule successfully applied to line 7.\n",
      "'imp intro' rule for line 6 failed.\n",
      "'repeat' rule for line 6 failed.\n",
      "'bot elim' rule for line 6 failed.\n",
      "'not elim' rule for line 6 failed.\n",
      "'imp elim' rule successfully applied to line 6.\n",
      "'repeat' rule for line 5 failed.\n",
      "'bot elim' rule for line 5 failed.\n",
      "'not elim' rule for line 5 failed.\n",
      "'imp elim' rule successfully applied to line 5.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. A imp B imp C\t .hyp\n",
      "│├─\n",
      "│││3. A imp B\t .hyp\n",
      "││├─\n",
      "││││4. A\t .hyp\n",
      "│││├─\n",
      "││││5. B\t\u001b[92m✓\u001b[39m imp elim 3,4\n",
      "││││6. B imp C\t\u001b[92m✓\u001b[39m imp elim 2,4\n",
      "││││7. C\t\u001b[92m✓\u001b[39m imp elim 5,6\n",
      "│││8. A imp C\t\u001b[92m✓\u001b[39m imp intro 4-7\n",
      "││9. (A imp B) imp A imp C\t\u001b[92m✓\u001b[39m imp intro 3-8\n",
      "│10. (A imp B imp C) imp (A imp B) imp A imp C\t\u001b[92m✓\u001b[39m imp intro 2-9\n"
     ]
    }
   ],
   "source": [
    "# Axiom 3 (Hilbert, Lukasiewicz), aka contraposition\n",
    "\n",
    "prf_str4 = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. not B imp not A .hyp\n",
    "  proves\n",
    "    3. A .hyp\n",
    "    proves\n",
    "      4. not B .hyp\n",
    "      proves\n",
    "      5. not A \n",
    "      6. bot \n",
    "    7. B \n",
    "  8. A imp B \n",
    "9. (not B imp not A) imp (A imp B) \n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'imp intro' rule successfully applied to line 7.\n",
      "'imp intro' rule successfully applied to line 6.\n",
      "'repeat' rule for line 5 failed.\n",
      "'bot elim' rule successfully applied to line 5.\n",
      "'bot intro' rule successfully applied to line 4.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. not A\t .hyp\n",
      "│├─\n",
      "│││3. A\t .hyp\n",
      "││├─\n",
      "│││4. bot\t\u001b[92m✓\u001b[39m bot intro 2,3\n",
      "│││5. B\t\u001b[92m✓\u001b[39m bot elim 4\n",
      "││6. A imp B\t\u001b[92m✓\u001b[39m imp intro 3-5\n",
      "│7. not A imp A imp B\t\u001b[92m✓\u001b[39m imp intro 2-6\n"
     ]
    }
   ],
   "source": [
    "# not A imp (A imp B)\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. not A .hyp\n",
    "  proves\n",
    "    3. A .hyp\n",
    "    proves\n",
    "    4. bot \n",
    "    5. B \n",
    "  6. A imp B \n",
    "7. not A imp (A imp B) \n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. A\t .hyp\n",
      "│├─\n",
      "│││3. A imp B\t .hyp\n",
      "││├─\n",
      "││││4. A\t .hyp\n",
      "│││├─\n",
      "││││5. B\t\u001b[92m✓\u001b[39m imp elim 3,4\n",
      "│││6. A imp B\t\u001b[92m✓\u001b[39m imp intro 4-5\n",
      "│││7. B\t\u001b[92m✓\u001b[39m imp elim 6,2\n",
      "││8. (A imp B) imp B\t\u001b[92m✓\u001b[39m imp intro 3-7\n",
      "│9. A imp (A imp B) imp B\t\u001b[92m✓\u001b[39m imp intro 2-8\n"
     ]
    }
   ],
   "source": [
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. A .hyp\n",
    "  proves\n",
    "    3. A imp B .hyp\n",
    "    proves\n",
    "      4. A .hyp\n",
    "      proves\n",
    "      5. B .imp elim 3,4\n",
    "    6. A imp B .imp intro 4-5\n",
    "    7. B .imp elim 6,2\n",
    "  8. (A imp B) imp B .imp intro 3-7\n",
    "9. A imp ((A imp B) imp B) .imp intro 2-8\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'imp intro' rule successfully applied to line 9.\n",
      "'imp intro' rule successfully applied to line 8.\n",
      "'imp intro' rule successfully applied to line 7.\n",
      "'repeat' rule for line 6 failed.\n",
      "'bot elim' rule for line 6 failed.\n",
      "'not elim' rule for line 6 failed.\n",
      "'imp elim' rule successfully applied to line 6.\n",
      "'repeat' rule for line 5 failed.\n",
      "'bot elim' rule for line 5 failed.\n",
      "'not elim' rule for line 5 failed.\n",
      "'imp elim' rule successfully applied to line 5.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. A imp B\t .hyp\n",
      "│├─\n",
      "│││3. B imp C\t .hyp\n",
      "││├─\n",
      "││││4. A\t .hyp\n",
      "│││├─\n",
      "││││5. B\t\u001b[92m✓\u001b[39m imp elim 2,4\n",
      "││││6. C\t\u001b[92m✓\u001b[39m imp elim 3,5\n",
      "│││7. A imp C\t\u001b[92m✓\u001b[39m imp intro 4-6\n",
      "││8. (B imp C) imp A imp C\t\u001b[92m✓\u001b[39m imp intro 3-7\n",
      "│9. (A imp B) imp (B imp C) imp A imp C\t\u001b[92m✓\u001b[39m imp intro 2-8\n"
     ]
    }
   ],
   "source": [
    "# Transitivity of Implication\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. A imp B .hyp\n",
    "  proves\n",
    "    3. B imp C .hyp\n",
    "    proves\n",
    "      4. A .hyp\n",
    "      proves\n",
    "      5. B \n",
    "      6. C \n",
    "    7. A imp C \n",
    "  8. (B imp C) imp (A imp C) \n",
    "9. (A imp B) imp ((B imp C) imp (A imp C)) \n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'iff intro' rule successfully applied to line 16.\n",
      "'imp intro' rule successfully applied to line 15.\n",
      "'imp intro' rule successfully applied to line 14.\n",
      "'repeat' rule for line 13 failed.\n",
      "'bot elim' rule for line 13 failed.\n",
      "'not elim' rule for line 13 failed.\n",
      "'imp elim' rule successfully applied to line 13.\n",
      "'and intro' rule successfully applied to line 12.\n",
      "'imp intro' rule successfully applied to line 8.\n",
      "'repeat' rule for line 7 failed.\n",
      "'bot elim' rule for line 7 failed.\n",
      "'not elim' rule for line 7 failed.\n",
      "'imp elim' rule successfully applied to line 7.\n",
      "'repeat' rule for line 6 failed.\n",
      "'bot elim' rule for line 6 failed.\n",
      "'not elim' rule for line 6 failed.\n",
      "'imp elim' rule for line 6 failed.\n",
      "'iff elim' rule for line 6 failed.\n",
      "'and elim' rule successfully applied to line 6.\n",
      "'imp intro' rule for line 5 failed.\n",
      "'repeat' rule for line 5 failed.\n",
      "'bot elim' rule for line 5 failed.\n",
      "'not elim' rule for line 5 failed.\n",
      "'imp elim' rule successfully applied to line 5.\n",
      "'repeat' rule for line 4 failed.\n",
      "'bot elim' rule for line 4 failed.\n",
      "'not elim' rule for line 4 failed.\n",
      "'imp elim' rule for line 4 failed.\n",
      "'iff elim' rule for line 4 failed.\n",
      "'and elim' rule successfully applied to line 4.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. A imp B imp C\t .hyp\n",
      "│├─\n",
      "│││3. A and B\t .hyp\n",
      "││├─\n",
      "│││4. A\t\u001b[92m✓\u001b[39m and elim 3\n",
      "│││5. B imp C\t\u001b[92m✓\u001b[39m imp elim 2,4\n",
      "│││6. B\t\u001b[92m✓\u001b[39m and elim 3\n",
      "│││7. C\t\u001b[92m✓\u001b[39m imp elim 5,6\n",
      "││8. A and B imp C\t\u001b[92m✓\u001b[39m imp intro 3-7\n",
      "││9. A and B imp C\t .hyp\n",
      "│├─\n",
      "│││10. A\t .hyp\n",
      "││├─\n",
      "││││11. B\t .hyp\n",
      "│││├─\n",
      "││││12. A and B\t\u001b[92m✓\u001b[39m and intro 10,11\n",
      "││││13. C\t\u001b[92m✓\u001b[39m imp elim 9,12\n",
      "│││14. B imp C\t\u001b[92m✓\u001b[39m imp intro 11-13\n",
      "││15. A imp B imp C\t\u001b[92m✓\u001b[39m imp intro 10-14\n",
      "│16. (A and B imp C) iff (A imp B imp C)\t\u001b[92m✓\u001b[39m iff intro 2-8,9-15\n"
     ]
    }
   ],
   "source": [
    "# Transitivity of implication may be easier to understand\n",
    "# if we write it as follows:\n",
    "#   (A imp B) and (B imp C) imp (A imp C)\n",
    "# In fact, the following is a tautology.\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. A imp (B imp C) .hyp\n",
    "  proves\n",
    "    3. A and B .hyp\n",
    "    proves\n",
    "    4. A \n",
    "    5. B imp C \n",
    "    6. B \n",
    "    7. C \n",
    "  8. A and B imp C \n",
    "  9. A and B imp C .hyp\n",
    "  proves\n",
    "    10. A .hyp\n",
    "    proves\n",
    "      11. B  .hyp\n",
    "      proves\n",
    "      12. A and B \n",
    "      13. C \n",
    "    14. B imp C \n",
    "  15. A imp (B imp C) \n",
    "16. (A and B imp C) iff (A imp (B imp C)) \n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'imp intro' rule successfully applied to line 6.\n",
      "'repeat' rule for line 5 failed.\n",
      "'bot elim' rule for line 5 failed.\n",
      "'not elim' rule successfully applied to line 5.\n",
      "'bot intro' rule successfully applied to line 4.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. not not A\t .hyp\n",
      "│├─\n",
      "│││3. not A\t .hyp\n",
      "││├─\n",
      "│││4. bot\t\u001b[92m✓\u001b[39m bot intro 2,3\n",
      "││5. A\t\u001b[92m✓\u001b[39m not elim 3-4\n",
      "│6. not not A imp A\t\u001b[92m✓\u001b[39m imp intro 2-5\n"
     ]
    }
   ],
   "source": [
    "# Double negation elimination\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. not not A .hyp\n",
    "  proves\n",
    "    3. not A .hyp\n",
    "    proves\n",
    "    4. bot \n",
    "  5. A \n",
    "7. not not A imp A \n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'imp intro' rule successfully applied to line 6.\n",
      "'not intro' rule successfully applied to line 5.\n",
      "'bot intro' rule successfully applied to line 4.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. A\t .hyp\n",
      "│├─\n",
      "│││3. not A\t .hyp\n",
      "││├─\n",
      "│││4. bot\t\u001b[92m✓\u001b[39m bot intro 2,3\n",
      "││5. not not A\t\u001b[92m✓\u001b[39m not intro 3-4\n",
      "│6. A imp not not A\t\u001b[92m✓\u001b[39m imp intro 2-5\n"
     ]
    }
   ],
   "source": [
    "# Double negation introduction\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. A .hyp\n",
    "  proves\n",
    "    3. not A .hyp\n",
    "    proves\n",
    "    4. bot \n",
    "  5. not not A \n",
    "7. A imp not not A \n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle (\\neg\\, A \\rightarrow B) \\rightarrow (\\neg\\, A \\rightarrow \\neg\\, B) \\rightarrow A$"
      ],
      "text/plain": [
       "<IPython.core.display.Math object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'imp intro' rule successfully applied to line 10.\n",
      "'imp intro' rule successfully applied to line 9.\n",
      "'repeat' rule for line 8 failed.\n",
      "'bot elim' rule for line 8 failed.\n",
      "'not elim' rule successfully applied to line 8.\n",
      "'bot intro' rule successfully applied to line 7.\n",
      "'not intro' rule for line 6 failed.\n",
      "'repeat' rule for line 6 failed.\n",
      "'bot elim' rule for line 6 failed.\n",
      "'not elim' rule for line 6 failed.\n",
      "'imp elim' rule successfully applied to line 6.\n",
      "'repeat' rule for line 5 failed.\n",
      "'bot elim' rule for line 5 failed.\n",
      "'not elim' rule for line 5 failed.\n",
      "'imp elim' rule successfully applied to line 5.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. not A imp B\t .hyp\n",
      "│├─\n",
      "│││3. not A imp not B\t .hyp\n",
      "││├─\n",
      "││││4. not A\t .hyp\n",
      "│││├─\n",
      "││││5. B\t\u001b[92m✓\u001b[39m imp elim 2,4\n",
      "││││6. not B\t\u001b[92m✓\u001b[39m imp elim 3,4\n",
      "││││7. bot\t\u001b[92m✓\u001b[39m bot intro 5,6\n",
      "│││8. A\t\u001b[92m✓\u001b[39m not elim 4-7\n",
      "││9. (not A imp not B) imp A\t\u001b[92m✓\u001b[39m imp intro 3-8\n",
      "│10. (not A imp B) imp (not A imp not B) imp A\t\u001b[92m✓\u001b[39m imp intro 2-9\n"
     ]
    }
   ],
   "source": [
    "# Following is a version of the Hilbert-Lukasiewicz axiom 3.\n",
    "fmla = '(not A imp B) imp (not A imp not B) imp A'\n",
    "show_formula(fmla)\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. not A imp B .hyp\n",
    "  proves\n",
    "    3. not A imp not B .hyp\n",
    "    proves\n",
    "      4. not A .hyp\n",
    "      proves\n",
    "      5. B \n",
    "      6. not B \n",
    "      7. bot \n",
    "    8. A \n",
    "  9. (not A imp not B) imp A \n",
    "10. (not A imp B) imp (not A imp not B) imp A \n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "mlenv",
   "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.11.2"
  },
  "orig_nbformat": 4
 },
 "nbformat": 4,
 "nbformat_minor": 2
}