Proofgold Address

Known df_docaN__df_djaN__df_dib__df_dic__df_dih__df_doch__df_djh__df_lpolN__df_lcdual__df_mapd__df_hvmap__df_hdmap1__df_hdmap__df_hgmap__df_hlhil__df_nacs__df_mzpcl__df_mzp : ∀ x0 : ο . (wceq cocaN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . cpw (cfv (cv x2) (cfv (cv x1) cltrn))) (λ x3 . cfv (co (co (cfv (cfv (cint (crab (λ x4 . wss (cv x3) (cv x4)) (λ x4 . crn (cfv (cv x2) (cfv (cv x1) cdia))))) (ccnv (cfv (cv x2) (cfv (cv x1) cdia)))) (cfv (cv x1) coc)) (cfv (cv x2) (cfv (cv x1) coc)) (cfv (cv x1) cjn)) (cv x2) (cfv (cv x1) cmee)) (cfv (cv x2) (cfv (cv x1) cdia)))))) ⟶ wceq cdjaN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt2 (λ x3 x4 . cpw (cfv (cv x2) (cfv (cv x1) cltrn))) (λ x3 x4 . cpw (cfv (cv x2) (cfv (cv x1) cltrn))) (λ x3 x4 . cfv (cin (cfv (cv x3) (cfv (cv x2) (cfv (cv x1) cocaN))) (cfv (cv x4) (cfv (cv x2) (cfv (cv x1) cocaN)))) (cfv (cv x2) (cfv (cv x1) cocaN)))))) ⟶ wceq cdib (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . cdm (cfv (cv x2) (cfv (cv x1) cdia))) (λ x3 . cxp (cfv (cv x3) (cfv (cv x2) (cfv (cv x1) cdia))) (csn (cmpt (λ x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x4 . cres cid (cfv (cv x1) cbs)))))))) ⟶ wceq cdic (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . crab (λ x4 . wn (wbr (cv x4) (cv x2) (cfv (cv x1) cple))) (λ x4 . cfv (cv x1) catm)) (λ x3 . copab (λ x4 x5 . wa (wceq (cv x4) (cfv (crio (λ x6 . wceq (cfv (cfv (cv x2) (cfv (cv x1) coc)) (cv x6)) (cv x3)) (λ x6 . cfv (cv x2) (cfv (cv x1) cltrn))) (cv x5))) (wcel (cv x5) (cfv (cv x2) (cfv (cv x1) ctendo)))))))) ⟶ wceq cdih (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . cfv (cv x1) cbs) (λ x3 . cif (wbr (cv x3) (cv x2) (cfv (cv x1) cple)) (cfv (cv x3) (cfv (cv x2) (cfv (cv x1) cdib))) (crio (λ x4 . wral (λ x5 . wa (wn (wbr (cv x5) (cv x2) (cfv (cv x1) cple))) (wceq (co (cv x5) (co (cv x3) (cv x2) (cfv (cv x1) cmee)) (cfv (cv x1) cjn)) (cv x3)) ⟶ wceq (cv x4) (co (cfv (cv x5) (cfv (cv x2) (cfv (cv x1) cdic))) (cfv (co (cv x3) (cv x2) (cfv (cv x1) cmee)) (cfv (cv x2) (cfv (cv x1) cdib))) (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clsm))) (λ x5 . cfv (cv x1) catm)) (λ x4 . cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clss)))))) ⟶ wceq coch (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . cpw (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) cbs)) (λ x3 . cfv (cfv (cfv (crab (λ x4 . wss (cv x3) (cfv (cv x4) (cfv (cv x2) (cfv (cv x1) cdih)))) (λ x4 . cfv (cv x1) cbs)) (cfv (cv x1) cglb)) (cfv (cv x1) coc)) (cfv (cv x2) (cfv (cv x1) cdih)))))) ⟶ wceq cdjh (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt2 (λ x3 x4 . cpw (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) cbs)) (λ x3 x4 . cpw (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) cbs)) (λ x3 x4 . cfv (cin (cfv (cv x3) (cfv (cv x2) (cfv (cv x1) coch))) (cfv (cv x4) (cfv (cv x2) (cfv (cv x1) coch)))) (cfv (cv x2) (cfv (cv x1) coch)))))) ⟶ wceq clpoN (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . w3a (wceq (cfv (cfv (cv x1) cbs) (cv x2)) (csn (cfv (cv x1) c0g))) (∀ x3 x4 . w3a (wss (cv x3) (cfv (cv x1) cbs)) (wss (cv x4) (cfv (cv x1) cbs)) (wss (cv x3) (cv x4)) ⟶ wss (cfv (cv x4) (cv x2)) (cfv (cv x3) (cv x2))) (wral (λ x3 . wa (wcel (cfv (cv x3) (cv x2)) (cfv (cv x1) clsh)) (wceq (cfv (cfv (cv x3) (cv x2)) (cv x2)) (cv x3))) (λ x3 . cfv (cv x1) clsa))) (λ x2 . co (cfv (cv x1) clss) (cpw (cfv (cv x1) cbs)) cmap))) ⟶ wceq clcd (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . co (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) cld) (crab (λ x3 . wceq (cfv (cfv (cfv (cv x3) (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clk)) (cfv (cv x2) (cfv (cv x1) coch))) (cfv (cv x2) (cfv (cv x1) coch))) (cfv (cv x3) (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clk))) (λ x3 . cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clfn)) cress))) ⟶ wceq cmpd (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clss) (λ x3 . crab (λ x4 . wa (wceq (cfv (cfv (cfv (cv x4) (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clk)) (cfv (cv x2) (cfv (cv x1) coch))) (cfv (cv x2) (cfv (cv x1) coch))) (cfv (cv x4) (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clk))) (wss (cfv (cfv (cv x4) (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clk)) (cfv (cv x2) (cfv (cv x1) coch))) (cv x3))) (λ x4 . cfv (cfv (cv x2) (cfv (cv x1) cdvh)) clfn))))) ⟶ wceq chvm (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . cdif (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) cbs) (csn (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) c0g))) (λ x3 . cmpt (λ x4 . cfv (cfv (cv x2) (cfv (cv x1) cdvh)) cbs) (λ x4 . crio (λ x5 . wrex (λ x6 . wceq (cv x4) (co (cv x6) (co (cv x5) (cv x3) (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) cvsca)) (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) cplusg))) (λ x6 . cfv (csn (cv x3)) (cfv (cv x2) (cfv (cv x1) coch)))) (λ x5 . cfv (cfv (cfv (cv x2) (cfv (cv x1) cdvh)) csca) cbs)))))) ⟶ wceq chdma1 (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cab (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wsbc (λ x8 . wsbc (λ x9 . wsbc (λ x10 . wcel (cv x3) (cmpt (λ x11 . cxp (cxp (cv x5) (cv x8)) (cv x5)) (λ x11 . cif (wceq (cfv (cv x11) c2nd) (cfv (cv x4) c0g)) (cfv (cv x7) c0g) (crio (λ x12 . wa (wceq (cfv (cfv (csn (cfv (cv x11) c2nd)) (cv x6)) (cv x10)) (cfv (csn (cv x12)) (cv x9))) (wceq (cfv (cfv (csn (co (cfv (cfv (cv x11) c1st) c1st) (cfv (cv x11) c2nd) (cfv (cv x4) csg))) (cv x6)) (cv x10)) (cfv (csn (co (cfv (cfv (cv x11) c1st) c2nd) (cv x12) (cfv (cv x7) csg))) (cv x9)))) (λ x12 . cv x8))))) (cfv (cv x2) (cfv (cv x1) cmpd))) (cfv (cv x7) clspn)) (cfv (cv x7) cbs)) (cfv (cv x2) (cfv (cv x1) clcd))) (cfv (cv x4) clspn)) (cfv (cv x4) cbs)) (cfv (cv x2) (cfv (cv x1) cdvh)))))) ⟶ wceq chdma (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cab (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wcel (cv x3) (cmpt (λ x8 . cv x6) (λ x8 . crio (λ x9 . wral (λ x10 . wn (wcel (cv x10) (cun (cfv (csn (cv x4)) (cfv (cv x5) clspn)) (cfv (csn (cv x8)) (cfv (cv x5) clspn)))) ⟶ wceq (cv x9) (cfv (cotp (cv x10) (cfv (cotp (cv x4) (cfv (cv x4) (cfv (cv x2) (cfv (cv x1) chvm))) (cv x10)) (cv x7)) (cv x8)) (cv x7))) (λ x10 . cv x6)) (λ x9 . cfv (cfv (cv x2) (cfv (cv x1) clcd)) cbs)))) (cfv (cv x2) (cfv (cv x1) chdma1))) (cfv (cv x5) cbs)) (cfv (cv x2) (cfv (cv x1) cdvh))) (cop (cres cid (cfv (cv x1) cbs)) (cres cid (cfv (cv x2) (cfv (cv x1) cltrn)))))))) ⟶ wceq chg (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cab (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wcel (cv x3) (cmpt (λ x7 . cv x5) (λ x7 . crio (λ x8 . wral (λ x9 . wceq (cfv (co (cv x7) (cv x9) (cfv (cv x4) cvsca)) (cv x6)) (co (cv x8) (cfv (cv x9) (cv x6)) (cfv (cfv (cv x2) (cfv (cv x1) clcd)) cvsca))) (λ x9 . cfv (cv x4) cbs)) (λ x8 . cv x5)))) (cfv (cv x2) (cfv (cv x1) chdma))) (cfv (cfv (cv x4) csca) cbs)) (cfv (cv x2) (cfv (cv x1) cdvh)))))) ⟶ wceq chlh (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . csb (cfv (cv x2) (cfv (cv x1) cdvh)) (λ x3 . csb (cfv (cv x3) cbs) (λ x4 . cun (ctp (cop (cfv cnx cbs) (cv x4)) (cop (cfv cnx cplusg) (cfv (cv x3) cplusg)) (cop (cfv cnx csca) (co (cfv (cv x2) (cfv (cv x1) cedring)) (cop (cfv cnx cstv) (cfv (cv x2) (cfv (cv x1) chg))) csts))) (cpr (cop (cfv cnx cvsca) (cfv (cv x3) cvsca)) (cop (cfv cnx cip) (cmpt2 (λ x5 x6 . cv x4) (λ x5 x6 . cv x4) (λ x5 x6 . cfv (cv x5) (cfv (cv x6) (cfv (cv x2) (cfv (cv x1) chdma)))))))))))) ⟶ wceq cnacs (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wceq (cv x3) (cfv (cv x4) (cfv (cv x2) cmrc))) (λ x4 . cin (cpw (cv x1)) cfn)) (λ x3 . cv x2)) (λ x2 . cfv (cv x1) cacs))) ⟶ wceq cmzpcl (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wa (wral (λ x3 . wcel (cxp (co cz (cv x1) cmap) (csn (cv x3))) (cv x2)) (λ x3 . cz)) (wral (λ x3 . wcel (cmpt (λ x4 . co cz (cv x1) cmap) (λ x4 . cfv (cv x3) (cv x4))) (cv x2)) (λ x3 . cv x1))) (wral (λ x3 . wral (λ x4 . wa (wcel (co (cv x3) (cv x4) (cof caddc)) (cv x2)) (wcel (co (cv x3) (cv x4) (cof cmul)) (cv x2))) (λ x4 . cv x2)) (λ x3 . cv x2))) (λ x2 . cpw (co cz (co cz (cv x1) cmap) cmap)))) ⟶ wceq cmzp (cmpt (λ x1 . cvv) (λ x1 . cint (cfv (cv x1) cmzpcl))) ⟶ x0) ⟶ x0
Theorem df_docaN : wceq cocaN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) (cfv (cv x0) cltrn))) (λ x2 . cfv (co (co (cfv (cfv (cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . crn (cfv (cv x1) (cfv (cv x0) cdia))))) (ccnv (cfv (cv x1) (cfv (cv x0) cdia)))) (cfv (cv x0) coc)) (cfv (cv x1) (cfv (cv x0) coc)) (cfv (cv x0) cjn)) (cv x1) (cfv (cv x0) cmee)) (cfv (cv x1) (cfv (cv x0) cdia)))))) (proof)
Theorem df_djaN : wceq cdjaN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt2 (λ x2 x3 . cpw (cfv (cv x1) (cfv (cv x0) cltrn))) (λ x2 x3 . cpw (cfv (cv x1) (cfv (cv x0) cltrn))) (λ x2 x3 . cfv (cin (cfv (cv x2) (cfv (cv x1) (cfv (cv x0) cocaN))) (cfv (cv x3) (cfv (cv x1) (cfv (cv x0) cocaN)))) (cfv (cv x1) (cfv (cv x0) cocaN)))))) (proof)
Theorem df_dib : wceq cdib (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . cdm (cfv (cv x1) (cfv (cv x0) cdia))) (λ x2 . cxp (cfv (cv x2) (cfv (cv x1) (cfv (cv x0) cdia))) (csn (cmpt (λ x3 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x3 . cres cid (cfv (cv x0) cbs)))))))) (proof)
Theorem df_dic : wceq cdic (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . crab (λ x3 . wn (wbr (cv x3) (cv x1) (cfv (cv x0) cple))) (λ x3 . cfv (cv x0) catm)) (λ x2 . copab (λ x3 x4 . wa (wceq (cv x3) (cfv (crio (λ x5 . wceq (cfv (cfv (cv x1) (cfv (cv x0) coc)) (cv x5)) (cv x2)) (λ x5 . cfv (cv x1) (cfv (cv x0) cltrn))) (cv x4))) (wcel (cv x4) (cfv (cv x1) (cfv (cv x0) ctendo)))))))) (proof)
Theorem df_dih : wceq cdih (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . cfv (cv x0) cbs) (λ x2 . cif (wbr (cv x2) (cv x1) (cfv (cv x0) cple)) (cfv (cv x2) (cfv (cv x1) (cfv (cv x0) cdib))) (crio (λ x3 . wral (λ x4 . wa (wn (wbr (cv x4) (cv x1) (cfv (cv x0) cple))) (wceq (co (cv x4) (co (cv x2) (cv x1) (cfv (cv x0) cmee)) (cfv (cv x0) cjn)) (cv x2)) ⟶ wceq (cv x3) (co (cfv (cv x4) (cfv (cv x1) (cfv (cv x0) cdic))) (cfv (co (cv x2) (cv x1) (cfv (cv x0) cmee)) (cfv (cv x1) (cfv (cv x0) cdib))) (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clsm))) (λ x4 . cfv (cv x0) catm)) (λ x3 . cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clss)))))) (proof)
Theorem df_doch : wceq coch (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . cpw (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) cbs)) (λ x2 . cfv (cfv (cfv (crab (λ x3 . wss (cv x2) (cfv (cv x3) (cfv (cv x1) (cfv (cv x0) cdih)))) (λ x3 . cfv (cv x0) cbs)) (cfv (cv x0) cglb)) (cfv (cv x0) coc)) (cfv (cv x1) (cfv (cv x0) cdih)))))) (proof)
Theorem df_djh : wceq cdjh (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt2 (λ x2 x3 . cpw (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) cbs)) (λ x2 x3 . cpw (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) cbs)) (λ x2 x3 . cfv (cin (cfv (cv x2) (cfv (cv x1) (cfv (cv x0) coch))) (cfv (cv x3) (cfv (cv x1) (cfv (cv x0) coch)))) (cfv (cv x1) (cfv (cv x0) coch)))))) (proof)
Theorem df_lpolN : wceq clpoN (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . w3a (wceq (cfv (cfv (cv x0) cbs) (cv x1)) (csn (cfv (cv x0) c0g))) (∀ x2 x3 . w3a (wss (cv x2) (cfv (cv x0) cbs)) (wss (cv x3) (cfv (cv x0) cbs)) (wss (cv x2) (cv x3)) ⟶ wss (cfv (cv x3) (cv x1)) (cfv (cv x2) (cv x1))) (wral (λ x2 . wa (wcel (cfv (cv x2) (cv x1)) (cfv (cv x0) clsh)) (wceq (cfv (cfv (cv x2) (cv x1)) (cv x1)) (cv x2))) (λ x2 . cfv (cv x0) clsa))) (λ x1 . co (cfv (cv x0) clss) (cpw (cfv (cv x0) cbs)) cmap))) (proof)
Theorem df_lcdual : wceq clcd (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . co (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) cld) (crab (λ x2 . wceq (cfv (cfv (cfv (cv x2) (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clk)) (cfv (cv x1) (cfv (cv x0) coch))) (cfv (cv x1) (cfv (cv x0) coch))) (cfv (cv x2) (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clk))) (λ x2 . cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clfn)) cress))) (proof)
Theorem df_mapd : wceq cmpd (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clss) (λ x2 . crab (λ x3 . wa (wceq (cfv (cfv (cfv (cv x3) (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clk)) (cfv (cv x1) (cfv (cv x0) coch))) (cfv (cv x1) (cfv (cv x0) coch))) (cfv (cv x3) (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clk))) (wss (cfv (cfv (cv x3) (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clk)) (cfv (cv x1) (cfv (cv x0) coch))) (cv x2))) (λ x3 . cfv (cfv (cv x1) (cfv (cv x0) cdvh)) clfn))))) (proof)
Theorem df_hvmap : wceq chvm (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . cdif (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) cbs) (csn (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) c0g))) (λ x2 . cmpt (λ x3 . cfv (cfv (cv x1) (cfv (cv x0) cdvh)) cbs) (λ x3 . crio (λ x4 . wrex (λ x5 . wceq (cv x3) (co (cv x5) (co (cv x4) (cv x2) (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) cvsca)) (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) cplusg))) (λ x5 . cfv (csn (cv x2)) (cfv (cv x1) (cfv (cv x0) coch)))) (λ x4 . cfv (cfv (cfv (cv x1) (cfv (cv x0) cdvh)) csca) cbs)))))) (proof)
Theorem df_hdmap1 : wceq chdma1 (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cab (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wsbc (λ x8 . wsbc (λ x9 . wcel (cv x2) (cmpt (λ x10 . cxp (cxp (cv x4) (cv x7)) (cv x4)) (λ x10 . cif (wceq (cfv (cv x10) c2nd) (cfv (cv x3) c0g)) (cfv (cv x6) c0g) (crio (λ x11 . wa (wceq (cfv (cfv (csn (cfv (cv x10) c2nd)) (cv x5)) (cv x9)) (cfv (csn (cv x11)) (cv x8))) (wceq (cfv (cfv (csn (co (cfv (cfv (cv x10) c1st) c1st) (cfv (cv x10) c2nd) (cfv (cv x3) csg))) (cv x5)) (cv x9)) (cfv (csn (co (cfv (cfv (cv x10) c1st) c2nd) (cv x11) (cfv (cv x6) csg))) (cv x8)))) (λ x11 . cv x7))))) (cfv (cv x1) (cfv (cv x0) cmpd))) (cfv (cv x6) clspn)) (cfv (cv x6) cbs)) (cfv (cv x1) (cfv (cv x0) clcd))) (cfv (cv x3) clspn)) (cfv (cv x3) cbs)) (cfv (cv x1) (cfv (cv x0) cdvh)))))) (proof)
Theorem df_hdmap : wceq chdma (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cab (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wcel (cv x2) (cmpt (λ x7 . cv x5) (λ x7 . crio (λ x8 . wral (λ x9 . wn (wcel (cv x9) (cun (cfv (csn (cv x3)) (cfv (cv x4) clspn)) (cfv (csn (cv x7)) (cfv (cv x4) clspn)))) ⟶ wceq (cv x8) (cfv (cotp (cv x9) (cfv (cotp (cv x3) (cfv (cv x3) (cfv (cv x1) (cfv (cv x0) chvm))) (cv x9)) (cv x6)) (cv x7)) (cv x6))) (λ x9 . cv x5)) (λ x8 . cfv (cfv (cv x1) (cfv (cv x0) clcd)) cbs)))) (cfv (cv x1) (cfv (cv x0) chdma1))) (cfv (cv x4) cbs)) (cfv (cv x1) (cfv (cv x0) cdvh))) (cop (cres cid (cfv (cv x0) cbs)) (cres cid (cfv (cv x1) (cfv (cv x0) cltrn)))))))) (proof)
Theorem df_hgmap : wceq chg (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cab (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wcel (cv x2) (cmpt (λ x6 . cv x4) (λ x6 . crio (λ x7 . wral (λ x8 . wceq (cfv (co (cv x6) (cv x8) (cfv (cv x3) cvsca)) (cv x5)) (co (cv x7) (cfv (cv x8) (cv x5)) (cfv (cfv (cv x1) (cfv (cv x0) clcd)) cvsca))) (λ x8 . cfv (cv x3) cbs)) (λ x7 . cv x4)))) (cfv (cv x1) (cfv (cv x0) chdma))) (cfv (cfv (cv x3) csca) cbs)) (cfv (cv x1) (cfv (cv x0) cdvh)))))) (proof)
Theorem df_hlhil : wceq chlh (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . csb (cfv (cv x1) (cfv (cv x0) cdvh)) (λ x2 . csb (cfv (cv x2) cbs) (λ x3 . cun (ctp (cop (cfv cnx cbs) (cv x3)) (cop (cfv cnx cplusg) (cfv (cv x2) cplusg)) (cop (cfv cnx csca) (co (cfv (cv x1) (cfv (cv x0) cedring)) (cop (cfv cnx cstv) (cfv (cv x1) (cfv (cv x0) chg))) csts))) (cpr (cop (cfv cnx cvsca) (cfv (cv x2) cvsca)) (cop (cfv cnx cip) (cmpt2 (λ x4 x5 . cv x3) (λ x4 x5 . cv x3) (λ x4 x5 . cfv (cv x4) (cfv (cv x5) (cfv (cv x1) (cfv (cv x0) chdma)))))))))))) (proof)
Theorem df_nacs : wceq cnacs (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wceq (cv x2) (cfv (cv x3) (cfv (cv x1) cmrc))) (λ x3 . cin (cpw (cv x0)) cfn)) (λ x2 . cv x1)) (λ x1 . cfv (cv x0) cacs))) (proof)
Theorem df_mzpcl : wceq cmzpcl (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wa (wral (λ x2 . wcel (cxp (co cz (cv x0) cmap) (csn (cv x2))) (cv x1)) (λ x2 . cz)) (wral (λ x2 . wcel (cmpt (λ x3 . co cz (cv x0) cmap) (λ x3 . cfv (cv x2) (cv x3))) (cv x1)) (λ x2 . cv x0))) (wral (λ x2 . wral (λ x3 . wa (wcel (co (cv x2) (cv x3) (cof caddc)) (cv x1)) (wcel (co (cv x2) (cv x3) (cof cmul)) (cv x1))) (λ x3 . cv x1)) (λ x2 . cv x1))) (λ x1 . cpw (co cz (co cz (cv x0) cmap) cmap)))) (proof)
Theorem df_mzp : wceq cmzp (cmpt (λ x0 . cvv) (λ x0 . cint (cfv (cv x0) cmzpcl))) (proof)