search

gheber / kenzo

A repackaged version of the Kenzo program by Francis Sergeraert and collaborators.
https://sur-l-analysis-sit.us/
Other
50 stars 8 forks source link

cl-space-efhm.lisp #102

Closed gheber closed 8 years ago

gheber commented 8 years ago

; in: DEFUN CS-HAT-U-U ; (THE CAT::CHAIN-COMPLEX (CAT::TNSR-PRDC CAT::CLSP-TNSR-SMGR CAT::BAR)) ; ; note: type assertion too complex to check: ; (VALUES CHAIN-COMPLEX &REST T).

; in: DEFUN CS-HAT-RIGHT-PERTURBATION ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC CAT::HAT-U-U :TRGT CAT::HAT-U-U :DEGR -1 :INTR ; (CAT::CS-HAT-RIGHT-PERTURBATION-INTR CAT::SMGR) :STRT ; :GNRT :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN CS-HAT-U-T ; (THE CAT::CHAIN-COMPLEX ; (PROGN ; (SETF (SLOT-VALUE CAT::HAT-RIGHT-PERTURBATION 'CAT::SORC) CAT::HAT-U-U ; (SLOT-VALUE CAT::HAT-RIGHT-PERTURBATION 'CAT::TRGT) CAT::HAT-U-U) ; (CAT::ADD CAT::HAT-U-U CAT::HAT-RIGHT-PERTURBATION))) ; ; note: type assertion too complex to check: ; (VALUES CHAIN-COMPLEX &REST T).

; in: DEFUN CS-LEFT-HMEQ-HAT ; (THE CAT::CHAIN-COMPLEX (CAT::ADD CAT::HAT-T-U CAT::HAT-RIGHT-PERTURBATION)) ; ; note: type assertion too complex to check: ; (VALUES CHAIN-COMPLEX &REST T).

; in: DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-F ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC CAT::HAT-U-T :TRGT CAT::CLASSIFYING-SPACE :DEGR 0 ; :INTR #'CAT::CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-F ; :STRT :CMBN :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-G ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC CAT::CLASSIFYING-SPACE :TRGT CAT::HAT-U-T :DEGR 0 ; :INTR ; (CAT::CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-G ; (CAT::BSPN CAT::SMGR)) ; :STRT :CMBN :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-H ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC CAT::HAT-U-T :TRGT CAT::HAT-U-T :DEGR 1 :INTR ; (CAT::CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-INTR-H ; (CAT::CMPR CAT::HAT-U-T) (CAT::BSPN CAT::SMGR)) ; :STRT :CMBN :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN CS-PRE-LEFT-HMEQ-LEFT-REDUCTION ; (THE CAT::REDUCTION ; (CAT::BUILD-RDCT :F (CAT::CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-F CAT::SMGR) ; :G (CAT::CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-G CAT::SMGR) ; :H (CAT::CS-PRE-LEFT-HMEQ-LEFT-REDUCTION-H CAT::SMGR) ; :ORGN ; `(CAT::CS-PRE-LEFT-HMEQ-LEFT-REDUCTION ,CAT::SMGR))) ; ; note: type assertion too complex to check: ; (VALUES REDUCTION &REST T).

; in: DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-F ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC CAT::HAT-T-U :TRGT CAT::BAR :DEGR 0 :INTR ; #'CAT::CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-INTR-F :STRT ; :CMBN :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-G ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC CAT::BAR :TRGT CAT::HAT-T-U :DEGR 0 :INTR ; (CAT::CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-INTR-G ; CAT::IDNT) ; :STRT :CMBN :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-H ; (THE CAT::MORPHISM ; (CAT::TNSR-PRDC CAT::TNPR-CONTRACTION (CAT::IDNT-MRPH CAT::BAR))) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION ; (THE CAT::REDUCTION ; (CAT::BUILD-RDCT :F (CAT::CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-F CAT::SMGR) ; :G (CAT::CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-G CAT::SMGR) ; :H (CAT::CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION-H CAT::SMGR) ; :ORGN ; `(CAT::CS-PRE-LEFT-HMEQ-RIGHT-REDUCTION ,CAT::SMGR))) ; ; note: type assertion too complex to check: ; (VALUES REDUCTION &REST T).

; in: DEFUN CS-LEFT-HMEQ-RIGHT-REDUCTION ; (THE CAT::REDUCTION ; (PROGN ; (SETF (SLOT-VALUE CAT::PERTURBATION 'CAT::SORC) ; (CAT::TCC CAT::PRE-REDUCTION) ; (SLOT-VALUE CAT::PERTURBATION 'CAT::TRGT) ; (CAT::TCC CAT::PRE-REDUCTION)) ; (CAT::SPECIAL-BPL-2 CAT::PRE-REDUCTION CAT::PERTURBATION))) ; ; note: type assertion too complex to check: ; (VALUES REDUCTION &REST T).

; in: DEFUN CS-LEFT-HMEQ ; (THE CAT::HOMOTOPY-EQUIVALENCE ; (CAT::BUILD-HMEQ :LRDCT (CAT::CS-LEFT-HMEQ-LEFT-REDUCTION CAT::SMGR) ; :RRDCT (CAT::CS-LEFT-HMEQ-RIGHT-REDUCTION CAT::SMGR) ; :ORGN `(CAT::CS-LEFT-HMEQ ,CAT::SMGR))) ; ; note: type assertion too complex to check: ; (VALUES HOMOTOPY-EQUIVALENCE &REST T).