diff --git a/examples/Chapter2.ipynb b/examples/Chapter2.ipynb index f1b3997..2b443f3 100644 --- a/examples/Chapter2.ipynb +++ b/examples/Chapter2.ipynb @@ -2,7 +2,7 @@ "cells": [ { "cell_type": "code", - "execution_count": 1, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -24,7 +24,7 @@ "(:KENZO)" ] }, - "execution_count": 1, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -35,7 +35,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -54,7 +54,7 @@ "NIL" ] }, - "execution_count": 2, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -72,7 +72,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -120,7 +120,7 @@ "-----------------------------------------------------------------------------\"" ] }, - "execution_count": 3, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -138,7 +138,7 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -168,7 +168,7 @@ "------------------------------------------------------------------------------\"" ] }, - "execution_count": 4, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -186,7 +186,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -230,7 +230,7 @@ "------------------------------------------------------------------------------\"" ] }, - "execution_count": 5, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -241,7 +241,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -260,7 +260,7 @@ "------------------------------------------------------------------------------\"" ] }, - "execution_count": 6, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -278,7 +278,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -289,7 +289,7 @@ "CDELTA" ] }, - "execution_count": 7, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -319,7 +319,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -330,7 +330,7 @@ "MAKE-F" ] }, - "execution_count": 8, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -353,7 +353,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -364,7 +364,7 @@ "MAKE-G" ] }, - "execution_count": 9, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -380,7 +380,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -391,7 +391,7 @@ "MAKE-H" ] }, - "execution_count": 10, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -416,7 +416,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -427,7 +427,7 @@ "MAKE-RDCT" ] }, - "execution_count": 11, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -444,7 +444,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -455,7 +455,7 @@ "[K8 Reduction K1 => K3]" ] }, - "execution_count": 12, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -466,7 +466,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -477,7 +477,7 @@ "(REDUCTION DELTA 6 3)" ] }, - "execution_count": 13, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -488,7 +488,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -507,7 +507,7 @@ "NIL" ] }, - "execution_count": 14, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -518,7 +518,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -535,7 +535,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 15, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -546,7 +546,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -560,7 +560,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 16, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -571,7 +571,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -648,7 +648,7 @@ "NIL" ] }, - "execution_count": 17, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -659,7 +659,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -670,7 +670,7 @@ "[K35 Reduction K1 => K30]" ] }, - "execution_count": 18, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -681,7 +681,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -692,7 +692,7 @@ "[K39 Reduction K30 => K3]" ] }, - "execution_count": 19, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -703,7 +703,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -714,7 +714,7 @@ "[K45 Reduction K1 => K3]" ] }, - "execution_count": 20, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -725,7 +725,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -744,7 +744,7 @@ "NIL" ] }, - "execution_count": 21, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -755,7 +755,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -832,7 +832,7 @@ "NIL" ] }, - "execution_count": 22, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -851,7 +851,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -862,7 +862,7 @@ "[K66 Homotopy-Equivalence K30 <= K30 => K30]" ] }, - "execution_count": 23, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -873,7 +873,7 @@ }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -884,7 +884,7 @@ "[K74 Homotopy-Equivalence K69 <= K69 => K69]" ] }, - "execution_count": 24, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -895,7 +895,7 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -908,7 +908,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 25, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -926,7 +926,7 @@ }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -945,7 +945,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 26, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -957,7 +957,7 @@ }, { "cell_type": "code", - "execution_count": 27, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -968,7 +968,7 @@ "((2 . ) (4 . ) (6 . ) (3 . ) (5 . ) (7 . ))" ] }, - "execution_count": 27, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -987,7 +987,7 @@ }, { "cell_type": "code", - "execution_count": 28, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -1003,7 +1003,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 28, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -1014,7 +1014,7 @@ }, { "cell_type": "code", - "execution_count": 29, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -1029,7 +1029,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 29, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -1040,7 +1040,7 @@ }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -1054,7 +1054,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 30, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -1065,7 +1065,7 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -1084,7 +1084,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 31, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -1095,7 +1095,7 @@ }, { "cell_type": "code", - "execution_count": 32, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -1111,7 +1111,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 32, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -1122,7 +1122,7 @@ }, { "cell_type": "code", - "execution_count": 33, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -1137,7 +1137,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 33, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -1148,7 +1148,7 @@ }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -1162,7 +1162,7 @@ "------------------------------------------------------------------------------\n" ] }, - "execution_count": 34, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -1173,7 +1173,7 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": 64, "metadata": { "collapsed": false }, @@ -1199,7 +1199,7 @@ ")" ] }, - "execution_count": 35, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -1209,6 +1209,1058 @@ " (cat:dispatch-bicn-cmbn comb-bic)\n", " (list b c d))" ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## 2.6 Construction of abicone from 2 reductions\n", + "#### Example" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:cat-init)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "CDELTA" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(defun cdelta (dmns)\n", + " (cat:build-chcm\n", + " :cmpr #'cat:l-cmpr\n", + " :basis #'(lambda (n)\n", + " (mapcar #'cat:dlop-int-ext (funcall (cat:delta-n-basis dmns) n)))\n", + " :bsgn '(0)\n", + " :intr-dffr\n", + " #'(lambda (degr gmsm)\n", + " (cat:make-cmbn\n", + " :degr (1- degr)\n", + " :list (do ((rslt cat:+empty-list+\n", + " (cons (cons sign\n", + " (append\n", + " (subseq gmsm 0 nark)\n", + " (subseq gmsm (1+ nark))))\n", + " rslt))\n", + " (sign 1 (- sign))\n", + " (nark 0 (1+ nark)))\n", + " ((> nark degr) rslt))))\n", + " :strt :gnrt\n", + " :orgn `(Effective version of C_* delta ,dmns)))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "[K1 Chain-Complex]" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:def delta3 (cdelta 3))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "((0) (1) (2) (3))" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:basis delta3 0)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "((0 1) (0 2) (1 2) (0 3) (1 3) (2 3))" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:basis delta3 1)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "((0 1 2) (0 1 3) (0 2 3) (1 2 3))" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:basis delta3 2)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "((0 1 2 3))" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:basis delta3 3)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:basis delta3 4)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "[K15 Chain-Complex]" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:def bic (cat:bicone (make-rdct 3 2) (make-rdct 4 2)))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "( ...)" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:basis bic 0)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "( ...)" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:basis bic 1)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "()" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:basis bic 4)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "\n", + "----------------------------------------------------------------------{CMBN 1}\n", + "<3 * >\n", + "<-3 * >\n", + "<3 * >\n", + "<12 * >\n", + "<-4 * >\n", + "<4 * >\n", + "<-4 * >\n", + "<5 * >\n", + "<-5 * >\n", + "<5 * >\n", + "------------------------------------------------------------------------------\n" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:? bic (cat:cmbn 2 3 (cat:bcnb '(0 1 3)) 4 (cat:bcnc '(0 1 2 3)) 5 (cat:bcnd '(0 1 4))))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "\n", + "----------------------------------------------------------------------{CMBN 0}\n", + "------------------------------------------------------------------------------\n" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:? bic (cat:? bic (cat:cmbn 2 3 (cat:bcnb '(0 1 3)) 4 (cat:bcnc '(0 1 2 3)) 5 (cat:bcnd '(0 1 4)))))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## 2.7 Composition of homotopy equivalences\n", + "#### Example" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:cat-init)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "[K1 Chain-Complex]" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:def c (cat:build-chcm\n", + " :cmpr #'cat:s-cmpr\n", + " :basis #'(lambda (dmns) (declare (ignore dmns)) '(a))\n", + " :bsgn 'a\n", + " :intr-dffr #'cat:zero-intr-dffr\n", + " :strt :cmbn\n", + " :orgn '(c)))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "[K6 Homotopy-Equivalence K1 <= K1 => K1]" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:def h1 (cat:trivial-hmeq c))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "[K17 Homotopy-Equivalence K1 <= K7 => K1]" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:def h2 (cat:cmps h1 h1))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:pre-check-rdct (cat:lrdct h2))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "\n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * >\n", + "<10 * >\n", + "<100 * >\n", + "------------------------------------------------------------------------------\n" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(setf cat:*tc* (cat:cmbn 3 1 (cat:bcnb 'a) 10 (cat:bcnc 'a) 100 (cat:bcnd 'a)))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "\n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * A>\n", + "------------------------------------------------------------------------------\n" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(setf cat:*bc* (cat:cmbn 3 1 'a))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "*TC* => \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * >\n", + "<10 * >\n", + "<100 * >\n", + "------------------------------------------------------------------------------\n", + "\n", + "*BC* => \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * A>\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *TDD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 1}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *BDD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 1}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *DF-FD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 2}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *DG-GD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 2}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *ID-FG* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *ID-GF-DH-HD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *HH* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 5}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *FH* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 4}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *HG* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 4}\n", + "------------------------------------------------------------------------------\n", + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:check-rdct-no-wait)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:pre-check-rdct (cat:rrdct h2))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "*TC* => \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * >\n", + "<10 * >\n", + "<100 * >\n", + "------------------------------------------------------------------------------\n", + "\n", + "*BC* => \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * A>\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *TDD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 1}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *BDD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 1}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *DF-FD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 2}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *DG-GD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 2}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *ID-FG* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *ID-GF-DH-HD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *HH* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 5}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *FH* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 4}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *HG* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 4}\n", + "------------------------------------------------------------------------------\n", + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:check-rdct-no-wait)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "[K65 Homotopy-Equivalence K1 <= K55 => K1]" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:def h3 (cat:cmps h2 h2))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/plain": [ + "\n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * >>\n", + "<10 * >>\n", + "<100 * >>\n", + "<1000 * >\n", + "<10000 * >>\n", + "<5234 * >>\n", + "<223 * >>\n", + "------------------------------------------------------------------------------\n" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(setf cat:*tc* (cat:cmbn 3 1 (cat:bcnb (cat:bcnb 'a)) 10 (cat:bcnb (cat:bcnc 'a)) 100 (cat:bcnb (cat:bcnd 'a))\n", + " 1000 (cat:bcnc 'a)\n", + " 10000 (cat:bcnd (cat:bcnb 'a)) 5234 (cat:bcnd (cat:bcnc 'a))\n", + " 223 (cat:bcnd (cat:bcnd 'a))))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:pre-check-rdct (cat:lrdct h3))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "*TC* => \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * >>\n", + "<10 * >>\n", + "<100 * >>\n", + "<1000 * >\n", + "<10000 * >>\n", + "<5234 * >>\n", + "<223 * >>\n", + "------------------------------------------------------------------------------\n", + "\n", + "*BC* => \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * A>\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *TDD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 1}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *BDD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 1}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *DF-FD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 2}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *DG-GD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 2}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *ID-FG* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *ID-GF-DH-HD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *HH* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 5}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *FH* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 4}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *HG* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 4}\n", + "------------------------------------------------------------------------------\n", + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:check-rdct-no-wait)" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:pre-check-rdct (cat:rrdct h3))" + ] + }, + { + "cell_type": "code", + "execution_count": 64, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "*TC* => \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * >>\n", + "<10 * >>\n", + "<100 * >>\n", + "<1000 * >\n", + "<10000 * >>\n", + "<5234 * >>\n", + "<223 * >>\n", + "------------------------------------------------------------------------------\n", + "\n", + "*BC* => \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "<1 * A>\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *TDD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 1}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *BDD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 1}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *DF-FD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 2}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *DG-GD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 2}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *ID-FG* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *ID-GF-DH-HD* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 3}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *HH* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 5}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *FH* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 4}\n", + "------------------------------------------------------------------------------\n", + "\n", + "Checking *HG* = 0\n", + "Result: \n", + "----------------------------------------------------------------------{CMBN 4}\n", + "------------------------------------------------------------------------------\n", + "\n", + "---done---" + ] + }, + { + "data": { + "text/plain": [ + "NIL" + ] + }, + "execution_count": 64, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(cat:check-rdct-no-wait)" + ] } ], "metadata": {