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

lp-space-efhm.lisp #97

Closed gheber closed 8 years ago

gheber commented 8 years ago

; in: DEFUN LS-HAT-U-U ; (THE CAT::CHAIN-COMPLEX (CAT::TNSR-PRDC CAT::COBAR CAT::SPAC-TNSR-LPSP)) ; ; note: type assertion too complex to check: ; (VALUES CHAIN-COMPLEX &REST T).

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

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

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

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

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

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

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

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

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

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

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

; in: DEFUN LS-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 CAT::PRE-REDUCTION CAT::PERTURBATION))) ; ; note: type assertion too complex to check: ; (VALUES REDUCTION &REST T).

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