Proofgold Address

Known df_dip__df_ssp__df_lno__df_nmoo__df_blo__df_0o__df_aj__df_hmo__df_ph__df_cbn__df_hlo__df_hnorm__df_hba__df_h0v__df_hvsub__df_hlim__df_hcau__ax_hilex : ∀ x0 : ο . (wceq cdip (cmpt (λ x1 . cnv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cba) (λ x2 x3 . cfv (cv x1) cba) (λ x2 x3 . co (csu (co c1 c4 cfz) (λ x4 . co (co ci (cv x4) cexp) (co (cfv (co (cv x2) (co (co ci (cv x4) cexp) (cv x3) (cfv (cv x1) cns)) (cfv (cv x1) cpv)) (cfv (cv x1) cnmcv)) c2 cexp) cmul)) c4 cdiv))) ⟶ wceq css (cmpt (λ x1 . cnv) (λ x1 . crab (λ x2 . w3a (wss (cfv (cv x2) cpv) (cfv (cv x1) cpv)) (wss (cfv (cv x2) cns) (cfv (cv x1) cns)) (wss (cfv (cv x2) cnmcv) (cfv (cv x1) cnmcv))) (λ x2 . cnv))) ⟶ wceq clno (cmpt2 (λ x1 x2 . cnv) (λ x1 x2 . cnv) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wceq (cfv (co (co (cv x4) (cv x5) (cfv (cv x1) cns)) (cv x6) (cfv (cv x1) cpv)) (cv x3)) (co (co (cv x4) (cfv (cv x5) (cv x3)) (cfv (cv x2) cns)) (cfv (cv x6) (cv x3)) (cfv (cv x2) cpv))) (λ x6 . cfv (cv x1) cba)) (λ x5 . cfv (cv x1) cba)) (λ x4 . cc)) (λ x3 . co (cfv (cv x2) cba) (cfv (cv x1) cba) cmap))) ⟶ wceq cnmoo (cmpt2 (λ x1 x2 . cnv) (λ x1 x2 . cnv) (λ x1 x2 . cmpt (λ x3 . co (cfv (cv x2) cba) (cfv (cv x1) cba) cmap) (λ x3 . csup (cab (λ x4 . wrex (λ x5 . wa (wbr (cfv (cv x5) (cfv (cv x1) cnmcv)) c1 cle) (wceq (cv x4) (cfv (cfv (cv x5) (cv x3)) (cfv (cv x2) cnmcv)))) (λ x5 . cfv (cv x1) cba))) cxr clt))) ⟶ wceq cblo (cmpt2 (λ x1 x2 . cnv) (λ x1 x2 . cnv) (λ x1 x2 . crab (λ x3 . wbr (cfv (cv x3) (co (cv x1) (cv x2) cnmoo)) cpnf clt) (λ x3 . co (cv x1) (cv x2) clno))) ⟶ wceq c0o (cmpt2 (λ x1 x2 . cnv) (λ x1 x2 . cnv) (λ x1 x2 . cxp (cfv (cv x1) cba) (csn (cfv (cv x2) cn0v)))) ⟶ wceq caj (cmpt2 (λ x1 x2 . cnv) (λ x1 x2 . cnv) (λ x1 x2 . copab (λ x3 x4 . w3a (wf (cfv (cv x1) cba) (cfv (cv x2) cba) (cv x3)) (wf (cfv (cv x2) cba) (cfv (cv x1) cba) (cv x4)) (wral (λ x5 . wral (λ x6 . wceq (co (cfv (cv x5) (cv x3)) (cv x6) (cfv (cv x2) cdip)) (co (cv x5) (cfv (cv x6) (cv x4)) (cfv (cv x1) cdip))) (λ x6 . cfv (cv x2) cba)) (λ x5 . cfv (cv x1) cba))))) ⟶ wceq chmo (cmpt (λ x1 . cnv) (λ x1 . crab (λ x2 . wceq (cfv (cv x2) (co (cv x1) (cv x1) caj)) (cv x2)) (λ x2 . cdm (co (cv x1) (cv x1) caj)))) ⟶ wceq ccphlo (cin cnv (coprab (λ x1 x2 x3 . wral (λ x4 . wral (λ x5 . wceq (co (co (cfv (co (cv x4) (cv x5) (cv x1)) (cv x3)) c2 cexp) (co (cfv (co (cv x4) (co (cneg c1) (cv x5) (cv x2)) (cv x1)) (cv x3)) c2 cexp) caddc) (co c2 (co (co (cfv (cv x4) (cv x3)) c2 cexp) (co (cfv (cv x5) (cv x3)) c2 cexp) caddc) cmul)) (λ x5 . crn (cv x1))) (λ x4 . crn (cv x1))))) ⟶ wceq ccbn (crab (λ x1 . wcel (cfv (cv x1) cims) (cfv (cfv (cv x1) cba) cms)) (λ x1 . cnv)) ⟶ wceq chlo (cin ccbn ccphlo) ⟶ wceq cno (cmpt (λ x1 . cdm (cdm csp)) (λ x1 . cfv (co (cv x1) (cv x1) csp) csqrt)) ⟶ wceq chil (cfv (cop (cop cva csm) cno) cba) ⟶ wceq c0v (cfv (cop (cop cva csm) cno) cn0v) ⟶ wceq cmv (cmpt2 (λ x1 x2 . chil) (λ x1 x2 . chil) (λ x1 x2 . co (cv x1) (co (cneg c1) (cv x2) csm) cva)) ⟶ wceq chli (copab (λ x1 x2 . wa (wa (wf cn chil (cv x1)) (wcel (cv x2) chil)) (wral (λ x3 . wrex (λ x4 . wral (λ x5 . wbr (cfv (co (cfv (cv x5) (cv x1)) (cv x2) cmv) cno) (cv x3) clt) (λ x5 . cfv (cv x4) cuz)) (λ x4 . cn)) (λ x3 . crp)))) ⟶ wceq ccau (crab (λ x1 . wral (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cfv (co (cfv (cv x3) (cv x1)) (cfv (cv x4) (cv x1)) cmv) cno) (cv x2) clt) (λ x4 . cfv (cv x3) cuz)) (λ x3 . cn)) (λ x2 . crp)) (λ x1 . co chil cn cmap)) ⟶ wcel chil cvv ⟶ x0) ⟶ x0
Theorem df_dip : wceq cdip (cmpt (λ x0 . cnv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cba) (λ x1 x2 . cfv (cv x0) cba) (λ x1 x2 . co (csu (co c1 c4 cfz) (λ x3 . co (co ci (cv x3) cexp) (co (cfv (co (cv x1) (co (co ci (cv x3) cexp) (cv x2) (cfv (cv x0) cns)) (cfv (cv x0) cpv)) (cfv (cv x0) cnmcv)) c2 cexp) cmul)) c4 cdiv))) (proof)
Theorem df_ssp : wceq css (cmpt (λ x0 . cnv) (λ x0 . crab (λ x1 . w3a (wss (cfv (cv x1) cpv) (cfv (cv x0) cpv)) (wss (cfv (cv x1) cns) (cfv (cv x0) cns)) (wss (cfv (cv x1) cnmcv) (cfv (cv x0) cnmcv))) (λ x1 . cnv))) (proof)
Theorem df_lno : wceq clno (cmpt2 (λ x0 x1 . cnv) (λ x0 x1 . cnv) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (cfv (co (co (cv x3) (cv x4) (cfv (cv x0) cns)) (cv x5) (cfv (cv x0) cpv)) (cv x2)) (co (co (cv x3) (cfv (cv x4) (cv x2)) (cfv (cv x1) cns)) (cfv (cv x5) (cv x2)) (cfv (cv x1) cpv))) (λ x5 . cfv (cv x0) cba)) (λ x4 . cfv (cv x0) cba)) (λ x3 . cc)) (λ x2 . co (cfv (cv x1) cba) (cfv (cv x0) cba) cmap))) (proof)
Theorem df_nmoo : wceq cnmoo (cmpt2 (λ x0 x1 . cnv) (λ x0 x1 . cnv) (λ x0 x1 . cmpt (λ x2 . co (cfv (cv x1) cba) (cfv (cv x0) cba) cmap) (λ x2 . csup (cab (λ x3 . wrex (λ x4 . wa (wbr (cfv (cv x4) (cfv (cv x0) cnmcv)) c1 cle) (wceq (cv x3) (cfv (cfv (cv x4) (cv x2)) (cfv (cv x1) cnmcv)))) (λ x4 . cfv (cv x0) cba))) cxr clt))) (proof)
Theorem df_blo : wceq cblo (cmpt2 (λ x0 x1 . cnv) (λ x0 x1 . cnv) (λ x0 x1 . crab (λ x2 . wbr (cfv (cv x2) (co (cv x0) (cv x1) cnmoo)) cpnf clt) (λ x2 . co (cv x0) (cv x1) clno))) (proof)
Theorem df_0o : wceq c0o (cmpt2 (λ x0 x1 . cnv) (λ x0 x1 . cnv) (λ x0 x1 . cxp (cfv (cv x0) cba) (csn (cfv (cv x1) cn0v)))) (proof)
Theorem df_aj : wceq caj (cmpt2 (λ x0 x1 . cnv) (λ x0 x1 . cnv) (λ x0 x1 . copab (λ x2 x3 . w3a (wf (cfv (cv x0) cba) (cfv (cv x1) cba) (cv x2)) (wf (cfv (cv x1) cba) (cfv (cv x0) cba) (cv x3)) (wral (λ x4 . wral (λ x5 . wceq (co (cfv (cv x4) (cv x2)) (cv x5) (cfv (cv x1) cdip)) (co (cv x4) (cfv (cv x5) (cv x3)) (cfv (cv x0) cdip))) (λ x5 . cfv (cv x1) cba)) (λ x4 . cfv (cv x0) cba))))) (proof)
Theorem df_hmo : wceq chmo (cmpt (λ x0 . cnv) (λ x0 . crab (λ x1 . wceq (cfv (cv x1) (co (cv x0) (cv x0) caj)) (cv x1)) (λ x1 . cdm (co (cv x0) (cv x0) caj)))) (proof)
Theorem df_ph : wceq ccphlo (cin cnv (coprab (λ x0 x1 x2 . wral (λ x3 . wral (λ x4 . wceq (co (co (cfv (co (cv x3) (cv x4) (cv x0)) (cv x2)) c2 cexp) (co (cfv (co (cv x3) (co (cneg c1) (cv x4) (cv x1)) (cv x0)) (cv x2)) c2 cexp) caddc) (co c2 (co (co (cfv (cv x3) (cv x2)) c2 cexp) (co (cfv (cv x4) (cv x2)) c2 cexp) caddc) cmul)) (λ x4 . crn (cv x0))) (λ x3 . crn (cv x0))))) (proof)
Theorem df_cbn : wceq ccbn (crab (λ x0 . wcel (cfv (cv x0) cims) (cfv (cfv (cv x0) cba) cms)) (λ x0 . cnv)) (proof)
Theorem df_hlo : wceq chlo (cin ccbn ccphlo) (proof)
Theorem df_hnorm : wceq cno (cmpt (λ x0 . cdm (cdm csp)) (λ x0 . cfv (co (cv x0) (cv x0) csp) csqrt)) (proof)
Theorem df_hba : wceq chil (cfv (cop (cop cva csm) cno) cba) (proof)
Theorem df_h0v : wceq c0v (cfv (cop (cop cva csm) cno) cn0v) (proof)
Theorem df_hvsub : wceq cmv (cmpt2 (λ x0 x1 . chil) (λ x0 x1 . chil) (λ x0 x1 . co (cv x0) (co (cneg c1) (cv x1) csm) cva)) (proof)
Theorem df_hlim : wceq chli (copab (λ x0 x1 . wa (wa (wf cn chil (cv x0)) (wcel (cv x1) chil)) (wral (λ x2 . wrex (λ x3 . wral (λ x4 . wbr (cfv (co (cfv (cv x4) (cv x0)) (cv x1) cmv) cno) (cv x2) clt) (λ x4 . cfv (cv x3) cuz)) (λ x3 . cn)) (λ x2 . crp)))) (proof)
Theorem df_hcau : wceq ccau (crab (λ x0 . wral (λ x1 . wrex (λ x2 . wral (λ x3 . wbr (cfv (co (cfv (cv x2) (cv x0)) (cfv (cv x3) (cv x0)) cmv) cno) (cv x1) clt) (λ x3 . cfv (cv x2) cuz)) (λ x2 . cn)) (λ x1 . crp)) (λ x0 . co chil cn cmap)) (proof)
Theorem ax_hilex : wcel chil cvv (proof)