{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "\n",
    "#  $\\lambda$-calcul"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from lambda_calcul import Lambda_terme"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "lines_to_next_cell": 0
   },
   "source": [
    "Voici la grammaire du langage décrivant les $\\lambda$-termes\n",
    "\n",
    "    term ::= VAR | LAMBDA VAR POINT term | LPAR term term RPAR\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## La classe `Lambda_terme`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = Lambda_terme(\"x\")\n",
    "T2 = Lambda_terme(\"(x x)\")\n",
    "T3 = Lambda_terme(\"!x.x\")\n",
    "T4 = Lambda_terme('!x.(x x)')\n",
    "T5 = Lambda_terme('(!x.(x y) z)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x\n",
      "(x x)\n",
      "λx.x\n",
      "λx.(x x)\n",
      "(λx.(x y) z)\n"
     ]
    }
   ],
   "source": [
    "print(T1)\n",
    "print(T2)\n",
    "print(T3)\n",
    "print(T4)\n",
    "print(T5)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "termes = (T1, T2, T3, T4, T5)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, False, False, False, False)"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_variable() for t in termes)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, False, True, True, False)"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_abstraction() for t in termes)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, True, False, False, True)"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_application() for t in termes)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, False, False, False, True)"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_redex() for t in termes)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, True, True, True, False)"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.est_forme_normale() for t in termes)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "({'x'}, {'x'}, set(), set(), {'y', 'z'})"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tuple(t.variables_libres() for t in termes)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x --> x\n",
      "x --> (y x)\n"
     ]
    }
   ],
   "source": [
    "print(T1, '-->', T1.subs('y', Lambda_terme('(y x)')))\n",
    "print(T1, '-->', T1.subs('x', Lambda_terme('(y x)')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.y --> λx.y\n",
      "λx.y --> λx.(t z)\n",
      "λx.y --> λx0.(x z)\n"
     ]
    }
   ],
   "source": [
    "T5 = Lambda_terme('!x.y')\n",
    "print(T5, '-->', T5.subs('x', Lambda_terme('(y z)')))\n",
    "print(T5, '-->', T5.subs('y', Lambda_terme('(t z)')))\n",
    "print(T5, '-->', T5.subs('y', Lambda_terme('(x z)')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.x --> λx.x\n",
      "λx.x --> λx.x\n"
     ]
    }
   ],
   "source": [
    "print(T3, '-->', T3.subs('y', Lambda_terme('(y x)')))\n",
    "print(T3, '-->', T3.subs('x', Lambda_terme('(y x)')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.x\n",
      "λy.x\n",
      "λx.(x x)\n",
      "λy.(x x)\n",
      "λx.λx.x\n",
      "λy.λx.x\n",
      "λx.λx.(x x)\n",
      "λy.λx.(x x)\n",
      "λx.(λx.(x y) z)\n",
      "λy.(λx.(x y) z)\n"
     ]
    }
   ],
   "source": [
    "for t in termes:\n",
    "    for v in ('x', 'y'):\n",
    "        print(t.abstrait(v))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(x x)\n",
      "(x (x x))\n",
      "(x λx.x)\n",
      "(x λx.(x x))\n",
      "(x (λx.(x y) z))\n",
      "((x x) x)\n",
      "((x x) (x x))\n",
      "((x x) λx.x)\n",
      "((x x) λx.(x x))\n",
      "((x x) (λx.(x y) z))\n",
      "(λx.x x)\n",
      "(λx.x (x x))\n",
      "(λx.x λx.x)\n",
      "(λx.x λx.(x x))\n",
      "(λx.x (λx.(x y) z))\n",
      "(λx.(x x) x)\n",
      "(λx.(x x) (x x))\n",
      "(λx.(x x) λx.x)\n",
      "(λx.(x x) λx.(x x))\n",
      "(λx.(x x) (λx.(x y) z))\n",
      "((λx.(x y) z) x)\n",
      "((λx.(x y) z) (x x))\n",
      "((λx.(x y) z) λx.x)\n",
      "((λx.(x y) z) λx.(x x))\n",
      "((λx.(x y) z) (λx.(x y) z))\n"
     ]
    }
   ],
   "source": [
    "for t1 in termes:\n",
    "    for t2 in termes:\n",
    "        print(t1.applique(t2))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [],
   "source": [
    "OMEGA = Lambda_terme('(!x.(x x) !x.(x x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λx.(x x) λx.(x x))\n"
     ]
    }
   ],
   "source": [
    "print(OMEGA)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OMEGA.est_redex()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OMEGA.est_forme_normale()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OMEGA.variables_libres()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λx.(x x) λx.(x x))\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "res, est_red = OMEGA.reduit()\n",
    "print(res)\n",
    "print(est_red)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(eric vero) True\n"
     ]
    }
   ],
   "source": [
    "res, est_red = Lambda_terme('(!x.(eric x) vero)').reduit()\n",
    "print(res, est_red)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λx.(x x) λx.(x x))\n",
      "  1: ---> (λx.(x x) λx.(x x))\n",
      "  2: ---> (λx.(x x) λx.(x x))\n",
      "  3: ---> (λx.(x x) λx.(x x))\n",
      "  4: ---> (λx.(x x) λx.(x x))\n",
      "  5: ---> (λx.(x x) λx.(x x))\n",
      "  6: ---> (λx.(x x) λx.(x x))\n",
      "  7: ---> (λx.(x x) λx.(x x))\n",
      "  8: ---> (λx.(x x) λx.(x x))\n",
      "  9: ---> (λx.(x x) λx.(x x))\n",
      " 10: ---> (λx.(x x) λx.(x x))\n",
      "Pas de forme normale atteinte après 10 étapes de réduction\n"
     ]
    }
   ],
   "source": [
    "OMEGA.forme_normale(nb_etapes_max=10, verbose=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Entiers, successeurs, addition, multiplication et exponentiation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [],
   "source": [
    "ZERO = Lambda_terme('!f.!x.x')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [],
   "source": [
    "UN = Lambda_terme('!f.!x.(f x)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [],
   "source": [
    "DEUX = Lambda_terme('!f.!x.(f (f x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [],
   "source": [
    "SUC = Lambda_terme('!n.!f.!x.(f ((n f) x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x)))\n",
      "  1: ---> (λn.λf.λx.(f ((n f) x)) λf.λx.(f (f x)))\n",
      "  2: ---> λf.λx.(f ((λf.λx.(f (f x)) f) x))\n",
      "  3: ---> λf.λx.(f (λx.(f (f x)) x))\n",
      "  4: ---> λf.λx.(f (f (f x)))\n",
      "Forme normale calculée : λf.λx.(f (f (f x)))\n"
     ]
    }
   ],
   "source": [
    "TROIS = SUC.applique(DEUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) λf.λx.x)\n",
      "  1: ---> ((λf.λx.(f (f (f x))) λn.λf.λx.(f ((n f) x))) λf.λx.x)\n",
      "  2: ---> (λx.(λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) x))) λf.λx.x)\n",
      "  3: ---> (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.x)))\n",
      "  4: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λn.λf.λx.(f ((n f) x)) λf.λx.x)) f) x))\n",
      "  5: ---> λf.λx.(f ((λf.λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.x) f) x)) f) x))\n",
      "  6: ---> λf.λx.(f (λx.(f (((λn.λf.λx.(f ((n f) x)) λf.λx.x) f) x)) x))\n",
      "  7: ---> λf.λx.(f (f (((λn.λf.λx.(f ((n f) x)) λf.λx.x) f) x)))\n",
      "  8: ---> λf.λx.(f (f ((λf.λx.(f ((λf.λx.x f) x)) f) x)))\n",
      "  9: ---> λf.λx.(f (f (λx.(f ((λf.λx.x f) x)) x)))\n",
      " 10: ---> λf.λx.(f (f (f ((λf.λx.x f) x))))\n",
      " 11: ---> λf.λx.(f (f (f (λx.x x))))\n",
      " 12: ---> λf.λx.(f (f (f x)))\n",
      "Forme normale calculée : λf.λx.(f (f (f x)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed71d9b7f0>"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "TROIS.applique(SUC).applique(ZERO).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [],
   "source": [
    "ADD = Lambda_terme('!n.!m.!f.!x.((n f) ((m f) x))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f x)) λf.λx.(f (f (f x))))\n",
      "  1: ---> ((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f x)) λf.λx.(f (f (f x))))\n",
      "  2: ---> (λm.λf.λx.((λf.λx.(f x) f) ((m f) x)) λf.λx.(f (f (f x))))\n",
      "  3: ---> λf.λx.((λf.λx.(f x) f) ((λf.λx.(f (f (f x))) f) x))\n",
      "  4: ---> λf.λx.(λx.(f x) ((λf.λx.(f (f (f x))) f) x))\n",
      "  5: ---> λf.λx.(f ((λf.λx.(f (f (f x))) f) x))\n",
      "  6: ---> λf.λx.(f (λx.(f (f (f x))) x))\n",
      "  7: ---> λf.λx.(f (f (f (f x))))\n",
      "Forme normale calculée : λf.λx.(f (f (f (f x))))\n"
     ]
    }
   ],
   "source": [
    "QUATRE = ADD.applique(UN).applique(TROIS).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
      "  1: ---> ((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
      "  2: ---> (λm.λf.λx.((λf.λx.(f (f (f x))) f) ((m f) x)) λf.λx.(f (f x)))\n",
      "  3: ---> λf.λx.((λf.λx.(f (f (f x))) f) ((λf.λx.(f (f x)) f) x))\n",
      "  4: ---> λf.λx.(λx.(f (f (f x))) ((λf.λx.(f (f x)) f) x))\n",
      "  5: ---> λf.λx.(f (f (f ((λf.λx.(f (f x)) f) x))))\n",
      "  6: ---> λf.λx.(f (f (f (λx.(f (f x)) x))))\n",
      "  7: ---> λf.λx.(f (f (f (f (f x)))))\n",
      "Forme normale calculée : λf.λx.(f (f (f (f (f x)))))\n"
     ]
    }
   ],
   "source": [
    "CINQ = ADD.applique(TROIS).applique(DEUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f (f (f (f x))))) λf.λx.(f (f (f x))))\n",
      "  1: ---> ((λn.λm.λf.λx.((n f) ((m f) x)) λf.λx.(f (f (f (f x))))) λf.λx.(f (f (f x))))\n",
      "  2: ---> (λm.λf.λx.((λf.λx.(f (f (f (f x)))) f) ((m f) x)) λf.λx.(f (f (f x))))\n",
      "  3: ---> λf.λx.((λf.λx.(f (f (f (f x)))) f) ((λf.λx.(f (f (f x))) f) x))\n",
      "  4: ---> λf.λx.(λx.(f (f (f (f x)))) ((λf.λx.(f (f (f x))) f) x))\n",
      "  5: ---> λf.λx.(f (f (f (f ((λf.λx.(f (f (f x))) f) x)))))\n",
      "  6: ---> λf.λx.(f (f (f (f (λx.(f (f (f x))) x)))))\n",
      "  7: ---> λf.λx.(f (f (f (f (f (f (f x)))))))\n",
      "Forme normale calculée : λf.λx.(f (f (f (f (f (f (f x)))))))\n"
     ]
    }
   ],
   "source": [
    "SEPT = ADD.applique(QUATRE).applique(TROIS).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [],
   "source": [
    "MUL = Lambda_terme('!n.!m.!f.(n (m f))')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.λf.(n (m f)) λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
      "  1: ---> ((λn.λm.λf.(n (m f)) λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
      "  2: ---> (λm.λf.(λf.λx.(f (f x)) (m f)) λf.λx.(f (f (f x))))\n",
      "  3: ---> λf.(λf.λx.(f (f x)) (λf.λx.(f (f (f x))) f))\n",
      "  4: ---> λf.λx.((λf.λx.(f (f (f x))) f) ((λf.λx.(f (f (f x))) f) x))\n",
      "  5: ---> λf.λx.(λx.(f (f (f x))) ((λf.λx.(f (f (f x))) f) x))\n",
      "  6: ---> λf.λx.(f (f (f ((λf.λx.(f (f (f x))) f) x))))\n",
      "  7: ---> λf.λx.(f (f (f (λx.(f (f (f x))) x))))\n",
      "  8: ---> λf.λx.(f (f (f (f (f (f x))))))\n",
      "Forme normale calculée : λf.λx.(f (f (f (f (f (f x))))))\n"
     ]
    }
   ],
   "source": [
    "SIX = MUL.applique(DEUX).applique(TROIS).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [],
   "source": [
    "EXP = Lambda_terme('!n.!m.(m n)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.(m n) λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
      "  1: ---> ((λn.λm.(m n) λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
      "  2: ---> (λm.(m λf.λx.(f (f x))) λf.λx.(f (f (f x))))\n",
      "  3: ---> (λf.λx.(f (f (f x))) λf.λx.(f (f x)))\n",
      "  4: ---> λx.(λf.λx.(f (f x)) (λf.λx.(f (f x)) (λf.λx.(f (f x)) x)))\n",
      "  5: ---> λx.λx0.((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))\n",
      "  6: ---> λx.λx0.(λx0.((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) x0)) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))\n",
      "  7: ---> λx.λx0.((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0)))\n",
      "  8: ---> λx.λx0.(λx0.(x (x x0)) ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0)))\n",
      "  9: ---> λx.λx0.(x (x ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))))\n",
      " 10: ---> λx.λx0.(x (x (λx0.(x (x x0)) ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0))))\n",
      " 11: ---> λx.λx0.(x (x (x (x ((λf.λx.(f (f x)) (λf.λx.(f (f x)) x)) x0)))))\n",
      " 12: ---> λx.λx0.(x (x (x (x (λx0.((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) x0)) x0)))))\n",
      " 13: ---> λx.λx0.(x (x (x (x ((λf.λx.(f (f x)) x) ((λf.λx.(f (f x)) x) x0))))))\n",
      " 14: ---> λx.λx0.(x (x (x (x (λx0.(x (x x0)) ((λf.λx.(f (f x)) x) x0))))))\n",
      " 15: ---> λx.λx0.(x (x (x (x (x (x ((λf.λx.(f (f x)) x) x0)))))))\n",
      " 16: ---> λx.λx0.(x (x (x (x (x (x (λx0.(x (x x0)) x0)))))))\n",
      " 17: ---> λx.λx0.(x (x (x (x (x (x (x (x x0))))))))\n",
      "Forme normale calculée : λx.λx0.(x (x (x (x (x (x (x (x x0))))))))\n"
     ]
    }
   ],
   "source": [
    "HUIT = EXP.applique(DEUX).applique(TROIS).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.(m n) λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
      "  1: ---> ((λn.λm.(m n) λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
      "  2: ---> (λm.(m λf.λx.(f (f (f x)))) λf.λx.(f (f x)))\n",
      "  3: ---> (λf.λx.(f (f x)) λf.λx.(f (f (f x))))\n",
      "  4: ---> λx.(λf.λx.(f (f (f x))) (λf.λx.(f (f (f x))) x))\n",
      "  5: ---> λx.λx0.((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) x0)))\n",
      "  6: ---> λx.λx0.(λx0.(x (x (x x0))) ((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) x0)))\n",
      "  7: ---> λx.λx0.(x (x (x ((λf.λx.(f (f (f x))) x) ((λf.λx.(f (f (f x))) x) x0)))))\n",
      "  8: ---> λx.λx0.(x (x (x (λx0.(x (x (x x0))) ((λf.λx.(f (f (f x))) x) x0)))))\n",
      "  9: ---> λx.λx0.(x (x (x (x (x (x ((λf.λx.(f (f (f x))) x) x0)))))))\n",
      " 10: ---> λx.λx0.(x (x (x (x (x (x (λx0.(x (x (x x0))) x0)))))))\n",
      " 11: ---> λx.λx0.(x (x (x (x (x (x (x (x (x x0)))))))))\n",
      "Forme normale calculée : λx.λx0.(x (x (x (x (x (x (x (x (x x0)))))))))\n"
     ]
    }
   ],
   "source": [
    "NEUF = EXP.applique(TROIS).applique(DEUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Booléens, opérateurs logiques et conditionnelles"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [],
   "source": [
    "VRAI = Lambda_terme('!x.!y.x')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [],
   "source": [
    "FAUX = Lambda_terme('!x.!y.y')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [],
   "source": [
    "COND = Lambda_terme('!c.!a.!s.((c a) s)') "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(((λc.λa.λs.((c a) s) λx.λy.x) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  1: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  2: ---> ((λa.λs.((λx.λy.x a) s) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  3: ---> (λs.((λx.λy.x λf.λx.(f x)) s) λf.λx.(f (f x)))\n",
      "  4: ---> ((λx.λy.x λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  5: ---> (λy.λf.λx.(f x) λf.λx.(f (f x)))\n",
      "  6: ---> λf.λx.(f x)\n",
      "Forme normale calculée : λf.λx.(f x)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed720bf438>"
      ]
     },
     "execution_count": 43,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "COND.applique(VRAI).applique(UN).applique(DEUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(((λc.λa.λs.((c a) s) λx.λy.y) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  1: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  2: ---> ((λa.λs.((λx.λy.y a) s) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  3: ---> (λs.((λx.λy.y λf.λx.(f x)) s) λf.λx.(f (f x)))\n",
      "  4: ---> ((λx.λy.y λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  5: ---> (λy.y λf.λx.(f (f x)))\n",
      "  6: ---> λf.λx.(f (f x))\n",
      "Forme normale calculée : λf.λx.(f (f x))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed720bf748>"
      ]
     },
     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "COND.applique(FAUX).applique(UN).applique(DEUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [],
   "source": [
    "ET = COND.applique(Lambda_terme('a')).applique(Lambda_terme('b')).applique(FAUX).abstrait('b').abstrait('a')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y)\n"
     ]
    }
   ],
   "source": [
    "print(ET)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.x) λx.λy.x)\n",
      "  1: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.x) λx.λy.x)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) b) λx.λy.y) λx.λy.x)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.x) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.x λx.λy.x) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.x λx.λy.x) λx.λy.y)\n",
      "  7: ---> (λy.λx.λy.x λx.λy.y)\n",
      "  8: ---> λx.λy.x\n",
      "Forme normale calculée : λx.λy.x\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72488c88>"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ET.applique(VRAI).applique(VRAI).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  1: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) b) λx.λy.y) λx.λy.y)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.y) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.y) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.x λx.λy.y) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.x λx.λy.y) λx.λy.y)\n",
      "  7: ---> (λy.λx.λy.y λx.λy.y)\n",
      "  8: ---> λx.λy.y\n",
      "Forme normale calculée : λx.λy.y\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72397b38>"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ET.applique(VRAI).applique(FAUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.y) λx.λy.x)\n",
      "  1: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.y) λx.λy.x)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) b) λx.λy.y) λx.λy.x)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.x) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.y λx.λy.x) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.y λx.λy.x) λx.λy.y)\n",
      "  7: ---> (λy.y λx.λy.y)\n",
      "  8: ---> λx.λy.y\n",
      "Forme normale calculée : λx.λy.y\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72397b38>"
      ]
     },
     "execution_count": 49,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ET.applique(FAUX).applique(VRAI).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.y) λx.λy.y)\n",
      "  1: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) λx.λy.y) λx.λy.y)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) b) λx.λy.y) λx.λy.y)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.y) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.y) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.y λx.λy.y) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.y λx.λy.y) λx.λy.y)\n",
      "  7: ---> (λy.y λx.λy.y)\n",
      "  8: ---> λx.λy.y\n",
      "Forme normale calculée : λx.λy.y\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72397b38>"
      ]
     },
     "execution_count": 50,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ET.applique(FAUX).applique(FAUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "metadata": {},
   "outputs": [],
   "source": [
    "OU = COND.applique(Lambda_terme('a')).applique(VRAI).applique(Lambda_terme('b')).abstrait('b').abstrait('a')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b)\n"
     ]
    }
   ],
   "source": [
    "print(OU)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.x) λx.λy.x)\n",
      "  1: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.x) λx.λy.x)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) b) λx.λy.x)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) λx.λy.x)\n",
      "  4: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.x) λx.λy.x)\n",
      "  5: ---> (λs.((λx.λy.x λx.λy.x) s) λx.λy.x)\n",
      "  6: ---> ((λx.λy.x λx.λy.x) λx.λy.x)\n",
      "  7: ---> (λy.λx.λy.x λx.λy.x)\n",
      "  8: ---> λx.λy.x\n",
      "Forme normale calculée : λx.λy.x\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72488c88>"
      ]
     },
     "execution_count": 53,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OU.applique(VRAI).applique(VRAI).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.x) λx.λy.y)\n",
      "  1: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.x) λx.λy.y)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) b) λx.λy.y)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.x) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.x) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.x λx.λy.x) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.x λx.λy.x) λx.λy.y)\n",
      "  7: ---> (λy.λx.λy.x λx.λy.y)\n",
      "  8: ---> λx.λy.x\n",
      "Forme normale calculée : λx.λy.x\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72488c88>"
      ]
     },
     "execution_count": 54,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OU.applique(VRAI).applique(FAUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.y) λx.λy.x)\n",
      "  1: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.y) λx.λy.x)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) b) λx.λy.x)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) λx.λy.x)\n",
      "  4: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.x) λx.λy.x)\n",
      "  5: ---> (λs.((λx.λy.y λx.λy.x) s) λx.λy.x)\n",
      "  6: ---> ((λx.λy.y λx.λy.x) λx.λy.x)\n",
      "  7: ---> (λy.y λx.λy.x)\n",
      "  8: ---> λx.λy.x\n",
      "Forme normale calculée : λx.λy.x\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72488c88>"
      ]
     },
     "execution_count": 55,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OU.applique(FAUX).applique(VRAI).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.y) λx.λy.y)\n",
      "  1: ---> ((λa.λb.(((λc.λa.λs.((c a) s) a) λx.λy.x) b) λx.λy.y) λx.λy.y)\n",
      "  2: ---> (λb.(((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) b) λx.λy.y)\n",
      "  3: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  4: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.x) λx.λy.y)\n",
      "  5: ---> (λs.((λx.λy.y λx.λy.x) s) λx.λy.y)\n",
      "  6: ---> ((λx.λy.y λx.λy.x) λx.λy.y)\n",
      "  7: ---> (λy.y λx.λy.y)\n",
      "  8: ---> λx.λy.y\n",
      "Forme normale calculée : λx.λy.y\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72397b38>"
      ]
     },
     "execution_count": 56,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "OU.applique(FAUX).applique(FAUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [],
   "source": [
    "NON = COND.applique(Lambda_terme('a')).applique(FAUX).applique(VRAI).abstrait('a')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x)\n"
     ]
    }
   ],
   "source": [
    "print(NON)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x) λx.λy.x)\n",
      "  1: ---> (λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x) λx.λy.x)\n",
      "  2: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λx.λy.y) λx.λy.x)\n",
      "  3: ---> ((λa.λs.((λx.λy.x a) s) λx.λy.y) λx.λy.x)\n",
      "  4: ---> (λs.((λx.λy.x λx.λy.y) s) λx.λy.x)\n",
      "  5: ---> ((λx.λy.x λx.λy.y) λx.λy.x)\n",
      "  6: ---> (λy.λx.λy.y λx.λy.x)\n",
      "  7: ---> λx.λy.y\n",
      "Forme normale calculée : λx.λy.y\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72397b38>"
      ]
     },
     "execution_count": 60,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "NON.applique(VRAI).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  1: ---> (λa.(((λc.λa.λs.((c a) s) a) λx.λy.y) λx.λy.x) λx.λy.y)\n",
      "  2: ---> (((λc.λa.λs.((c a) s) λx.λy.y) λx.λy.y) λx.λy.x)\n",
      "  3: ---> ((λa.λs.((λx.λy.y a) s) λx.λy.y) λx.λy.x)\n",
      "  4: ---> (λs.((λx.λy.y λx.λy.y) s) λx.λy.x)\n",
      "  5: ---> ((λx.λy.y λx.λy.y) λx.λy.x)\n",
      "  6: ---> (λy.y λx.λy.x)\n",
      "  7: ---> λx.λy.x\n",
      "Forme normale calculée : λx.λy.x\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72488c88>"
      ]
     },
     "execution_count": 61,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "NON.applique(FAUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 62,
   "metadata": {},
   "outputs": [],
   "source": [
    "NUL = Lambda_terme('!n.((n !x.{:s}) {:s})'.format(str(FAUX), str(VRAI)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λn.((n λx.λx.λy.y) λx.λy.x)\n"
     ]
    }
   ],
   "source": [
    "print(NUL)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.x)\n",
      "  1: ---> (λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.x)\n",
      "  2: ---> ((λf.λx.x λx.λx.λy.y) λx.λy.x)\n",
      "  3: ---> (λx.x λx.λy.x)\n",
      "  4: ---> λx.λy.x\n",
      "Forme normale calculée : λx.λy.x\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed72233cf8>"
      ]
     },
     "execution_count": 64,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "NUL.applique(ZERO).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.(f (f (f x))))\n",
      "  1: ---> (λn.((n λx.λx.λy.y) λx.λy.x) λf.λx.(f (f (f x))))\n",
      "  2: ---> ((λf.λx.(f (f (f x))) λx.λx.λy.y) λx.λy.x)\n",
      "  3: ---> (λx.(λx.λx.λy.y (λx.λx.λy.y (λx.λx.λy.y x))) λx.λy.x)\n",
      "  4: ---> (λx.λx.λy.y (λx.λx.λy.y (λx.λx.λy.y λx.λy.x)))\n",
      "  5: ---> λx.λy.y\n",
      "Forme normale calculée : λx.λy.y\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed722334e0>"
      ]
     },
     "execution_count": 65,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "NUL.applique(TROIS).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Couples"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "metadata": {},
   "outputs": [],
   "source": [
    "CONS = Lambda_terme('!x.!y.!s.((({:s} s) x) y)'.format(str(COND)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y)\n"
     ]
    }
   ],
   "source": [
    "print(CONS)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  1: ---> ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  2: ---> (λy.λs.(((λc.λa.λs.((c a) s) s) λf.λx.(f x)) y) λf.λx.(f (f x)))\n",
      "  3: ---> λs.(((λc.λa.λs.((c a) s) s) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  4: ---> λs.((λa.λs0.((s a) s0) λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  5: ---> λs.(λs0.((s λf.λx.(f x)) s0) λf.λx.(f (f x)))\n",
      "  6: ---> λs.((s λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "Forme normale calculée : λs.((s λf.λx.(f x)) λf.λx.(f (f x)))\n"
     ]
    }
   ],
   "source": [
    "UN_DEUX = CONS.applique(UN).applique(DEUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {},
   "outputs": [],
   "source": [
    "CAR = Lambda_terme('!c.(c {:s})'.format(str(VRAI)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λc.(c λx.λy.x)\n"
     ]
    }
   ],
   "source": [
    "print(CAR)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λc.(c λx.λy.x) λs.((s λf.λx.(f x)) λf.λx.(f (f x))))\n",
      "  1: ---> (λc.(c λx.λy.x) λs.((s λf.λx.(f x)) λf.λx.(f (f x))))\n",
      "  2: ---> (λs.((s λf.λx.(f x)) λf.λx.(f (f x))) λx.λy.x)\n",
      "  3: ---> ((λx.λy.x λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  4: ---> (λy.λf.λx.(f x) λf.λx.(f (f x)))\n",
      "  5: ---> λf.λx.(f x)\n",
      "Forme normale calculée : λf.λx.(f x)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed720bf438>"
      ]
     },
     "execution_count": 72,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "CAR.applique(UN_DEUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "metadata": {},
   "outputs": [],
   "source": [
    "CDR = Lambda_terme('!c.(c {:s})'.format(str(FAUX)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λc.(c λx.λy.y)\n"
     ]
    }
   ],
   "source": [
    "print(CDR)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λc.(c λx.λy.y) λs.((s λf.λx.(f x)) λf.λx.(f (f x))))\n",
      "  1: ---> (λc.(c λx.λy.y) λs.((s λf.λx.(f x)) λf.λx.(f (f x))))\n",
      "  2: ---> (λs.((s λf.λx.(f x)) λf.λx.(f (f x))) λx.λy.y)\n",
      "  3: ---> ((λx.λy.y λf.λx.(f x)) λf.λx.(f (f x)))\n",
      "  4: ---> (λy.y λf.λx.(f (f x)))\n",
      "  5: ---> λf.λx.(f (f x))\n",
      "Forme normale calculée : λf.λx.(f (f x))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed720bf748>"
      ]
     },
     "execution_count": 76,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "CDR.applique(UN_DEUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 77,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λn.(CAR ((n λc.((CONS (CDR c)) (SUC (CDR c)))) ((CONS ZERO) ZERO)))\n",
      "λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n"
     ]
    }
   ],
   "source": [
    "M_PRED = Lambda_terme('!n.(CAR ((n !c.((CONS (CDR c)) (SUC (CDR c)))) ((CONS ZERO) ZERO)))')\n",
    "print(M_PRED)\n",
    "PRED = M_PRED.subs('CAR', CAR).subs('CONS', CONS).subs('CDR', CDR).subs('SUC', SUC).subs('ZERO', ZERO)\n",
    "print(PRED)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 78,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f (f x)))\n",
      "  1: ---> (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f (f x)))\n",
      "  2: ---> (λc.(c λx.λy.x) ((λf.λx.(f (f x)) λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      "  3: ---> (((λf.λx.(f (f x)) λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  4: ---> ((λx.(λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) x)) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  5: ---> ((λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λx.λy.x)\n",
      "  6: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.x)\n",
      "  7: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.x)\n",
      "  8: ---> (λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.x)\n",
      "  9: ---> (((λc.λa.λs.((c a) s) λx.λy.x) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 10: ---> ((λa.λs.((λx.λy.x a) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 11: ---> (λs.((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 12: ---> ((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 13: ---> (λy.(λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 14: ---> (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      " 15: ---> ((λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.y)\n",
      " 16: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y)\n",
      " 17: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y)\n",
      " 18: ---> (λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y)\n",
      " 19: ---> (((λc.λa.λs.((c a) s) λx.λy.y) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 20: ---> ((λa.λs.((λx.λy.y a) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 21: ---> (λs.((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 22: ---> ((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 23: ---> (λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 24: ---> (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      " 25: ---> λf.λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) f) x))\n",
      " 26: ---> λf.λx.(f (((((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x) λx.λy.y) f) x))\n",
      " 27: ---> λf.λx.(f ((((λy.λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) y) λf.λx.x) λx.λy.y) f) x))\n",
      " 28: ---> λf.λx.(f (((λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) λf.λx.x) λx.λy.y) f) x))\n",
      " 29: ---> λf.λx.(f (((((λc.λa.λs.((c a) s) λx.λy.y) λf.λx.x) λf.λx.x) f) x))\n",
      " 30: ---> λf.λx.(f ((((λa.λs.((λx.λy.y a) s) λf.λx.x) λf.λx.x) f) x))\n",
      " 31: ---> λf.λx.(f (((λs.((λx.λy.y λf.λx.x) s) λf.λx.x) f) x))\n",
      " 32: ---> λf.λx.(f ((((λx.λy.y λf.λx.x) λf.λx.x) f) x))\n",
      " 33: ---> λf.λx.(f (((λy.y λf.λx.x) f) x))\n",
      " 34: ---> λf.λx.(f ((λf.λx.x f) x))\n",
      " 35: ---> λf.λx.(f (λx.x x))\n",
      " 36: ---> λf.λx.(f x)\n",
      "Forme normale calculée : λf.λx.(f x)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed726b20f0>"
      ]
     },
     "execution_count": 78,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "PRED.applique(DEUX).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 79,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.x)\n",
      "  1: ---> (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.x)\n",
      "  2: ---> (λc.(c λx.λy.x) ((λf.λx.x λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      "  3: ---> (((λf.λx.x λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  4: ---> ((λx.x ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  5: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x) λx.λy.x)\n",
      "  6: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) y) λf.λx.x) λx.λy.x)\n",
      "  7: ---> (λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) λf.λx.x) λx.λy.x)\n",
      "  8: ---> (((λc.λa.λs.((c a) s) λx.λy.x) λf.λx.x) λf.λx.x)\n",
      "  9: ---> ((λa.λs.((λx.λy.x a) s) λf.λx.x) λf.λx.x)\n",
      " 10: ---> (λs.((λx.λy.x λf.λx.x) s) λf.λx.x)\n",
      " 11: ---> ((λx.λy.x λf.λx.x) λf.λx.x)\n",
      " 12: ---> (λy.λf.λx.x λf.λx.x)\n",
      " 13: ---> λf.λx.x\n",
      "Forme normale calculée : λf.λx.x\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed720bf0b8>"
      ]
     },
     "execution_count": 79,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "PRED.applique(ZERO).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 80,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λn.λm.((m PRED) n)\n",
      "λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n)\n"
     ]
    }
   ],
   "source": [
    "M_SUB = Lambda_terme('!n.!m.((m PRED) n)')\n",
    "print(M_SUB)\n",
    "SUB = M_SUB.subs('PRED', PRED)\n",
    "print(SUB)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 81,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f (f (f x)))) λf.λx.(f x))\n",
      "  1: ---> ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f (f (f x)))) λf.λx.(f x))\n",
      "  2: ---> (λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f (f (f x)))) λf.λx.(f x))\n",
      "  3: ---> ((λf.λx.(f x) λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f (f (f x))))\n",
      "  4: ---> (λx.(λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) x) λf.λx.(f (f (f x))))\n",
      "  5: ---> (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f (f (f x))))\n",
      "  6: ---> (λc.(c λx.λy.x) ((λf.λx.(f (f (f x))) λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))\n",
      "  7: ---> (((λf.λx.(f (f (f x))) λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  8: ---> ((λx.(λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) x))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.x)\n",
      "  9: ---> ((λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.x)\n",
      " 10: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
      " 11: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
      " 12: ---> (λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))) λx.λy.x)\n",
      " 13: ---> (((λc.λa.λs.((c a) s) λx.λy.x) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 14: ---> ((λa.λs.((λx.λy.x a) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 15: ---> (λs.((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 16: ---> ((λx.λy.x (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 17: ---> (λy.(λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))))\n",
      " 18: ---> (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 19: ---> ((λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λx.λy.y)\n",
      " 20: ---> (((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
      " 21: ---> ((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
      " 22: ---> (λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))) λx.λy.y)\n",
      " 23: ---> (((λc.λa.λs.((c a) s) λx.λy.y) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 24: ---> ((λa.λs.((λx.λy.y a) s) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 25: ---> (λs.((λx.λy.y (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 26: ---> ((λx.λy.y (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 27: ---> (λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))))\n",
      " 28: ---> (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))))\n",
      " 29: ---> λf.λx.(f (((λc.(c λx.λy.y) (λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) f) x))\n",
      " 30: ---> λf.λx.(f ((((λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) λx.λy.y) f) x))\n",
      " 31: ---> λf.λx.(f (((((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
      " 32: ---> λf.λx.(f ((((λy.λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
      " 33: ---> λf.λx.(f (((λs.(((λc.λa.λs.((c a) s) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λx.λy.y) f) x))\n",
      " 34: ---> λf.λx.(f (((((λc.λa.λs.((c a) s) λx.λy.y) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 35: ---> λf.λx.(f ((((λa.λs.((λx.λy.y a) s) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 36: ---> λf.λx.(f (((λs.((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) s) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 37: ---> λf.λx.(f ((((λx.λy.y (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 38: ---> λf.λx.(f (((λy.y (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) f) x))\n",
      " 39: ---> λf.λx.(f (((λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) f) x))\n",
      " 40: ---> λf.λx.(f ((λf.λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) f) x)) f) x))\n",
      " 41: ---> λf.λx.(f (λx.(f (((λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) f) x)) x))\n",
      " 42: ---> λf.λx.(f (f (((λc.(c λx.λy.y) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)) f) x)))\n",
      " 43: ---> λf.λx.(f (f (((((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x) λx.λy.y) f) x)))\n",
      " 44: ---> λf.λx.(f (f ((((λy.λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) y) λf.λx.x) λx.λy.y) f) x)))\n",
      " 45: ---> λf.λx.(f (f (((λs.(((λc.λa.λs.((c a) s) s) λf.λx.x) λf.λx.x) λx.λy.y) f) x)))\n",
      " 46: ---> λf.λx.(f (f (((((λc.λa.λs.((c a) s) λx.λy.y) λf.λx.x) λf.λx.x) f) x)))\n",
      " 47: ---> λf.λx.(f (f ((((λa.λs.((λx.λy.y a) s) λf.λx.x) λf.λx.x) f) x)))\n",
      " 48: ---> λf.λx.(f (f (((λs.((λx.λy.y λf.λx.x) s) λf.λx.x) f) x)))\n",
      " 49: ---> λf.λx.(f (f ((((λx.λy.y λf.λx.x) λf.λx.x) f) x)))\n",
      " 50: ---> λf.λx.(f (f (((λy.y λf.λx.x) f) x)))\n",
      " 51: ---> λf.λx.(f (f ((λf.λx.x f) x)))\n",
      " 52: ---> λf.λx.(f (f (λx.x x)))\n",
      " 53: ---> λf.λx.(f (f x))\n",
      "Forme normale calculée : λf.λx.(f (f x))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "<lambda_calcul.Lambda_terme at 0x7fed71d9b860>"
      ]
     },
     "execution_count": 81,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "SUB.applique(TROIS).applique(UN).forme_normale(verbose=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 86,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λn.λm.(NUL ((SUB n) m))\n"
     ]
    }
   ],
   "source": [
    "M_INF = Lambda_terme('!n.!m.(NUL ((SUB n) m))')\n",
    "print(M_INF)\n",
    "INF = M_INF.subs('NUL', NUL).subs('SUB', SUB)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 87,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.λy.y\n"
     ]
    }
   ],
   "source": [
    "print(INF.applique(TROIS).applique(UN).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 88,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.λy.x\n"
     ]
    }
   ],
   "source": [
    "print(INF.applique(UN).applique(TROIS).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 89,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.λy.x\n"
     ]
    }
   ],
   "source": [
    "print(INF.applique(UN).applique(UN).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 91,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λn.λm.((ET ((INF n) m)) ((INF m) n))\n",
      "λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n))\n"
     ]
    }
   ],
   "source": [
    "M_EGAL = Lambda_terme('!n.!m.((ET ((INF n) m)) ((INF m) n))')\n",
    "print(M_EGAL)\n",
    "EGAL = M_EGAL.subs('ET', ET).subs('INF', INF)\n",
    "print(EGAL)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 93,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.λy.x\n"
     ]
    }
   ],
   "source": [
    "print(EGAL.applique(UN).applique(UN).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 94,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λx.λy.y\n"
     ]
    }
   ],
   "source": [
    "print(EGAL.applique(UN).applique(DEUX).forme_normale())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Itération"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 95,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λn.(CDR ((n λc.((CONS (SUC (CAR c))) ((MUL (SUC (CAR c))) (CDR c)))) ((CONS ZERO) UN)))\n",
      "λn.(λc.(c λx.λy.y) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.x) c))) ((λn.λm.λf.(n (m f)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.x) c))) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.(f x))))\n"
     ]
    }
   ],
   "source": [
    "M_FACTv1 = Lambda_terme('!n.(CDR ((n !c.((CONS (SUC (CAR c))) ((MUL (SUC (CAR c))) (CDR c)))) ((CONS ZERO) UN)))')\n",
    "print(M_FACTv1)\n",
    "FACTv1 = M_FACTv1.subs('CONS', CONS).subs('CAR', CAR).subs('CDR', CDR).subs('SUC', SUC).subs('MUL', MUL).subs('UN', UN).subs('ZERO', ZERO)\n",
    "print(FACTv1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 96,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f x)\n"
     ]
    }
   ],
   "source": [
    "print(FACTv1.applique(ZERO).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 97,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f x)\n"
     ]
    }
   ],
   "source": [
    "print(FACTv1.applique(UN).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 98,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "None\n"
     ]
    }
   ],
   "source": [
    "print(FACTv1.applique(DEUX).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 99,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f (f x))\n"
     ]
    }
   ],
   "source": [
    "print(FACTv1.applique(DEUX).forme_normale(nb_etapes_max=200))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 100,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f (f (f (f (f (f x))))))\n"
     ]
    }
   ],
   "source": [
    "print(FACTv1.applique(TROIS).forme_normale(nb_etapes_max=500))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 101,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))\n"
     ]
    }
   ],
   "source": [
    "print(FACTv1.applique(QUATRE).forme_normale(nb_etapes_max=1700))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Et la récursivité ? "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 102,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λn.(((COND ((EGAL n) ZERO)) UN) ((MUL n) (f (PRED n))))\n",
      "λf.λn.(((λc.λa.λs.((c a) s) ((λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) n) λf.λx.x)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) n))))\n"
     ]
    }
   ],
   "source": [
    "M_PHI_FACT = Lambda_terme('!f.!n.(((COND ((EGAL n) ZERO)) UN) ((MUL n) (f (PRED n))))')\n",
    "print(M_PHI_FACT)\n",
    "PHI_FACT = M_PHI_FACT.subs('COND', COND).subs('EGAL', EGAL).subs('ZERO', ZERO).subs('UN', UN).subs('MUL', MUL).subs('PRED', PRED)\n",
    "print(PHI_FACT)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 103,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λy.(λx.(x x) λx.(x x))\n"
     ]
    }
   ],
   "source": [
    "BOTTOM = Lambda_terme('!y.OMEGA').subs('OMEGA', OMEGA)\n",
    "print(BOTTOM)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 104,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACT0 = PHI_FACT.applique(BOTTOM)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 105,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f x)\n"
     ]
    }
   ],
   "source": [
    "print(FACT0.applique(ZERO).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 107,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((λf.λn.(((λc.λa.λs.((c a) s) ((λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) n) λf.λx.x)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) n)))) λy.(λx.(x x) λx.(x x))) λf.λx.(f x))\n",
      "  1: ---> ((λf.λn.(((λc.λa.λs.((c a) s) ((λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) n) λf.λx.x)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (f (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) n)))) λy.(λx.(x x) λx.(x x))) λf.λx.(f x))\n",
      "  2: ---> (λn.(((λc.λa.λs.((c a) s) ((λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) n) λf.λx.x)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) n) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) n)))) λf.λx.(f x))\n",
      "  3: ---> (((λc.λa.λs.((c a) s) ((λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) λf.λx.(f x)) λf.λx.x)) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  4: ---> ((λa.λs.((((λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) λf.λx.(f x)) λf.λx.x) a) s) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  5: ---> (λs.((((λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) λf.λx.(f x)) λf.λx.x) λf.λx.(f x)) s) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  6: ---> ((((λn.λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) n) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) n)) λf.λx.(f x)) λf.λx.x) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  7: ---> (((λm.((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) m)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) m) λf.λx.(f x))) λf.λx.x) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  8: ---> ((((λa.λb.(((λc.λa.λs.((c a) s) a) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      "  9: ---> (((λb.(((λc.λa.λs.((c a) s) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x)) b) λx.λy.y) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 10: ---> (((((λc.λa.λs.((c a) s) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 11: ---> ((((λa.λs.((((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x) a) s) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 12: ---> (((λs.((((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) s) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 13: ---> ((((((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.(f x)) λf.λx.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 14: ---> (((((λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f x)) m)) λf.λx.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 15: ---> (((((λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f x)) λf.λx.x)) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 16: ---> ((((((((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) λf.λx.(f x)) λf.λx.x) λx.λx.λy.y) λx.λy.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 17: ---> (((((((λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f x)) λf.λx.x) λx.λx.λy.y) λx.λy.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 18: ---> ((((((((λf.λx.x λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) λf.λx.(f x)) λx.λx.λy.y) λx.λy.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 19: ---> (((((((λx.x λf.λx.(f x)) λx.λx.λy.y) λx.λy.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 20: ---> ((((((λf.λx.(f x) λx.λx.λy.y) λx.λy.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 21: ---> (((((λx.(λx.λx.λy.y x) λx.λy.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 22: ---> (((((λx.λx.λy.y λx.λy.x) ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 23: ---> ((((λx.λy.y ((λn.λm.(λn.((n λx.λx.λy.y) λx.λy.x) ((λn.λm.((m λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x)))) n) n) m)) λf.λx.x) λf.λx.(f x))) λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 24: ---> (((λy.y λx.λy.y) λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 25: ---> ((λx.λy.y λf.λx.(f x)) ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 26: ---> (λy.y ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x)))))\n",
      " 27: ---> ((λn.λm.λf.(n (m f)) λf.λx.(f x)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x))))\n",
      " 28: ---> (λm.λf.(λf.λx.(f x) (m f)) (λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x))))\n",
      " 29: ---> λf.(λf.λx.(f x) ((λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x))) f))\n",
      " 30: ---> λf.λx.(((λy.(λx.(x x) λx.(x x)) (λn.(λc.(c λx.λy.x) ((n λc.((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) (λc.(c λx.λy.y) c)) (λn.λf.λx.(f ((n f) x)) (λc.(c λx.λy.y) c)))) ((λx.λy.λs.(((λc.λa.λs.((c a) s) s) x) y) λf.λx.x) λf.λx.x))) λf.λx.(f x))) f) x)\n",
      " 31: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      " 32: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      " 33: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      " 34: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      " 35: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      " 36: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      " 37: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      " 38: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      " 39: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      " 40: ---> λf.λx.(((λx.(x x) λx.(x x)) f) x)\n",
      "Pas de forme normale atteinte après 40 étapes de réduction\n"
     ]
    }
   ],
   "source": [
    "FACT0.applique(UN).forme_normale(verbose=True, nb_etapes_max=40)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 108,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACT1 = PHI_FACT.applique(FACT0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 109,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f x)\n"
     ]
    }
   ],
   "source": [
    "print(FACT1.applique(ZERO).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 110,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f x)\n"
     ]
    }
   ],
   "source": [
    "print(FACT1.applique(UN).forme_normale(nb_etapes_max=200))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 111,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.(λx.(f (x x)) λx.(f (x x)))\n"
     ]
    }
   ],
   "source": [
    "FIX_CURRY = Lambda_terme('!f.(!x.(f (x x)) !x.(f (x x)))')\n",
    "print(FIX_CURRY)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 112,
   "metadata": {},
   "outputs": [],
   "source": [
    "FACTv2 = FIX_CURRY.applique(PHI_FACT)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 113,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f x)\n"
     ]
    }
   ],
   "source": [
    "print(FACTv2.applique(ZERO).forme_normale())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 115,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f x)\n"
     ]
    }
   ],
   "source": [
    "print(FACTv2.applique(UN).forme_normale(nb_etapes_max=200))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 116,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f (f x))\n"
     ]
    }
   ],
   "source": [
    "print(FACTv2.applique(DEUX).forme_normale(nb_etapes_max=700))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 117,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f (f (f (f (f (f x))))))\n"
     ]
    }
   ],
   "source": [
    "print(FACTv2.applique(TROIS).forme_normale(nb_etapes_max=4000))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 118,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "λf.λx.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))\n"
     ]
    }
   ],
   "source": [
    "print(FACTv2.applique(QUATRE).forme_normale(nb_etapes_max=25000))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 120,
   "metadata": {},
   "outputs": [],
   "source": [
    "PF = FIX_CURRY.applique(Lambda_terme('M'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 121,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(λf.(λx.(f (x x)) λx.(f (x x))) M)\n",
      "  1: ---> (λf.(λx.(f (x x)) λx.(f (x x))) M)\n",
      "  2: ---> (λx.(M (x x)) λx.(M (x x)))\n",
      "  3: ---> (M (λx.(M (x x)) λx.(M (x x))))\n",
      "  4: ---> (M (M (λx.(M (x x)) λx.(M (x x)))))\n",
      "  5: ---> (M (M (M (λx.(M (x x)) λx.(M (x x))))))\n",
      "  6: ---> (M (M (M (M (λx.(M (x x)) λx.(M (x x)))))))\n",
      "  7: ---> (M (M (M (M (M (λx.(M (x x)) λx.(M (x x))))))))\n",
      "  8: ---> (M (M (M (M (M (M (λx.(M (x x)) λx.(M (x x)))))))))\n",
      "  9: ---> (M (M (M (M (M (M (M (λx.(M (x x)) λx.(M (x x))))))))))\n",
      " 10: ---> (M (M (M (M (M (M (M (M (λx.(M (x x)) λx.(M (x x)))))))))))\n",
      "Pas de forme normale atteinte après 10 étapes de réduction\n"
     ]
    }
   ],
   "source": [
    "PF.forme_normale(verbose=True, nb_etapes_max=10)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "lines_to_next_cell": 2
   },
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# $\\lambda$-calcul avec les lambda-expressions de Python"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Les entiers de Church"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "zero = lambda f: lambda x: x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "un = lambda f: lambda x: f(x)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "deux = lambda f: lambda x: f(f(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "trois = lambda f: lambda x: f(f(f(x)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def entier_church_en_int(ec):\n",
    "    return ec(lambda n: n+1)(0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(entier_church_en_int(n) for n in (zero, un, deux, trois))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "suc = lambda n: lambda f: lambda x: f(n(f)(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(entier_church_en_int(suc(n)) for n in (zero, un, deux, trois)) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def int_en_entier_church(n):\n",
    "    if n == 0:\n",
    "        return zero\n",
    "    else:\n",
    "        return suc(int_en_entier_church(n - 1))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(entier_church_en_int(int_en_entier_church(n)) for n in range(10))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "add = lambda n: lambda m: lambda f: lambda x: n(f)(m(f)(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cinq = add(deux)(trois)\n",
    "entier_church_en_int(cinq)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "mul = lambda n: lambda m: lambda f: n(m(f))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "six = mul(deux)(trois)\n",
    "entier_church_en_int(six)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "exp = lambda n: lambda m: m(n)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "huit = exp(deux)(trois)\n",
    "entier_church_en_int(huit)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Les booléens"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "vrai = lambda x: lambda y: x\n",
    "faux = lambda x: lambda y: y"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def booleen_en_bool(b):\n",
    "    return b(True)(False)\n",
    "    "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(b) for b in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cond = lambda c: lambda a: lambda s: c(a)(s) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cond(vrai)(1)(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cond(faux)(1)(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cond(vrai)(1)(1/0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "non = lambda b: cond(b)(faux)(vrai)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(non(b)) for b in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "et = lambda b1: lambda b2: cond(b1)(b2)(faux)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(et(b1)(b2)) for b1 in (vrai, faux) for b2 in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ou = lambda b1: lambda b2: cond(b1)(vrai)(b2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(ou(b1)(b2)) for b1 in (vrai, faux) for b2 in (vrai, faux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "est_nul = lambda n : n(lambda x: faux)(vrai)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(est_nul(n)) for n in (zero, un, deux, trois, cinq, six, huit))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Les couples"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cons = lambda x: lambda y: lambda z: z(x)(y)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "un_deux = cons(un)(deux)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "car = lambda c: c(vrai)\n",
    "cdr = lambda c: c(faux)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "entier_church_en_int(car(un_deux)), entier_church_en_int(cdr(un_deux))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "pred = lambda n: car(n(lambda c: cons(cdr(c))(suc(cdr(c))))(cons(zero)(zero)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(entier_church_en_int(pred(int_en_entier_church(n))) for n in range(10))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "sub = lambda n: lambda m: m(pred)(n)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "entier_church_en_int(sub(huit)(trois))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "est_inf_ou_egal = lambda n: lambda m: est_nul(sub(m)(n))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(est_inf_ou_egal(cinq)(int_en_entier_church(n))) for n in range(10))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "est_egal = lambda n: lambda m: et(est_inf_ou_egal(n)(m))(est_inf_ou_egal(m)(n))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(booleen_en_bool(est_egal(cinq)(int_en_entier_church(n))) for n in range(10))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Itération"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fact = lambda n: cdr(n(lambda c: (cons(suc(car(c)))(mul(suc(car(c)))(cdr(c)))))(cons(zero)(un)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(entier_church_en_int(fact(int_en_entier_church(n))) for n in range(7))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Combinateur de point fixe"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "phi_fact = lambda f: lambda n: 1 if n == 0 else n*f(n-1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "bottom = lambda x: (lambda y: y(y))(lambda y:y(y))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "f0 = phi_fact(bottom)\n",
    "f1 = phi_fact(f0)\n",
    "f2 = phi_fact(f1)\n",
    "f3 = phi_fact(f2)\n",
    "f4 = phi_fact(f3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(f4(n) for n in range(4))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "def fact_rec(n):\n",
    "    if n == 0:\n",
    "        return 1\n",
    "    else:\n",
    "        return n * fact_rec(n - 1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fact2 = phi_fact(fact_rec)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(fact2(n) for n in range(7))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fix_curry = lambda f: (lambda x: lambda y: f(x(x))(y))(lambda x: lambda y: f(x(x))(y))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fact3 = fix_curry(phi_fact)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "tuple(fact3(n) for n in range(7))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "incorrectly_encoded_metadata": "toc-hr-collapsed=true toc-nb-collapsed=true"
   },
   "source": [
    "## Un programme obscur"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print((lambda x: (lambda y: lambda z: x(y(y))(z))(lambda y: lambda z: x(y(y))(z))) \n",
    "      (lambda x: lambda y: '' if y == [] else chr(y[0])+x(y[1:]))\n",
    "      (((lambda x: (lambda y: lambda z: x(y(y))(z)) (lambda y: lambda z: x(y(y))(z)))\n",
    "        (lambda x: lambda y: lambda z: [] if z == [] else [y(z[0])]+x(y)(z[1:])))      \n",
    "       (lambda x: (lambda x: (lambda y: lambda z: x(y(y))(z))(lambda y: lambda z: x(y(y))(z)))\n",
    "        (lambda x: lambda y: lambda z: lambda t: 1 if t == 0 else (lambda x: ((lambda u: 1 if u == 0 else z)(t % 2)) * x * x % y)\n",
    "         (x(y)(z)(t // 2)))(989)(x)(761))\n",
    "       ([377, 900, 27, 27, 182, 647, 163, 182, 390, 27, 726, 937])))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "phiListEnChaine = lambda x: lambda y: '' if y == [] else chr(y[0]) + x(y[1:])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fix_curry(phiListEnChaine)([65+k for k in range(26)])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "phiMap = lambda x: lambda y: lambda z: [] if z == [] else [y(z[0])] + x(y)(z[1:])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fix_curry(phiMap)(lambda x: x*x)([1, 2, 3, 4])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "phiExpoMod = lambda x: lambda y: lambda z: lambda t: 1 if z == 0 else (lambda u: 1 if u == 0 else y)(z % 2) * x(y)(z//2)(t) ** 2 % t"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "fix_curry(phiExpoMod)(2)(10)(1000)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "jupytext": {
   "formats": "ipynb,md"
  },
  "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.7.3"
  },
  "toc-autonumbering": true,
  "widgets": {
   "application/vnd.jupyter.widget-state+json": {
    "state": {},
    "version_major": 2,
    "version_minor": 0
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}