realpytest.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "bc72cb91-2972-4104-bcc4-cca2517c788f",
   "metadata": {},
   "source": [
    "# RealPy"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "c8976e80-ee2f-4346-9bb8-9b288fcc144e",
   "metadata": {},
   "outputs": [],
   "source": [
    "from IPython.display import display, Math, Markdown, Latex, display_markdown, HTML\n",
    "#import pandas as pd\n",
    "from sympy.logic.boolalg import truth_table, distribute_and_over_or, distribute_or_over_and, distribute_xor_over_and, Xor, And, Or, Not, Implies, Equivalent, eliminate_implications\n",
    "from sympy.abc import x,y,z,A,B,C\n",
    "from sympy import latex, S\n",
    "\n",
    "import realpy.tf\n",
    "import realpy.core\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "7c43a94b-b1f0-4d30-8a21-495bbfbd3fb6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The proof is complete.\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Statement</th>\n",
       "      <th>Block ID</th>\n",
       "      <th>Rule</th>\n",
       "      <th>Lines</th>\n",
       "      <th>Blocks</th>\n",
       "      <th>Status</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>Line</th>\n",
       "      <td>~A</td>\n",
       "      <td>1</td>\n",
       "      <td>Goal</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>Implies(A, B)</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>~B</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>A</td>\n",
       "      <td>11</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>B</td>\n",
       "      <td>11</td>\n",
       "      <td>ImpElim</td>\n",
       "      <td>3, 1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>False</td>\n",
       "      <td>11</td>\n",
       "      <td>NegElim</td>\n",
       "      <td>2, 4</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>~A</td>\n",
       "      <td>1</td>\n",
       "      <td>NegIntro</td>\n",
       "      <td></td>\n",
       "      <td>11</td>\n",
       "      <td>Complete</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "          Statement Block ID        Rule Lines Blocks    Status\n",
       "Line             ~A        1        Goal                       \n",
       "1     Implies(A, B)        1     Premise                       \n",
       "2                ~B        1     Premise                       \n",
       "3                 A       11  Assumption                       \n",
       "4                 B       11     ImpElim  3, 1                 \n",
       "5             False       11     NegElim  2, 4                 \n",
       "6                ~A        1    NegIntro           11  Complete"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "mt = realpy.tf.Proof([A >> B, ~B], ~A, 'Modus Tollens')\n",
    "mt.openblock(A)\n",
    "mt.impelim(3,1)\n",
    "mt.negelim(2,4)\n",
    "mt.closeblock()\n",
    "mt.negintro('11')\n",
    "realpy.core.display(mt)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "bd0a27d3-020d-4118-93d4-7edc83dd0176",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The proof is complete.\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Statement</th>\n",
       "      <th>Block ID</th>\n",
       "      <th>Rule</th>\n",
       "      <th>Lines</th>\n",
       "      <th>Blocks</th>\n",
       "      <th>Status</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>Line</th>\n",
       "      <td>(Implies(A, B)) &amp; (Implies(B, A))</td>\n",
       "      <td>1</td>\n",
       "      <td>Goal</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>A</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>B</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>A</td>\n",
       "      <td>11</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>B</td>\n",
       "      <td>11</td>\n",
       "      <td>Reit</td>\n",
       "      <td>2</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>Implies(A, B)</td>\n",
       "      <td>1</td>\n",
       "      <td>ImpIntro</td>\n",
       "      <td></td>\n",
       "      <td>11</td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>B</td>\n",
       "      <td>12</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>A</td>\n",
       "      <td>12</td>\n",
       "      <td>Reit</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>Implies(B, A)</td>\n",
       "      <td>1</td>\n",
       "      <td>ImpIntro</td>\n",
       "      <td></td>\n",
       "      <td>12</td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>(Implies(A, B)) &amp; (Implies(B, A))</td>\n",
       "      <td>1</td>\n",
       "      <td>ConjIntro</td>\n",
       "      <td>8, 5</td>\n",
       "      <td></td>\n",
       "      <td>Complete</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "                              Statement Block ID        Rule Lines Blocks  \\\n",
       "Line  (Implies(A, B)) & (Implies(B, A))        1        Goal                \n",
       "1                                     A        1     Premise                \n",
       "2                                     B        1     Premise                \n",
       "3                                     A       11  Assumption                \n",
       "4                                     B       11        Reit     2          \n",
       "5                         Implies(A, B)        1    ImpIntro           11   \n",
       "6                                     B       12  Assumption                \n",
       "7                                     A       12        Reit     1          \n",
       "8                         Implies(B, A)        1    ImpIntro           12   \n",
       "9     (Implies(A, B)) & (Implies(B, A))        1   ConjIntro  8, 5          \n",
       "\n",
       "        Status  \n",
       "Line            \n",
       "1               \n",
       "2               \n",
       "3               \n",
       "4               \n",
       "5               \n",
       "6               \n",
       "7               \n",
       "8               \n",
       "9     Complete  "
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "t = realpy.tf.Proof([A, B], (A >> B) & (B >> A), 'Biconditional Introduction Test')\n",
    "t.openblock(A)\n",
    "t.reit(2)\n",
    "t.closeblock()\n",
    "t.impintro('11')\n",
    "t.openblock(B)\n",
    "t.reit(1)\n",
    "t.closeblock()\n",
    "t.impintro('12')\n",
    "t.conjintro(8,5)\n",
    "realpy.core.display(t)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "f907017f-a2f4-4230-aef9-41baa1c9c412",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The proof is complete.\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Statement</th>\n",
       "      <th>Block ID</th>\n",
       "      <th>Rule</th>\n",
       "      <th>Lines</th>\n",
       "      <th>Blocks</th>\n",
       "      <th>Status</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>Line</th>\n",
       "      <td>Implies(A, B)</td>\n",
       "      <td>1</td>\n",
       "      <td>Goal</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>(Implies(A, B)) &amp; (Implies(B, A))</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>Implies(A, B)</td>\n",
       "      <td>1</td>\n",
       "      <td>BiCondElim</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td>Complete</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "                              Statement Block ID        Rule Lines Blocks  \\\n",
       "Line                      Implies(A, B)        1        Goal                \n",
       "1     (Implies(A, B)) & (Implies(B, A))        1     Premise                \n",
       "2                         Implies(A, B)        1  BiCondElim     1          \n",
       "\n",
       "        Status  \n",
       "Line            \n",
       "1               \n",
       "2     Complete  "
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "s = realpy.tf.Proof([(A >> B) & (B >> A)],A >> B,'Biconditional Elimination Test')\n",
    "s.bicondelim(1)\n",
    "realpy.core.display(s)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "945dc6d0-49fe-4253-acb7-9a8407797f59",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The proof is complete.\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Statement</th>\n",
       "      <th>Block ID</th>\n",
       "      <th>Rule</th>\n",
       "      <th>Lines</th>\n",
       "      <th>Blocks</th>\n",
       "      <th>Status</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>Line</th>\n",
       "      <td>(A &amp; B) | (A &amp; C)</td>\n",
       "      <td>1</td>\n",
       "      <td>Goal</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>A &amp; (B | C)</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>A</td>\n",
       "      <td>1</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>B | C</td>\n",
       "      <td>1</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>B</td>\n",
       "      <td>11</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>A &amp; B</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjIntro</td>\n",
       "      <td>2, 4</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>(A &amp; B) | (A &amp; C)</td>\n",
       "      <td>11</td>\n",
       "      <td>DisjIntro</td>\n",
       "      <td>5</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>C</td>\n",
       "      <td>12</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>A &amp; C</td>\n",
       "      <td>12</td>\n",
       "      <td>ConjIntro</td>\n",
       "      <td>2, 7</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>(A &amp; B) | (A &amp; C)</td>\n",
       "      <td>12</td>\n",
       "      <td>DisjIntro</td>\n",
       "      <td>8</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>(A &amp; B) | (A &amp; C)</td>\n",
       "      <td>1</td>\n",
       "      <td>DisjElim</td>\n",
       "      <td></td>\n",
       "      <td>[11, 12]</td>\n",
       "      <td>Complete</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "              Statement Block ID        Rule Lines    Blocks    Status\n",
       "Line  (A & B) | (A & C)        1        Goal                          \n",
       "1           A & (B | C)        1     Premise                          \n",
       "2                     A        1    ConjElim     1                    \n",
       "3                 B | C        1    ConjElim     1                    \n",
       "4                     B       11  Assumption                          \n",
       "5                 A & B       11   ConjIntro  2, 4                    \n",
       "6     (A & B) | (A & C)       11   DisjIntro     5                    \n",
       "7                     C       12  Assumption                          \n",
       "8                 A & C       12   ConjIntro  2, 7                    \n",
       "9     (A & B) | (A & C)       12   DisjIntro     8                    \n",
       "10    (A & B) | (A & C)        1    DisjElim        [11, 12]  Complete"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "r = realpy.tf.Proof([A & (B | C)], (A & B) | (A & C),'Trial')\n",
    "r.conjelim(1)\n",
    "r.openblock(B)\n",
    "r.conjintro(2,4)\n",
    "r.disjintro(A & C, 5)\n",
    "r.closeblock()\n",
    "r.openblock(C)\n",
    "r.conjintro(2,7)\n",
    "r.disjintro(A & B, 8)\n",
    "r.closeblock()\n",
    "r.disjelim(3, ['11','12'])\n",
    "realpy.core.display(r)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "7f045a22-3ada-4d06-9d2b-77afa508d7bc",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Statement</th>\n",
       "      <th>Block ID</th>\n",
       "      <th>Rule</th>\n",
       "      <th>Lines</th>\n",
       "      <th>Blocks</th>\n",
       "      <th>Status</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>Line</th>\n",
       "      <td>B</td>\n",
       "      <td>1</td>\n",
       "      <td>Goal</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>A</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>Implies(A, B)</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>A</td>\n",
       "      <td>1</td>\n",
       "      <td>Reit</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>A &amp; (Implies(A, B))</td>\n",
       "      <td>1</td>\n",
       "      <td>ConjIntro</td>\n",
       "      <td>1, 2</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>A</td>\n",
       "      <td>1</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>4</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>Implies(A, B)</td>\n",
       "      <td>1</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>4</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>A | C</td>\n",
       "      <td>1</td>\n",
       "      <td>DisjIntro</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>B &amp; C</td>\n",
       "      <td>11</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>B</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>8</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>C</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>8</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>11</th>\n",
       "      <td>A &amp; B &amp; C</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjIntro</td>\n",
       "      <td>1, 8</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>A</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>11</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>13</th>\n",
       "      <td>B</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>11</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>14</th>\n",
       "      <td>C</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>11</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>Implies(B &amp; C, C)</td>\n",
       "      <td>1</td>\n",
       "      <td>ImpIntro</td>\n",
       "      <td></td>\n",
       "      <td>11</td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>16</th>\n",
       "      <td>C</td>\n",
       "      <td>12</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "                Statement Block ID        Rule Lines Blocks Status\n",
       "Line                    B        1        Goal                    \n",
       "1                       A        1     Premise                    \n",
       "2           Implies(A, B)        1     Premise                    \n",
       "3                       A        1        Reit     1              \n",
       "4     A & (Implies(A, B))        1   ConjIntro  1, 2              \n",
       "5                       A        1    ConjElim     4              \n",
       "6           Implies(A, B)        1    ConjElim     4              \n",
       "7                   A | C        1   DisjIntro     1              \n",
       "8                   B & C       11  Assumption                    \n",
       "9                       B       11    ConjElim     8              \n",
       "10                      C       11    ConjElim     8              \n",
       "11              A & B & C       11   ConjIntro  1, 8              \n",
       "12                      A       11    ConjElim    11              \n",
       "13                      B       11    ConjElim    11              \n",
       "14                      C       11    ConjElim    11              \n",
       "15      Implies(B & C, C)        1    ImpIntro           11       \n",
       "16                      C       12  Assumption                    "
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "p = realpy.tf.Proof([A, A >> B], B, 'First Proof')\n",
    "p.reit(1)\n",
    "p.conjintro(1,2)\n",
    "p.conjelim(4)\n",
    "p.disjintro(C,1)\n",
    "p.opensubproof(And(C, B))\n",
    "p.conjelim(8)\n",
    "p.conjintro(1,8)\n",
    "p.conjelim(11)\n",
    "p.closesubproof()\n",
    "p.impintro('11')\n",
    "#p.impelim(1,6)\n",
    "#p.assumption(~A)\n",
    "#p.negintro(3,17)\n",
    "\n",
    "p.opensubproof(C)\n",
    "realpy.core.display(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "83e266eb-ce2b-46ff-bc3d-56c664ebe36e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Name: First Proof\n",
      "Goal: B\n",
      "Premises\n",
      "   A\n",
      "   Implies(A, B)\n",
      "Completed: No\n",
      "Lines: 16\n",
      "Subproofs: 2\n"
     ]
    }
   ],
   "source": [
    "realpy.core.metadata(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "5e8bffd4-7e16-4ff7-baec-cbc7a6ba0ac4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[['11', [8, 14]], ['12', [16]]]\n"
     ]
    }
   ],
   "source": [
    "print(p.subproofs)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "ded321c7-073d-4450-8ef1-2e6b099f7a5a",
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The proof is complete.\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Statement</th>\n",
       "      <th>Block ID</th>\n",
       "      <th>Rule</th>\n",
       "      <th>Lines</th>\n",
       "      <th>Blocks</th>\n",
       "      <th>Status</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>Line</th>\n",
       "      <td>~(A &amp; ~A)</td>\n",
       "      <td>1</td>\n",
       "      <td>Goal</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>A &amp; ~A</td>\n",
       "      <td>11</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>A</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>~A</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>False</td>\n",
       "      <td>11</td>\n",
       "      <td>NegElim</td>\n",
       "      <td>2, 3</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>~(A &amp; ~A)</td>\n",
       "      <td>1</td>\n",
       "      <td>NegIntro</td>\n",
       "      <td></td>\n",
       "      <td>11</td>\n",
       "      <td>Complete</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "      Statement Block ID        Rule Lines Blocks    Status\n",
       "Line  ~(A & ~A)        1        Goal                       \n",
       "1        A & ~A       11  Assumption                       \n",
       "2             A       11    ConjElim     1                 \n",
       "3            ~A       11    ConjElim     1                 \n",
       "4         False       11     NegElim  2, 3                 \n",
       "5     ~(A & ~A)        1    NegIntro           11  Complete"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "q=realpy.tf.Proof([], ~(A & ~A), 'Negation')\n",
    "q.opensubproof(A & ~A)\n",
    "q.conjelim(1)\n",
    "q.negelim(2,3)\n",
    "q.closesubproof()\n",
    "q.negintro('11')\n",
    "realpy.core.display(q)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "029691c5-6aca-4379-9050-1e0a40fffb55",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "([1, 2], [['11', [8, 14]], ['12', [16]]])"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "p.subproofcounts, p.subproofs"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "749f7f5c-4044-4ca5-b3df-de314f24c60f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAADAAAAAQCAYAAABQrvyxAAAACXBIWXMAAA7EAAAOxAGVKw4bAAAB4klEQVRIDb2W7VECQQyGD4cCGEvADnTs4OxAtAKlBMd//HOwA6EE7AA6QCiBDmToAN9nJ1n2jmNGGfcyk8tekt0km4+7zn6/L3LBaDQqdXZfdJLLxkWug+3cniiYDXIHkM1xP7jrC6WZm3q291vRJ2Ff+Gi8pXQ+bZ2dJP5cydgqLUOTTUUHaQbGYryD2rAUToWl3l9ECW4sbBNezZe5jNZtP4h3jzMhA1Lk5lOlnSmQBeBSmMoDM9dD/lzrbC4RuBNuw+rwgLfg1UvoS5s2B3lxo/VaPAIpRAeJ7Ggp+YeYTJw6EDj7h3WB3jn/1Lkbyda2h9t+q+3HVuB5BlzZ9Zo2ueyInnCwEJ80M0Ypy1+D9P3icJTyjWNYMrIDL2Qg7QHxwm35ptiw2tQDg0K7DzIUK8FM499O/oRL75pjMzFpYqIi3SikJUVD0cxtA1Mw9QP7sf55IQNEBG4tmErDiIfMG0rLVqHivPmCP0ymAF09uXVqDEEhpaFwLqQxV0ICi+WETotA1pn3TMBvId8EINQ/i07mf6GzmhjHmsACKUWZkgGOmtgF/0SZJuCfAWeFVEAArRkifK8qI5USygYyGlN9hhGyRxk78Gcw0ZmVcs5aQm75HCpHCYAPITdP7c+aLuQHuSioeUeu1ZIAAAAASUVORK5CYII=",
      "text/latex": [
       "$\\displaystyle x + y$"
      ],
      "text/plain": [
       "x + y"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "f2 = f.subs(A, x)\n",
    "f2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "8caee6a7-12a2-4181-90cd-fb5f5dcf8461",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle x^{2}$"
      ],
      "text/plain": [
       "x**2"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import symbols\n",
    "x, y, z A, B, C = symbols('x y A B')\n",
    "r = x**2\n",
    "r"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "id": "657a9eda-e6e4-4d08-aafc-54362a59f274",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(A + B\\right)^{2}$"
      ],
      "text/plain": [
       "(A + B)**2"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "r2 = r.subs(x,A + B)\n",
    "r2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "50e5b2f6-1399-4a97-bd82-7eb81722adce",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle y \\vee z$"
      ],
      "text/plain": [
       "y | z"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "r3 = z | y\n",
    "r3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "654aff9d-995b-472a-b320-00dc8c78d3aa",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'2,23'"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "s = ''.join([str(2),',',str(23)])\n",
    "s"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "a4877452-b6e5-4f68-9c71-3fddfb80efc0",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 \n"
     ]
    }
   ],
   "source": [
    "nums = [str(n)+' ' for n in range(20)]\n",
    "print(\"\".join(nums))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "f7bae193-412b-47a9-ae63-92d6dcaf5a91",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Name: First Proof\n",
      "Goal: B\n",
      "Premises\n",
      "   A\n",
      "   Implies(A, B)\n",
      "Completed: No\n",
      "Lines: 16\n",
      "Subproofs: 2\n"
     ]
    }
   ],
   "source": [
    "metadata(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "61eaf60a-60bf-4e1d-8c7a-8b4415dbb0e5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Statement</th>\n",
       "      <th>Block ID</th>\n",
       "      <th>Rule</th>\n",
       "      <th>Lines</th>\n",
       "      <th>Blocks</th>\n",
       "      <th>Status</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>Line</th>\n",
       "      <td>B</td>\n",
       "      <td>1</td>\n",
       "      <td>Goal</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>A</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>Implies(A, B)</td>\n",
       "      <td>1</td>\n",
       "      <td>Premise</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>A</td>\n",
       "      <td>1</td>\n",
       "      <td>Reit</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>A &amp; (Implies(A, B))</td>\n",
       "      <td>1</td>\n",
       "      <td>ConjIntro</td>\n",
       "      <td>1, 2</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>A</td>\n",
       "      <td>1</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>4</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>Implies(A, B)</td>\n",
       "      <td>1</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>4</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>A | C</td>\n",
       "      <td>1</td>\n",
       "      <td>DisjIntro</td>\n",
       "      <td>1</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>B &amp; C</td>\n",
       "      <td>11</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>B</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>8</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>C</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>8</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>11</th>\n",
       "      <td>A &amp; B &amp; C</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjIntro</td>\n",
       "      <td>1, 8</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>A</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>11</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>13</th>\n",
       "      <td>B</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>11</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>14</th>\n",
       "      <td>C</td>\n",
       "      <td>11</td>\n",
       "      <td>ConjElim</td>\n",
       "      <td>11</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>Implies(B &amp; C, C)</td>\n",
       "      <td>1</td>\n",
       "      <td>ImpIntro</td>\n",
       "      <td></td>\n",
       "      <td>11</td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>16</th>\n",
       "      <td>C</td>\n",
       "      <td>12</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "                Statement Block ID        Rule Lines Blocks Status\n",
       "Line                    B        1        Goal                    \n",
       "1                       A        1     Premise                    \n",
       "2           Implies(A, B)        1     Premise                    \n",
       "3                       A        1        Reit     1              \n",
       "4     A & (Implies(A, B))        1   ConjIntro  1, 2              \n",
       "5                       A        1    ConjElim     4              \n",
       "6           Implies(A, B)        1    ConjElim     4              \n",
       "7                   A | C        1   DisjIntro     1              \n",
       "8                   B & C       11  Assumption                    \n",
       "9                       B       11    ConjElim     8              \n",
       "10                      C       11    ConjElim     8              \n",
       "11              A & B & C       11   ConjIntro  1, 8              \n",
       "12                      A       11    ConjElim    11              \n",
       "13                      B       11    ConjElim    11              \n",
       "14                      C       11    ConjElim    11              \n",
       "15      Implies(B & C, C)        1    ImpIntro           11       \n",
       "16                      C       12  Assumption                    "
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "display(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "f24ac97d-759d-47e2-8ec3-9aa235b93068",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Implies"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "r = A >> B\n",
    "type(r)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "1f83e8ab-9a45-4c6a-bc52-e293f37dcdb4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Statement</th>\n",
       "      <th>Block ID</th>\n",
       "      <th>Rule</th>\n",
       "      <th>Lines</th>\n",
       "      <th>Blocks</th>\n",
       "      <th>Status</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>Line</th>\n",
       "      <td>Implies(Implies(Implies(P, Q), P), P)</td>\n",
       "      <td>1</td>\n",
       "      <td>Goal</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "                                  Statement Block ID  Rule Lines Blocks Status\n",
       "Line  Implies(Implies(Implies(P, Q), P), P)        1  Goal                    "
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.abc import P, Q\n",
    "peirce = realpy.tf.Proof([],((P >> Q) >> P) >>P, \"Peirce's Law\")\n",
    "realpy.core.display(peirce)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "231f2161-971a-4344-bbd8-740b36f2dba5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Statement</th>\n",
       "      <th>Block ID</th>\n",
       "      <th>Rule</th>\n",
       "      <th>Lines</th>\n",
       "      <th>Blocks</th>\n",
       "      <th>Status</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>Line</th>\n",
       "      <td>Implies(Implies(Implies(P, Q), P), P)</td>\n",
       "      <td>1</td>\n",
       "      <td>Goal</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>Implies(Implies(P, Q), P)</td>\n",
       "      <td>11</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>~P</td>\n",
       "      <td>111</td>\n",
       "      <td>Assumption</td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "      <td></td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "                                  Statement Block ID        Rule Lines Blocks  \\\n",
       "Line  Implies(Implies(Implies(P, Q), P), P)        1        Goal                \n",
       "1                 Implies(Implies(P, Q), P)       11  Assumption                \n",
       "2                                        ~P      111  Assumption                \n",
       "\n",
       "     Status  \n",
       "Line         \n",
       "1            \n",
       "2            "
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.abc import P, Q\n",
    "peirce = realpy.tf.Proof([],((P >> Q) >> P) >>P, \"Peirce's Law\")\n",
    "peirce.openblock((P >> Q) >> P)\n",
    "peirce.openblock(~P)\n",
    "realpy.core.display(peirce)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "f8150b38-11ba-4443-8ec3-478b64cdaabf",
   "metadata": {},
   "outputs": [],
   "source": [
    "from sympy import sympify"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "57f9227c-86ae-4307-a182-b180d95335ee",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle A \\vee \\neg A$"
      ],
      "text/plain": [
       "A | ~A"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "r = sympify(A | ~A, evaluate=True)\n",
    "r"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "29f461bc-8077-4977-ae47-5f514bf7e4ca",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "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.12.1"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}