Known df_mfsh__df_mevl__df_mvl__df_mvsb__df_mfrel__df_mdl__df_musyn__df_gmdl__df_mitp__df_mfitp__df_irng__df_cplmet__df_homlimb__df_homlim__df_plfl__df_sfl1__df_sfl__df_psl : ∀ x0 : ο . (wceq cmfsh (cslot c8) ⟶ wceq cmevl (cslot c9) ⟶ wceq cmvl (cmpt (λ x1 . cvv) (λ x1 . cixp (λ x2 . cfv (cv x1) cmvar) (λ x2 . cima (cfv (cv x1) cmuv) (csn (cfv (cv x2) (cfv (cv x1) cmty)))))) ⟶ wceq cmvsb (cmpt (λ x1 . cvv) (λ x1 . coprab (λ x2 x3 x4 . w3a (wa (wcel (cv x2) (crn (cfv (cv x1) cmsub))) (wcel (cv x3) (cfv (cv x1) cmvl))) (wral (λ x5 . wbr (cv x3) (cfv (cfv (cv x5) (cfv (cv x1) cmvh)) (cv x2)) (cdm (cfv (cv x1) cmevl))) (λ x5 . cfv (cv x1) cmvar)) (wceq (cv x4) (cmpt (λ x5 . cfv (cv x1) cmvar) (λ x5 . co (cv x3) (cfv (cfv (cv x5) (cfv (cv x1) cmvh)) (cv x2)) (cfv (cv x1) cmevl))))))) ⟶ wceq cmfr (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wceq (ccnv (cv x2)) (cv x2)) (wral (λ x3 . wral (λ x4 . wrex (λ x5 . wss (cv x4) (cima (cv x2) (csn (cv x5)))) (λ x5 . cima (cfv (cv x1) cmuv) (csn (cv x3)))) (λ x4 . cin (cpw (cfv (cv x1) cmuv)) cfn)) (λ x3 . cfv (cv x1) cmvt))) (λ x2 . cpw (cxp (cfv (cv x1) cmuv) (cfv (cv x1) cmuv))))) ⟶ wceq cmdl (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wa (w3a (wss (cv x2) (cxp (cfv (cv x1) cmtc) cvv)) (wcel (cv x6) (cfv (cv x1) cmfr)) (wcel (cv x5) (co (cv x2) (cxp (cv x4) (cfv (cv x1) cmex)) cpm))) (wral (λ x7 . wa (w3a (wral (λ x8 . wss (cima (cv x5) (csn (cop (cv x7) (cv x8)))) (cima (cv x2) (csn (cfv (cv x8) c1st)))) (λ x8 . cv x3)) (wral (λ x8 . wbr (cop (cv x7) (cfv (cv x8) (cfv (cv x1) cmvh))) (cfv (cv x8) (cv x7)) (cv x5)) (λ x8 . cfv (cv x1) cmvar)) (∀ x8 x9 x10 . wcel (cotp (cv x8) (cv x9) (cv x10)) (cfv (cv x1) cmax) ⟶ wa (∀ x11 x12 . wbr (cv x11) (cv x12) (cv x8) ⟶ wbr (cfv (cv x11) (cv x7)) (cfv (cv x12) (cv x7)) (cv x6)) (wss (cv x9) (cima (cdm (cv x5)) (csn (cv x7)))) ⟶ wbr (cv x7) (cv x10) (cdm (cv x5)))) (w3a (wral (λ x8 . wral (λ x9 . ∀ x10 . wbr (cop (cv x8) (cv x7)) (cv x10) (cfv (cv x1) cmvsb) ⟶ wceq (cima (cv x5) (csn (cop (cv x7) (cfv (cv x9) (cv x8))))) (cima (cv x5) (csn (cop (cv x10) (cv x9))))) (λ x9 . cfv (cv x1) cmex)) (λ x8 . crn (cfv (cv x1) cmsub))) (wral (λ x8 . wral (λ x9 . wceq (cres (cv x7) (cfv (cv x9) (cfv (cv x1) cmvrs))) (cres (cv x8) (cfv (cv x9) (cfv (cv x1) cmvrs))) ⟶ wceq (cima (cv x5) (csn (cop (cv x7) (cv x9)))) (cima (cv x5) (csn (cop (cv x8) (cv x9))))) (λ x9 . cv x3)) (λ x8 . cv x4)) (wral (λ x8 . wral (λ x9 . wss (cima (cv x7) (cfv (cv x9) (cfv (cv x1) cmvrs))) (cima (cv x6) (csn (cv x8))) ⟶ wss (cima (cv x5) (csn (cop (cv x7) (cv x9)))) (cima (cv x6) (csn (cv x8)))) (λ x9 . cv x3)) (λ x8 . cv x2)))) (λ x7 . cv x4))) (cfv (cv x1) cmfsh)) (cfv (cv x1) cmevl)) (cfv (cv x1) cmvl)) (cfv (cv x1) cmex)) (cfv (cv x1) cmuv)) (λ x1 . cmfs)) ⟶ wceq cusyn (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cmuv) (λ x2 . cop (cfv (cfv (cv x2) c1st) (cfv (cv x1) cmsy)) (cfv (cv x2) c2nd)))) ⟶ (∀ x1 . wceq cgmdl (crab (λ x2 . w3a (wral (λ x3 . wss (cima (cfv (cv x2) cmuv) (csn (cv x3))) (cima (cfv (cv x2) cmuv) (csn (cfv (cv x3) (cfv (cv x2) cmsy))))) (λ x3 . cfv (cv x2) cmtc)) (wral (λ x3 . wral (λ x4 . wb (wbr (cv x3) (cv x4) (cfv (cv x2) cmfsh)) (wbr (cv x3) (cfv (cv x4) (cfv (cv x2) cusyn)) (cfv (cv x2) cmfsh))) (λ x4 . cfv (cv x1) cmuv)) (λ x3 . cfv (cv x1) cmuv)) (wral (λ x3 . wral (λ x4 . wceq (cima (cfv (cv x2) cmevl) (csn (cop (cv x3) (cv x4)))) (cin (cima (cfv (cv x2) cmevl) (csn (cop (cv x3) (cfv (cv x4) (cfv (cv x2) cmesy))))) (cima (cfv (cv x2) cmuv) (csn (cfv (cv x4) c1st))))) (λ x4 . cfv (cv x2) cmex)) (λ x3 . cfv (cv x2) cmvl))) (λ x2 . cin cmgfs cmdl))) ⟶ wceq cmitp (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cmsa) (λ x2 . cmpt (λ x3 . cixp (λ x4 . cfv (cv x2) (cfv (cv x1) cmvrs)) (λ x4 . cima (cfv (cv x1) cmuv) (csn (cfv (cv x4) (cfv (cv x1) cmty))))) (λ x3 . cio (λ x4 . wrex (λ x5 . wa (wceq (cv x3) (cres (cv x5) (cfv (cv x2) (cfv (cv x1) cmvrs)))) (wceq (cv x4) (co (cv x5) (cv x2) (cfv (cv x1) cmevl)))) (λ x5 . cfv (cv x1) cmvl)))))) ⟶ wceq cmfitp (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cixp (λ x3 . cfv (cv x1) cmsa) (λ x3 . co (cima (cfv (cv x1) cmuv) (csn (cfv (cv x3) (cfv (cv x1) c1st)))) (cixp (λ x4 . cfv (cv x3) (cfv (cv x1) cmvrs)) (λ x4 . cima (cfv (cv x1) cmuv) (csn (cfv (cv x4) (cfv (cv x1) cmty))))) cmap)) (λ x2 . crio (λ x3 . wral (λ x4 . w3a (wral (λ x5 . wbr (cop (cv x4) (cfv (cv x5) (cfv (cv x1) cmvh))) (cfv (cv x5) (cv x4)) (cv x3)) (λ x5 . cfv (cv x1) cmvar)) (∀ x5 x6 x7 . wbr (cv x5) (cop (cv x6) (cv x7)) (cfv (cv x1) cmst) ⟶ wbr (cop (cv x4) (cv x5)) (cfv (cmpt (λ x8 . cfv (cv x6) (cfv (cv x1) cmvrs)) (λ x8 . co (cv x4) (cfv (cfv (cv x8) (cfv (cv x1) cmvh)) (cv x7)) (cv x3))) (cv x2)) (cv x3)) (wral (λ x5 . wceq (cima (cv x3) (csn (cop (cv x4) (cv x5)))) (cin (cima (cv x3) (csn (cop (cv x4) (cfv (cv x5) (cfv (cv x1) cmesy))))) (cima (cfv (cv x1) cmuv) (csn (cfv (cv x5) c1st))))) (λ x5 . cfv (cv x1) cmex))) (λ x4 . cfv (cv x1) cmvl)) (λ x3 . co (cfv (cv x1) cmuv) (cxp (cfv (cv x1) cmvl) (cfv (cv x1) cmex)) cpm)))) ⟶ wceq citr (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . ciun (λ x3 . cfv (co (cv x1) (cv x2) cress) cmn1) (λ x3 . cima (ccnv (cv x3)) (csn (cfv (cv x1) c0g))))) ⟶ wceq ccpms (cmpt (λ x1 . cvv) (λ x1 . csb (co (co (cv x1) cn cpws) (cfv (cfv (cv x1) cds) cca) cress) (λ x2 . csb (cfv (cv x2) cbs) (λ x3 . csb (copab (λ x4 x5 . wa (wss (cpr (cv x4) (cv x5)) (cv x3)) (wral (λ x6 . wrex (λ x7 . wf (cfv (cv x7) cuz) (co (cfv (cv x7) (cv x5)) (cv x6) (cfv (cfv (cv x1) cds) cbl)) (cres (cv x4) (cfv (cv x7) cuz))) (λ x7 . cz)) (λ x6 . crp)))) (λ x4 . co (co (cv x2) (cv x4) cqus) (csn (cop (cfv cnx cds) (coprab (λ x5 x6 x7 . wrex (λ x8 . wrex (λ x9 . wa (wa (wceq (cv x5) (cec (cv x8) (cv x4))) (wceq (cv x6) (cec (cv x9) (cv x4)))) (wbr (co (cv x8) (cv x9) (cof (cfv (cv x2) cds))) (cv x7) cli)) (λ x9 . cv x3)) (λ x8 . cv x3))))) csts))))) ⟶ wceq chlb (cmpt (λ x1 . cvv) (λ x1 . csb (ciun (λ x2 . cn) (λ x2 . cxp (csn (cv x2)) (cdm (cfv (cv x2) (cv x1))))) (λ x2 . csb (cint (cab (λ x3 . wa (wer (cv x2) (cv x3)) (wss (cmpt (λ x4 . cv x2) (λ x4 . cop (co (cfv (cv x4) c1st) c1 caddc) (cfv (cfv (cv x4) c2nd) (cfv (cfv (cv x4) c1st) (cv x1))))) (cv x3))))) (λ x3 . cop (cqs (cv x2) (cv x3)) (cmpt (λ x4 . cn) (λ x4 . cmpt (λ x5 . cdm (cfv (cv x4) (cv x1))) (λ x5 . cec (cop (cv x4) (cv x5)) (cv x3)))))))) ⟶ wceq chlim (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cv x2) chlb) (λ x3 . csb (cfv (cv x3) c1st) (λ x4 . csb (cfv (cv x3) c2nd) (λ x5 . cun (ctp (cop (cfv cnx cbs) (cv x4)) (cop (cfv cnx cplusg) (ciun (λ x6 . cn) (λ x6 . crn (cmpt2 (λ x7 x8 . cdm (cfv (cv x6) (cv x5))) (λ x7 x8 . cdm (cfv (cv x6) (cv x5))) (λ x7 x8 . cop (cop (cfv (cv x7) (cfv (cv x6) (cv x5))) (cfv (cv x8) (cfv (cv x6) (cv x5)))) (cfv (co (cv x7) (cv x8) (cfv (cfv (cv x6) (cv x1)) cplusg)) (cfv (cv x6) (cv x5)))))))) (cop (cfv cnx cmulr) (ciun (λ x6 . cn) (λ x6 . crn (cmpt2 (λ x7 x8 . cdm (cfv (cv x6) (cv x5))) (λ x7 x8 . cdm (cfv (cv x6) (cv x5))) (λ x7 x8 . cop (cop (cfv (cv x7) (cfv (cv x6) (cv x5))) (cfv (cv x8) (cfv (cv x6) (cv x5)))) (cfv (co (cv x7) (cv x8) (cfv (cfv (cv x6) (cv x1)) cmulr)) (cfv (cv x6) (cv x5))))))))) (ctp (cop (cfv cnx ctopn) (crab (λ x6 . wral (λ x7 . wcel (cima (ccnv (cfv (cv x7) (cv x5))) (cv x6)) (cfv (cfv (cv x7) (cv x1)) ctopn)) (λ x7 . cn)) (λ x6 . cpw (cv x4)))) (cop (cfv cnx cds) (ciun (λ x6 . cn) (λ x6 . crn (cmpt2 (λ x7 x8 . cdm (cfv (cv x6) (cfv (cv x6) (cv x5)))) (λ x7 x8 . cdm (cfv (cv x6) (cfv (cv x6) (cv x5)))) (λ x7 x8 . cop (cop (cfv (cv x7) (cfv (cv x6) (cv x5))) (cfv (cv x8) (cfv (cv x6) (cv x5)))) (co (cv x7) (cv x8) (cfv (cfv (cv x6) (cv x1)) cds))))))) (cop (cfv cnx cple) (ciun (λ x6 . cn) (λ x6 . ccom (ccnv (cfv (cv x6) (cv x5))) (ccom (cfv (cfv (cv x6) (cv x1)) cple) (cfv (cv x6) (cv x5)))))))))))) ⟶ wceq cpfl (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cv x1) cpl1) (λ x3 . csb (cfv (csn (cv x2)) (cfv (cv x3) crsp)) (λ x4 . csb (cmpt (λ x5 . cfv (cv x1) cbs) (λ x5 . cec (co (cv x5) (cfv (cv x3) cur) (cfv (cv x3) cvsca)) (co (cv x3) (cv x4) cqg))) (λ x5 . cop (csb (co (cv x3) (co (cv x3) (cv x4) cqg) cqus) (λ x6 . co (co (cv x6) (crio (λ x7 . wceq (ccom (cv x7) (cv x5)) (cfv (cv x1) cnm)) (λ x7 . cfv (cv x6) cabv)) ctng) (cop (cfv cnx cple) (csb (cmpt (λ x7 . cfv (cv x6) cbs) (λ x7 . crio (λ x8 . wbr (co (cv x1) (cv x8) cdg1) (co (cv x1) (cv x2) cdg1) clt) (λ x8 . cv x7))) (λ x7 . ccom (ccnv (cv x7)) (ccom (cfv (cv x3) cple) (cv x7))))) csts)) (cv x5)))))) ⟶ wceq csf1 (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (cv x1) cpl1) (λ x3 . cfv (cfv (co c1 (co (cv x1) (cv x3) cdg1) cfz) ccrd) (crdg (cmpt2 (λ x4 x5 . cvv) (λ x4 x5 . cvv) (λ x4 x5 . csb (cfv (cv x4) cmpl) (λ x6 . csb (crab (λ x7 . wa (wbr (cv x7) (ccom (cv x3) (cv x5)) (cfv (cv x6) cdsr)) (wbr c1 (co (cv x4) (cv x7) cdg1) clt)) (λ x7 . cin (cfv (cv x4) cmn1) (cfv (cv x6) cir))) (λ x7 . cif (wo (wceq (ccom (cv x3) (cv x5)) (cfv (cv x6) c0g)) (wceq (cv x7) c0)) (cop (cv x4) (cv x5)) (csb (cfv (cv x7) cglb) (λ x8 . csb (co (cv x4) (cv x8) cpfl) (λ x9 . cop (cfv (cv x9) c1st) (ccom (cv x5) (cfv (cv x9) c2nd))))))))) (cv x2))))) ⟶ wceq csf (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cio (λ x3 . wex (λ x4 . wa (wiso (co c1 (cfv (cv x2) chash) cfz) (cv x2) clt (cfv (cv x1) cplt) (cv x4)) (wceq (cv x3) (cfv (cfv (cv x2) chash) (cseq (cmpt2 (λ x5 x6 . cvv) (λ x5 x6 . cvv) (λ x5 x6 . cfv (cv x6) (co (cv x1) (cv x5) csf1))) (cun (cv x4) (csn (cop cc0 (cop (cv x1) (cres cid (cfv (cv x1) cbs)))))) cc0))))))) ⟶ wceq cpsl (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . co (cin (cpw (cfv (cv x1) cbs)) cfn) cn cmap) (λ x1 x2 . csb (ccom c1st (cseq (cmpt2 (λ x3 x4 . cvv) (λ x3 x4 . cvv) (λ x3 x4 . csb (cfv (cv x3) c1st) (λ x5 . csb (cfv (cv x5) c1st) (λ x6 . csb (co (cv x6) (crn (cmpt (λ x7 . cv x4) (λ x7 . ccom (cv x7) (cfv (cv x3) c2nd)))) csf) (λ x7 . cop (cv x7) (ccom (cfv (cv x3) c2nd) (cfv (cv x7) c2nd))))))) (cun (cv x2) (csn (cop cc0 (cop (cop (cv x1) c0) (cres cid (cfv (cv x1) cbs)))))) cc0)) (λ x3 . co (ccom c1st (co (cv x3) c1 cshi)) (ccom c2nd (cv x3)) chlim))) ⟶ x0) ⟶ x0
Theorem df_mfsh : wceq cmfsh (cslot c8) (proof)
Theorem df_mevl : wceq cmevl (cslot c9) (proof)
Theorem df_mvl : wceq cmvl (cmpt (λ x0 . cvv) (λ x0 . cixp (λ x1 . cfv (cv x0) cmvar) (λ x1 . cima (cfv (cv x0) cmuv) (csn (cfv (cv x1) (cfv (cv x0) cmty)))))) (proof)
Theorem df_mvsb : wceq cmvsb (cmpt (λ x0 . cvv) (λ x0 . coprab (λ x1 x2 x3 . w3a (wa (wcel (cv x1) (crn (cfv (cv x0) cmsub))) (wcel (cv x2) (cfv (cv x0) cmvl))) (wral (λ x4 . wbr (cv x2) (cfv (cfv (cv x4) (cfv (cv x0) cmvh)) (cv x1)) (cdm (cfv (cv x0) cmevl))) (λ x4 . cfv (cv x0) cmvar)) (wceq (cv x3) (cmpt (λ x4 . cfv (cv x0) cmvar) (λ x4 . co (cv x2) (cfv (cfv (cv x4) (cfv (cv x0) cmvh)) (cv x1)) (cfv (cv x0) cmevl))))))) (proof)
Theorem df_mfrel : wceq cmfr (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wceq (ccnv (cv x1)) (cv x1)) (wral (λ x2 . wral (λ x3 . wrex (λ x4 . wss (cv x3) (cima (cv x1) (csn (cv x4)))) (λ x4 . cima (cfv (cv x0) cmuv) (csn (cv x2)))) (λ x3 . cin (cpw (cfv (cv x0) cmuv)) cfn)) (λ x2 . cfv (cv x0) cmvt))) (λ x1 . cpw (cxp (cfv (cv x0) cmuv) (cfv (cv x0) cmuv))))) (proof)
Theorem df_mdl : wceq cmdl (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wa (w3a (wss (cv x1) (cxp (cfv (cv x0) cmtc) cvv)) (wcel (cv x5) (cfv (cv x0) cmfr)) (wcel (cv x4) (co (cv x1) (cxp (cv x3) (cfv (cv x0) cmex)) cpm))) (wral (λ x6 . wa (w3a (wral (λ x7 . wss (cima (cv x4) (csn (cop (cv x6) (cv x7)))) (cima (cv x1) (csn (cfv (cv x7) c1st)))) (λ x7 . cv x2)) (wral (λ x7 . wbr (cop (cv x6) (cfv (cv x7) (cfv (cv x0) cmvh))) (cfv (cv x7) (cv x6)) (cv x4)) (λ x7 . cfv (cv x0) cmvar)) (∀ x7 x8 x9 . wcel (cotp (cv x7) (cv x8) (cv x9)) (cfv (cv x0) cmax) ⟶ wa (∀ x10 x11 . wbr (cv x10) (cv x11) (cv x7) ⟶ wbr (cfv (cv x10) (cv x6)) (cfv (cv x11) (cv x6)) (cv x5)) (wss (cv x8) (cima (cdm (cv x4)) (csn (cv x6)))) ⟶ wbr (cv x6) (cv x9) (cdm (cv x4)))) (w3a (wral (λ x7 . wral (λ x8 . ∀ x9 . wbr (cop (cv x7) (cv x6)) (cv x9) (cfv (cv x0) cmvsb) ⟶ wceq (cima (cv x4) (csn (cop (cv x6) (cfv (cv x8) (cv x7))))) (cima (cv x4) (csn (cop (cv x9) (cv x8))))) (λ x8 . cfv (cv x0) cmex)) (λ x7 . crn (cfv (cv x0) cmsub))) (wral (λ x7 . wral (λ x8 . wceq (cres (cv x6) (cfv (cv x8) (cfv (cv x0) cmvrs))) (cres (cv x7) (cfv (cv x8) (cfv (cv x0) cmvrs))) ⟶ wceq (cima (cv x4) (csn (cop (cv x6) (cv x8)))) (cima (cv x4) (csn (cop (cv x7) (cv x8))))) (λ x8 . cv x2)) (λ x7 . cv x3)) (wral (λ x7 . wral (λ x8 . wss (cima (cv x6) (cfv (cv x8) (cfv (cv x0) cmvrs))) (cima (cv x5) (csn (cv x7))) ⟶ wss (cima (cv x4) (csn (cop (cv x6) (cv x8)))) (cima (cv x5) (csn (cv x7)))) (λ x8 . cv x2)) (λ x7 . cv x1)))) (λ x6 . cv x3))) (cfv (cv x0) cmfsh)) (cfv (cv x0) cmevl)) (cfv (cv x0) cmvl)) (cfv (cv x0) cmex)) (cfv (cv x0) cmuv)) (λ x0 . cmfs)) (proof)
Theorem df_musyn : wceq cusyn (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cmuv) (λ x1 . cop (cfv (cfv (cv x1) c1st) (cfv (cv x0) cmsy)) (cfv (cv x1) c2nd)))) (proof)
Theorem df_gmdl : ∀ x0 . wceq cgmdl (crab (λ x1 . w3a (wral (λ x2 . wss (cima (cfv (cv x1) cmuv) (csn (cv x2))) (cima (cfv (cv x1) cmuv) (csn (cfv (cv x2) (cfv (cv x1) cmsy))))) (λ x2 . cfv (cv x1) cmtc)) (wral (λ x2 . wral (λ x3 . wb (wbr (cv x2) (cv x3) (cfv (cv x1) cmfsh)) (wbr (cv x2) (cfv (cv x3) (cfv (cv x1) cusyn)) (cfv (cv x1) cmfsh))) (λ x3 . cfv (cv x0) cmuv)) (λ x2 . cfv (cv x0) cmuv)) (wral (λ x2 . wral (λ x3 . wceq (cima (cfv (cv x1) cmevl) (csn (cop (cv x2) (cv x3)))) (cin (cima (cfv (cv x1) cmevl) (csn (cop (cv x2) (cfv (cv x3) (cfv (cv x1) cmesy))))) (cima (cfv (cv x1) cmuv) (csn (cfv (cv x3) c1st))))) (λ x3 . cfv (cv x1) cmex)) (λ x2 . cfv (cv x1) cmvl))) (λ x1 . cin cmgfs cmdl)) (proof)
Theorem df_mitp : wceq cmitp (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cmsa) (λ x1 . cmpt (λ x2 . cixp (λ x3 . cfv (cv x1) (cfv (cv x0) cmvrs)) (λ x3 . cima (cfv (cv x0) cmuv) (csn (cfv (cv x3) (cfv (cv x0) cmty))))) (λ x2 . cio (λ x3 . wrex (λ x4 . wa (wceq (cv x2) (cres (cv x4) (cfv (cv x1) (cfv (cv x0) cmvrs)))) (wceq (cv x3) (co (cv x4) (cv x1) (cfv (cv x0) cmevl)))) (λ x4 . cfv (cv x0) cmvl)))))) (proof)
Theorem df_mfitp : wceq cmfitp (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cixp (λ x2 . cfv (cv x0) cmsa) (λ x2 . co (cima (cfv (cv x0) cmuv) (csn (cfv (cv x2) (cfv (cv x0) c1st)))) (cixp (λ x3 . cfv (cv x2) (cfv (cv x0) cmvrs)) (λ x3 . cima (cfv (cv x0) cmuv) (csn (cfv (cv x3) (cfv (cv x0) cmty))))) cmap)) (λ x1 . crio (λ x2 . wral (λ x3 . w3a (wral (λ x4 . wbr (cop (cv x3) (cfv (cv x4) (cfv (cv x0) cmvh))) (cfv (cv x4) (cv x3)) (cv x2)) (λ x4 . cfv (cv x0) cmvar)) (∀ x4 x5 x6 . wbr (cv x4) (cop (cv x5) (cv x6)) (cfv (cv x0) cmst) ⟶ wbr (cop (cv x3) (cv x4)) (cfv (cmpt (λ x7 . cfv (cv x5) (cfv (cv x0) cmvrs)) (λ x7 . co (cv x3) (cfv (cfv (cv x7) (cfv (cv x0) cmvh)) (cv x6)) (cv x2))) (cv x1)) (cv x2)) (wral (λ x4 . wceq (cima (cv x2) (csn (cop (cv x3) (cv x4)))) (cin (cima (cv x2) (csn (cop (cv x3) (cfv (cv x4) (cfv (cv x0) cmesy))))) (cima (cfv (cv x0) cmuv) (csn (cfv (cv x4) c1st))))) (λ x4 . cfv (cv x0) cmex))) (λ x3 . cfv (cv x0) cmvl)) (λ x2 . co (cfv (cv x0) cmuv) (cxp (cfv (cv x0) cmvl) (cfv (cv x0) cmex)) cpm)))) (proof)
Theorem df_irng : wceq citr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . ciun (λ x2 . cfv (co (cv x0) (cv x1) cress) cmn1) (λ x2 . cima (ccnv (cv x2)) (csn (cfv (cv x0) c0g))))) (proof)
Theorem df_cplmet : wceq ccpms (cmpt (λ x0 . cvv) (λ x0 . csb (co (co (cv x0) cn cpws) (cfv (cfv (cv x0) cds) cca) cress) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . csb (copab (λ x3 x4 . wa (wss (cpr (cv x3) (cv x4)) (cv x2)) (wral (λ x5 . wrex (λ x6 . wf (cfv (cv x6) cuz) (co (cfv (cv x6) (cv x4)) (cv x5) (cfv (cfv (cv x0) cds) cbl)) (cres (cv x3) (cfv (cv x6) cuz))) (λ x6 . cz)) (λ x5 . crp)))) (λ x3 . co (co (cv x1) (cv x3) cqus) (csn (cop (cfv cnx cds) (coprab (λ x4 x5 x6 . wrex (λ x7 . wrex (λ x8 . wa (wa (wceq (cv x4) (cec (cv x7) (cv x3))) (wceq (cv x5) (cec (cv x8) (cv x3)))) (wbr (co (cv x7) (cv x8) (cof (cfv (cv x1) cds))) (cv x6) cli)) (λ x8 . cv x2)) (λ x7 . cv x2))))) csts))))) (proof)
Theorem df_homlimb : wceq chlb (cmpt (λ x0 . cvv) (λ x0 . csb (ciun (λ x1 . cn) (λ x1 . cxp (csn (cv x1)) (cdm (cfv (cv x1) (cv x0))))) (λ x1 . csb (cint (cab (λ x2 . wa (wer (cv x1) (cv x2)) (wss (cmpt (λ x3 . cv x1) (λ x3 . cop (co (cfv (cv x3) c1st) c1 caddc) (cfv (cfv (cv x3) c2nd) (cfv (cfv (cv x3) c1st) (cv x0))))) (cv x2))))) (λ x2 . cop (cqs (cv x1) (cv x2)) (cmpt (λ x3 . cn) (λ x3 . cmpt (λ x4 . cdm (cfv (cv x3) (cv x0))) (λ x4 . cec (cop (cv x3) (cv x4)) (cv x2)))))))) (proof)
Theorem df_homlim : wceq chlim (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cfv (cv x1) chlb) (λ x2 . csb (cfv (cv x2) c1st) (λ x3 . csb (cfv (cv x2) c2nd) (λ x4 . cun (ctp (cop (cfv cnx cbs) (cv x3)) (cop (cfv cnx cplusg) (ciun (λ x5 . cn) (λ x5 . crn (cmpt2 (λ x6 x7 . cdm (cfv (cv x5) (cv x4))) (λ x6 x7 . cdm (cfv (cv x5) (cv x4))) (λ x6 x7 . cop (cop (cfv (cv x6) (cfv (cv x5) (cv x4))) (cfv (cv x7) (cfv (cv x5) (cv x4)))) (cfv (co (cv x6) (cv x7) (cfv (cfv (cv x5) (cv x0)) cplusg)) (cfv (cv x5) (cv x4)))))))) (cop (cfv cnx cmulr) (ciun (λ x5 . cn) (λ x5 . crn (cmpt2 (λ x6 x7 . cdm (cfv (cv x5) (cv x4))) (λ x6 x7 . cdm (cfv (cv x5) (cv x4))) (λ x6 x7 . cop (cop (cfv (cv x6) (cfv (cv x5) (cv x4))) (cfv (cv x7) (cfv (cv x5) (cv x4)))) (cfv (co (cv x6) (cv x7) (cfv (cfv (cv x5) (cv x0)) cmulr)) (cfv (cv x5) (cv x4))))))))) (ctp (cop (cfv cnx ctopn) (crab (λ x5 . wral (λ x6 . wcel (cima (ccnv (cfv (cv x6) (cv x4))) (cv x5)) (cfv (cfv (cv x6) (cv x0)) ctopn)) (λ x6 . cn)) (λ x5 . cpw (cv x3)))) (cop (cfv cnx cds) (ciun (λ x5 . cn) (λ x5 . crn (cmpt2 (λ x6 x7 . cdm (cfv (cv x5) (cfv (cv x5) (cv x4)))) (λ x6 x7 . cdm (cfv (cv x5) (cfv (cv x5) (cv x4)))) (λ x6 x7 . cop (cop (cfv (cv x6) (cfv (cv x5) (cv x4))) (cfv (cv x7) (cfv (cv x5) (cv x4)))) (co (cv x6) (cv x7) (cfv (cfv (cv x5) (cv x0)) cds))))))) (cop (cfv cnx cple) (ciun (λ x5 . cn) (λ x5 . ccom (ccnv (cfv (cv x5) (cv x4))) (ccom (cfv (cfv (cv x5) (cv x0)) cple) (cfv (cv x5) (cv x4)))))))))))) (proof)
Theorem df_plfl : wceq cpfl (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cfv (cv x0) cpl1) (λ x2 . csb (cfv (csn (cv x1)) (cfv (cv x2) crsp)) (λ x3 . csb (cmpt (λ x4 . cfv (cv x0) cbs) (λ x4 . cec (co (cv x4) (cfv (cv x2) cur) (cfv (cv x2) cvsca)) (co (cv x2) (cv x3) cqg))) (λ x4 . cop (csb (co (cv x2) (co (cv x2) (cv x3) cqg) cqus) (λ x5 . co (co (cv x5) (crio (λ x6 . wceq (ccom (cv x6) (cv x4)) (cfv (cv x0) cnm)) (λ x6 . cfv (cv x5) cabv)) ctng) (cop (cfv cnx cple) (csb (cmpt (λ x6 . cfv (cv x5) cbs) (λ x6 . crio (λ x7 . wbr (co (cv x0) (cv x7) cdg1) (co (cv x0) (cv x1) cdg1) clt) (λ x7 . cv x6))) (λ x6 . ccom (ccnv (cv x6)) (ccom (cfv (cv x2) cple) (cv x6))))) csts)) (cv x4)))))) (proof)
Theorem df_sfl1 : wceq csf1 (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (cv x0) cpl1) (λ x2 . cfv (cfv (co c1 (co (cv x0) (cv x2) cdg1) cfz) ccrd) (crdg (cmpt2 (λ x3 x4 . cvv) (λ x3 x4 . cvv) (λ x3 x4 . csb (cfv (cv x3) cmpl) (λ x5 . csb (crab (λ x6 . wa (wbr (cv x6) (ccom (cv x2) (cv x4)) (cfv (cv x5) cdsr)) (wbr c1 (co (cv x3) (cv x6) cdg1) clt)) (λ x6 . cin (cfv (cv x3) cmn1) (cfv (cv x5) cir))) (λ x6 . cif (wo (wceq (ccom (cv x2) (cv x4)) (cfv (cv x5) c0g)) (wceq (cv x6) c0)) (cop (cv x3) (cv x4)) (csb (cfv (cv x6) cglb) (λ x7 . csb (co (cv x3) (cv x7) cpfl) (λ x8 . cop (cfv (cv x8) c1st) (ccom (cv x4) (cfv (cv x8) c2nd))))))))) (cv x1))))) (proof)
Theorem df_sfl : wceq csf (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cio (λ x2 . wex (λ x3 . wa (wiso (co c1 (cfv (cv x1) chash) cfz) (cv x1) clt (cfv (cv x0) cplt) (cv x3)) (wceq (cv x2) (cfv (cfv (cv x1) chash) (cseq (cmpt2 (λ x4 x5 . cvv) (λ x4 x5 . cvv) (λ x4 x5 . cfv (cv x5) (co (cv x0) (cv x4) csf1))) (cun (cv x3) (csn (cop cc0 (cop (cv x0) (cres cid (cfv (cv x0) cbs)))))) cc0))))))) (proof)
Theorem df_psl : wceq cpsl (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . co (cin (cpw (cfv (cv x0) cbs)) cfn) cn cmap) (λ x0 x1 . csb (ccom c1st (cseq (cmpt2 (λ x2 x3 . cvv) (λ x2 x3 . cvv) (λ x2 x3 . csb (cfv (cv x2) c1st) (λ x4 . csb (cfv (cv x4) c1st) (λ x5 . csb (co (cv x5) (crn (cmpt (λ x6 . cv x3) (λ x6 . ccom (cv x6) (cfv (cv x2) c2nd)))) csf) (λ x6 . cop (cv x6) (ccom (cfv (cv x2) c2nd) (cfv (cv x6) c2nd))))))) (cun (cv x1) (csn (cop cc0 (cop (cop (cv x0) c0) (cres cid (cfv (cv x0) cbs)))))) cc0)) (λ x2 . co (ccom c1st (co (cv x2) c1 cshi)) (ccom c2nd (cv x2)) chlim))) (proof)

Proofgold Address