Proofgold Address

Known df_cph__df_tch__df_cfil__df_cau__df_cmet__df_cms__df_bn__df_hl__df_rrx__df_ehl__df_ovol__df_vol__df_mbf__df_itg1__df_itg2__df_ibl__df_itg__df_0p : ∀ x0 : ο . (wceq ccph (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . w3a (wceq (cv x2) (co ccnfld (cv x3) cress)) (wss (cima csqrt (cin (cv x3) (co cc0 cpnf cico))) (cv x3)) (wceq (cfv (cv x1) cnm) (cmpt (λ x4 . cfv (cv x1) cbs) (λ x4 . cfv (co (cv x4) (cv x4) (cfv (cv x1) cip)) csqrt)))) (cfv (cv x2) cbs)) (cfv (cv x1) csca)) (λ x1 . cin cphl cnlm)) ⟶ wceq ctch (cmpt (λ x1 . cvv) (λ x1 . co (cv x1) (cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . cfv (co (cv x2) (cv x2) (cfv (cv x1) cip)) csqrt)) ctng)) ⟶ wceq ccfil (cmpt (λ x1 . cuni (crn cxmt)) (λ x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wss (cima (cv x1) (cxp (cv x4) (cv x4))) (co cc0 (cv x3) cico)) (λ x4 . cv x2)) (λ x3 . crp)) (λ x2 . cfv (cdm (cdm (cv x1))) cfil))) ⟶ wceq cca (cmpt (λ x1 . cuni (crn cxmt)) (λ x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wf (cfv (cv x4) cuz) (co (cfv (cv x4) (cv x2)) (cv x3) (cfv (cv x1) cbl)) (cres (cv x2) (cfv (cv x4) cuz))) (λ x4 . cz)) (λ x3 . crp)) (λ x2 . co (cdm (cdm (cv x1))) cc cpm))) ⟶ wceq cms (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wne (co (cfv (cv x2) cmopn) (cv x3) cflim) c0) (λ x3 . cfv (cv x2) ccfil)) (λ x2 . cfv (cv x1) cme))) ⟶ wceq ccms (crab (λ x1 . wsbc (λ x2 . wcel (cres (cfv (cv x1) cds) (cxp (cv x2) (cv x2))) (cfv (cv x2) cms)) (cfv (cv x1) cbs)) (λ x1 . cmt)) ⟶ wceq cbn (crab (λ x1 . wcel (cfv (cv x1) csca) ccms) (λ x1 . cin cnvc ccms)) ⟶ wceq chl (cin cbn ccph) ⟶ wceq crrx (cmpt (λ x1 . cvv) (λ x1 . cfv (co crefld (cv x1) cfrlm) ctch)) ⟶ wceq cehl (cmpt (λ x1 . cn0) (λ x1 . cfv (co c1 (cv x1) cfz) crrx)) ⟶ wceq covol (cmpt (λ x1 . cpw cr) (λ x1 . cinf (crab (λ x2 . wrex (λ x3 . wa (wss (cv x1) (cuni (crn (ccom cioo (cv x3))))) (wceq (cv x2) (csup (crn (cseq caddc (ccom (ccom cabs cmin) (cv x3)) c1)) cxr clt))) (λ x3 . co (cin cle (cxp cr cr)) cn cmap)) (λ x2 . cxr)) cxr clt)) ⟶ wceq cvol (cres covol (cab (λ x1 . wral (λ x2 . wceq (cfv (cv x2) covol) (co (cfv (cin (cv x2) (cv x1)) covol) (cfv (cdif (cv x2) (cv x1)) covol) caddc)) (λ x2 . cima (ccnv covol) cr)))) ⟶ wceq cmbf (crab (λ x1 . wral (λ x2 . wa (wcel (cima (ccnv (ccom cre (cv x1))) (cv x2)) (cdm cvol)) (wcel (cima (ccnv (ccom cim (cv x1))) (cv x2)) (cdm cvol))) (λ x2 . crn cioo)) (λ x1 . co cc cr cpm)) ⟶ wceq citg1 (cmpt (λ x1 . crab (λ x2 . w3a (wf cr cr (cv x2)) (wcel (crn (cv x2)) cfn) (wcel (cfv (cima (ccnv (cv x2)) (cdif cr (csn cc0))) cvol) cr)) (λ x2 . cmbf)) (λ x1 . csu (cdif (crn (cv x1)) (csn cc0)) (λ x2 . co (cv x2) (cfv (cima (ccnv (cv x1)) (csn (cv x2))) cvol) cmul))) ⟶ wceq citg2 (cmpt (λ x1 . co (co cc0 cpnf cicc) cr cmap) (λ x1 . csup (cab (λ x2 . wrex (λ x3 . wa (wbr (cv x3) (cv x1) (cofr cle)) (wceq (cv x2) (cfv (cv x3) citg1))) (λ x3 . cdm citg1))) cxr clt)) ⟶ wceq cibl (crab (λ x1 . wral (λ x2 . wcel (cfv (cmpt (λ x3 . cr) (λ x3 . csb (cfv (co (cfv (cv x3) (cv x1)) (co ci (cv x2) cexp) cdiv) cre) (λ x4 . cif (wa (wcel (cv x3) (cdm (cv x1))) (wbr cc0 (cv x4) cle)) (cv x4) cc0))) citg2) cr) (λ x2 . co cc0 c3 cfz)) (λ x1 . cmbf)) ⟶ (∀ x1 x2 : ι → ι → ο . wceq (citg x1 x2) (csu (co cc0 c3 cfz) (λ x3 . co (co ci (cv x3) cexp) (cfv (cmpt (λ x4 . cr) (λ x4 . csb (cfv (co (x2 x4) (co ci (cv x3) cexp) cdiv) cre) (λ x5 . cif (wa (wcel (cv x4) (x1 x4)) (wbr cc0 (cv x5) cle)) (cv x5) cc0))) citg2) cmul))) ⟶ wceq c0p (cxp cc (csn cc0)) ⟶ x0) ⟶ x0
Theorem df_cph : wceq ccph (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . w3a (wceq (cv x1) (co ccnfld (cv x2) cress)) (wss (cima csqrt (cin (cv x2) (co cc0 cpnf cico))) (cv x2)) (wceq (cfv (cv x0) cnm) (cmpt (λ x3 . cfv (cv x0) cbs) (λ x3 . cfv (co (cv x3) (cv x3) (cfv (cv x0) cip)) csqrt)))) (cfv (cv x1) cbs)) (cfv (cv x0) csca)) (λ x0 . cin cphl cnlm)) (proof)
Theorem df_tch : wceq ctch (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . cfv (co (cv x1) (cv x1) (cfv (cv x0) cip)) csqrt)) ctng)) (proof)
Theorem df_cfil : wceq ccfil (cmpt (λ x0 . cuni (crn cxmt)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wss (cima (cv x0) (cxp (cv x3) (cv x3))) (co cc0 (cv x2) cico)) (λ x3 . cv x1)) (λ x2 . crp)) (λ x1 . cfv (cdm (cdm (cv x0))) cfil))) (proof)
Theorem df_cau : wceq cca (cmpt (λ x0 . cuni (crn cxmt)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wf (cfv (cv x3) cuz) (co (cfv (cv x3) (cv x1)) (cv x2) (cfv (cv x0) cbl)) (cres (cv x1) (cfv (cv x3) cuz))) (λ x3 . cz)) (λ x2 . crp)) (λ x1 . co (cdm (cdm (cv x0))) cc cpm))) (proof)
Theorem df_cmet : wceq cms (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wne (co (cfv (cv x1) cmopn) (cv x2) cflim) c0) (λ x2 . cfv (cv x1) ccfil)) (λ x1 . cfv (cv x0) cme))) (proof)
Theorem df_cms : wceq ccms (crab (λ x0 . wsbc (λ x1 . wcel (cres (cfv (cv x0) cds) (cxp (cv x1) (cv x1))) (cfv (cv x1) cms)) (cfv (cv x0) cbs)) (λ x0 . cmt)) (proof)
Theorem df_bn : wceq cbn (crab (λ x0 . wcel (cfv (cv x0) csca) ccms) (λ x0 . cin cnvc ccms)) (proof)
Theorem df_hl : wceq chl (cin cbn ccph) (proof)
Theorem df_rrx : wceq crrx (cmpt (λ x0 . cvv) (λ x0 . cfv (co crefld (cv x0) cfrlm) ctch)) (proof)
Theorem df_ehl : wceq cehl (cmpt (λ x0 . cn0) (λ x0 . cfv (co c1 (cv x0) cfz) crrx)) (proof)
Theorem df_ovol : wceq covol (cmpt (λ x0 . cpw cr) (λ x0 . cinf (crab (λ x1 . wrex (λ x2 . wa (wss (cv x0) (cuni (crn (ccom cioo (cv x2))))) (wceq (cv x1) (csup (crn (cseq caddc (ccom (ccom cabs cmin) (cv x2)) c1)) cxr clt))) (λ x2 . co (cin cle (cxp cr cr)) cn cmap)) (λ x1 . cxr)) cxr clt)) (proof)
Theorem df_vol : wceq cvol (cres covol (cab (λ x0 . wral (λ x1 . wceq (cfv (cv x1) covol) (co (cfv (cin (cv x1) (cv x0)) covol) (cfv (cdif (cv x1) (cv x0)) covol) caddc)) (λ x1 . cima (ccnv covol) cr)))) (proof)
Theorem df_mbf : wceq cmbf (crab (λ x0 . wral (λ x1 . wa (wcel (cima (ccnv (ccom cre (cv x0))) (cv x1)) (cdm cvol)) (wcel (cima (ccnv (ccom cim (cv x0))) (cv x1)) (cdm cvol))) (λ x1 . crn cioo)) (λ x0 . co cc cr cpm)) (proof)
Theorem df_itg1 : wceq citg1 (cmpt (λ x0 . crab (λ x1 . w3a (wf cr cr (cv x1)) (wcel (crn (cv x1)) cfn) (wcel (cfv (cima (ccnv (cv x1)) (cdif cr (csn cc0))) cvol) cr)) (λ x1 . cmbf)) (λ x0 . csu (cdif (crn (cv x0)) (csn cc0)) (λ x1 . co (cv x1) (cfv (cima (ccnv (cv x0)) (csn (cv x1))) cvol) cmul))) (proof)
Theorem df_itg2 : wceq citg2 (cmpt (λ x0 . co (co cc0 cpnf cicc) cr cmap) (λ x0 . csup (cab (λ x1 . wrex (λ x2 . wa (wbr (cv x2) (cv x0) (cofr cle)) (wceq (cv x1) (cfv (cv x2) citg1))) (λ x2 . cdm citg1))) cxr clt)) (proof)
Theorem df_ibl : wceq cibl (crab (λ x0 . wral (λ x1 . wcel (cfv (cmpt (λ x2 . cr) (λ x2 . csb (cfv (co (cfv (cv x2) (cv x0)) (co ci (cv x1) cexp) cdiv) cre) (λ x3 . cif (wa (wcel (cv x2) (cdm (cv x0))) (wbr cc0 (cv x3) cle)) (cv x3) cc0))) citg2) cr) (λ x1 . co cc0 c3 cfz)) (λ x0 . cmbf)) (proof)
Theorem df_itg : ∀ x0 x1 : ι → ι → ο . wceq (citg x0 x1) (csu (co cc0 c3 cfz) (λ x2 . co (co ci (cv x2) cexp) (cfv (cmpt (λ x3 . cr) (λ x3 . csb (cfv (co (x1 x3) (co ci (cv x2) cexp) cdiv) cre) (λ x4 . cif (wa (wcel (cv x3) (x0 x3)) (wbr cc0 (cv x4) cle)) (cv x4) cc0))) citg2) cmul)) (proof)
Theorem df_0p : wceq c0p (cxp cc (csn cc0)) (proof)