Proofgold Address

Known df_conngr__df_eupth__df_frgr__df_plig__df_grpo__df_gid__df_ginv__df_gdiv__df_ablo__df_vc__df_nv__df_va__df_ba__df_sm__df_0v__df_vs__df_nmcv__df_ims : ∀ x0 : ο . (wceq cconngr (cab (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wex (λ x5 . wex (λ x6 . wbr (cv x5) (cv x6) (co (cv x3) (cv x4) (cfv (cv x1) cpthson))))) (λ x4 . cv x2)) (λ x3 . cv x2)) (cfv (cv x1) cvtx))) ⟶ wceq ceupth (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wbr (cv x2) (cv x3) (cfv (cv x1) ctrls)) (wfo (co cc0 (cfv (cv x2) chash) cfzo) (cdm (cfv (cv x1) ciedg)) (cv x2))))) ⟶ wceq cfrgr (cab (λ x1 . wa (wcel (cv x1) cusgr) (wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wreu (λ x6 . wss (cpr (cpr (cv x6) (cv x4)) (cpr (cv x6) (cv x5))) (cv x3)) (λ x6 . cv x2)) (λ x5 . cdif (cv x2) (csn (cv x4)))) (λ x4 . cv x2)) (cfv (cv x1) cedg)) (cfv (cv x1) cvtx)))) ⟶ wceq cplig (cab (λ x1 . w3a (wral (λ x2 . wral (λ x3 . wne (cv x2) (cv x3) ⟶ wreu (λ x4 . wa (wcel (cv x2) (cv x4)) (wcel (cv x3) (cv x4))) (λ x4 . cv x1)) (λ x3 . cuni (cv x1))) (λ x2 . cuni (cv x1))) (wral (λ x2 . wrex (λ x3 . wrex (λ x4 . w3a (wne (cv x3) (cv x4)) (wcel (cv x3) (cv x2)) (wcel (cv x4) (cv x2))) (λ x4 . cuni (cv x1))) (λ x3 . cuni (cv x1))) (λ x2 . cv x1)) (wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wral (λ x5 . wn (w3a (wcel (cv x2) (cv x5)) (wcel (cv x3) (cv x5)) (wcel (cv x4) (cv x5)))) (λ x5 . cv x1)) (λ x4 . cuni (cv x1))) (λ x3 . cuni (cv x1))) (λ x2 . cuni (cv x1))))) ⟶ wceq cgr (cab (λ x1 . wex (λ x2 . w3a (wf (cxp (cv x2) (cv x2)) (cv x2) (cv x1)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (co (co (cv x3) (cv x4) (cv x1)) (cv x5) (cv x1)) (co (cv x3) (co (cv x4) (cv x5) (cv x1)) (cv x1))) (λ x5 . cv x2)) (λ x4 . cv x2)) (λ x3 . cv x2)) (wrex (λ x3 . wral (λ x4 . wa (wceq (co (cv x3) (cv x4) (cv x1)) (cv x4)) (wrex (λ x5 . wceq (co (cv x5) (cv x4) (cv x1)) (cv x3)) (λ x5 . cv x2))) (λ x4 . cv x2)) (λ x3 . cv x2))))) ⟶ wceq cgi (cmpt (λ x1 . cvv) (λ x1 . crio (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cv x1)) (cv x3)) (wceq (co (cv x3) (cv x2) (cv x1)) (cv x3))) (λ x3 . crn (cv x1))) (λ x2 . crn (cv x1)))) ⟶ wceq cgn (cmpt (λ x1 . cgr) (λ x1 . cmpt (λ x2 . crn (cv x1)) (λ x2 . crio (λ x3 . wceq (co (cv x3) (cv x2) (cv x1)) (cfv (cv x1) cgi)) (λ x3 . crn (cv x1))))) ⟶ wceq cgs (cmpt (λ x1 . cgr) (λ x1 . cmpt2 (λ x2 x3 . crn (cv x1)) (λ x2 x3 . crn (cv x1)) (λ x2 x3 . co (cv x2) (cfv (cv x3) (cfv (cv x1) cgn)) (cv x1)))) ⟶ wceq cablo (crab (λ x1 . wral (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cv x1)) (co (cv x3) (cv x2) (cv x1))) (λ x3 . crn (cv x1))) (λ x2 . crn (cv x1))) (λ x1 . cgr)) ⟶ wceq cvc (copab (λ x1 x2 . w3a (wcel (cv x1) cablo) (wf (cxp cc (crn (cv x1))) (crn (cv x1)) (cv x2)) (wral (λ x3 . wa (wceq (co c1 (cv x3) (cv x2)) (cv x3)) (wral (λ x4 . wa (wral (λ x5 . wceq (co (cv x4) (co (cv x3) (cv x5) (cv x1)) (cv x2)) (co (co (cv x4) (cv x3) (cv x2)) (co (cv x4) (cv x5) (cv x2)) (cv x1))) (λ x5 . crn (cv x1))) (wral (λ x5 . wa (wceq (co (co (cv x4) (cv x5) caddc) (cv x3) (cv x2)) (co (co (cv x4) (cv x3) (cv x2)) (co (cv x5) (cv x3) (cv x2)) (cv x1))) (wceq (co (co (cv x4) (cv x5) cmul) (cv x3) (cv x2)) (co (cv x4) (co (cv x5) (cv x3) (cv x2)) (cv x2)))) (λ x5 . cc))) (λ x4 . cc))) (λ x3 . crn (cv x1))))) ⟶ wceq cnv (coprab (λ x1 x2 x3 . w3a (wcel (cop (cv x1) (cv x2)) cvc) (wf (crn (cv x1)) cr (cv x3)) (wral (λ x4 . w3a (wceq (cfv (cv x4) (cv x3)) cc0 ⟶ wceq (cv x4) (cfv (cv x1) cgi)) (wral (λ x5 . wceq (cfv (co (cv x5) (cv x4) (cv x2)) (cv x3)) (co (cfv (cv x5) cabs) (cfv (cv x4) (cv x3)) cmul)) (λ x5 . cc)) (wral (λ x5 . wbr (cfv (co (cv x4) (cv x5) (cv x1)) (cv x3)) (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) caddc) cle) (λ x5 . crn (cv x1)))) (λ x4 . crn (cv x1))))) ⟶ wceq cpv (ccom c1st c1st) ⟶ wceq cba (cmpt (λ x1 . cvv) (λ x1 . crn (cfv (cv x1) cpv))) ⟶ wceq cns (ccom c2nd c1st) ⟶ wceq cn0v (ccom cgi cpv) ⟶ wceq cnsb (ccom cgs cpv) ⟶ wceq cnmcv c2nd ⟶ wceq cims (cmpt (λ x1 . cnv) (λ x1 . ccom (cfv (cv x1) cnmcv) (cfv (cv x1) cnsb))) ⟶ x0) ⟶ x0
Theorem df_conngr : wceq cconngr (cab (λ x0 . wsbc (λ x1 . wral (λ x2 . wral (λ x3 . wex (λ x4 . wex (λ x5 . wbr (cv x4) (cv x5) (co (cv x2) (cv x3) (cfv (cv x0) cpthson))))) (λ x3 . cv x1)) (λ x2 . cv x1)) (cfv (cv x0) cvtx))) (proof)
Theorem df_eupth : wceq ceupth (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wbr (cv x1) (cv x2) (cfv (cv x0) ctrls)) (wfo (co cc0 (cfv (cv x1) chash) cfzo) (cdm (cfv (cv x0) ciedg)) (cv x1))))) (proof)
Theorem df_frgr : wceq cfrgr (cab (λ x0 . wa (wcel (cv x0) cusgr) (wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wreu (λ x5 . wss (cpr (cpr (cv x5) (cv x3)) (cpr (cv x5) (cv x4))) (cv x2)) (λ x5 . cv x1)) (λ x4 . cdif (cv x1) (csn (cv x3)))) (λ x3 . cv x1)) (cfv (cv x0) cedg)) (cfv (cv x0) cvtx)))) (proof)
Theorem df_plig : wceq cplig (cab (λ x0 . w3a (wral (λ x1 . wral (λ x2 . wne (cv x1) (cv x2) ⟶ wreu (λ x3 . wa (wcel (cv x1) (cv x3)) (wcel (cv x2) (cv x3))) (λ x3 . cv x0)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (wral (λ x1 . wrex (λ x2 . wrex (λ x3 . w3a (wne (cv x2) (cv x3)) (wcel (cv x2) (cv x1)) (wcel (cv x3) (cv x1))) (λ x3 . cuni (cv x0))) (λ x2 . cuni (cv x0))) (λ x1 . cv x0)) (wrex (λ x1 . wrex (λ x2 . wrex (λ x3 . wral (λ x4 . wn (w3a (wcel (cv x1) (cv x4)) (wcel (cv x2) (cv x4)) (wcel (cv x3) (cv x4)))) (λ x4 . cv x0)) (λ x3 . cuni (cv x0))) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))))) (proof)
Theorem df_grpo : wceq cgr (cab (λ x0 . wex (λ x1 . w3a (wf (cxp (cv x1) (cv x1)) (cv x1) (cv x0)) (wral (λ x2 . wral (λ x3 . wral (λ x4 . wceq (co (co (cv x2) (cv x3) (cv x0)) (cv x4) (cv x0)) (co (cv x2) (co (cv x3) (cv x4) (cv x0)) (cv x0))) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1)) (wrex (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cv x0)) (cv x3)) (wrex (λ x4 . wceq (co (cv x4) (cv x3) (cv x0)) (cv x2)) (λ x4 . cv x1))) (λ x3 . cv x1)) (λ x2 . cv x1))))) (proof)
Theorem df_gid : wceq cgi (cmpt (λ x0 . cvv) (λ x0 . crio (λ x1 . wral (λ x2 . wa (wceq (co (cv x1) (cv x2) (cv x0)) (cv x2)) (wceq (co (cv x2) (cv x1) (cv x0)) (cv x2))) (λ x2 . crn (cv x0))) (λ x1 . crn (cv x0)))) (proof)
Theorem df_ginv : wceq cgn (cmpt (λ x0 . cgr) (λ x0 . cmpt (λ x1 . crn (cv x0)) (λ x1 . crio (λ x2 . wceq (co (cv x2) (cv x1) (cv x0)) (cfv (cv x0) cgi)) (λ x2 . crn (cv x0))))) (proof)
Theorem df_gdiv : wceq cgs (cmpt (λ x0 . cgr) (λ x0 . cmpt2 (λ x1 x2 . crn (cv x0)) (λ x1 x2 . crn (cv x0)) (λ x1 x2 . co (cv x1) (cfv (cv x2) (cfv (cv x0) cgn)) (cv x0)))) (proof)
Theorem df_ablo : wceq cablo (crab (λ x0 . wral (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) (cv x0)) (co (cv x2) (cv x1) (cv x0))) (λ x2 . crn (cv x0))) (λ x1 . crn (cv x0))) (λ x0 . cgr)) (proof)
Theorem df_vc : wceq cvc (copab (λ x0 x1 . w3a (wcel (cv x0) cablo) (wf (cxp cc (crn (cv x0))) (crn (cv x0)) (cv x1)) (wral (λ x2 . wa (wceq (co c1 (cv x2) (cv x1)) (cv x2)) (wral (λ x3 . wa (wral (λ x4 . wceq (co (cv x3) (co (cv x2) (cv x4) (cv x0)) (cv x1)) (co (co (cv x3) (cv x2) (cv x1)) (co (cv x3) (cv x4) (cv x1)) (cv x0))) (λ x4 . crn (cv x0))) (wral (λ x4 . wa (wceq (co (co (cv x3) (cv x4) caddc) (cv x2) (cv x1)) (co (co (cv x3) (cv x2) (cv x1)) (co (cv x4) (cv x2) (cv x1)) (cv x0))) (wceq (co (co (cv x3) (cv x4) cmul) (cv x2) (cv x1)) (co (cv x3) (co (cv x4) (cv x2) (cv x1)) (cv x1)))) (λ x4 . cc))) (λ x3 . cc))) (λ x2 . crn (cv x0))))) (proof)
Theorem df_nv : wceq cnv (coprab (λ x0 x1 x2 . w3a (wcel (cop (cv x0) (cv x1)) cvc) (wf (crn (cv x0)) cr (cv x2)) (wral (λ x3 . w3a (wceq (cfv (cv x3) (cv x2)) cc0 ⟶ wceq (cv x3) (cfv (cv x0) cgi)) (wral (λ x4 . wceq (cfv (co (cv x4) (cv x3) (cv x1)) (cv x2)) (co (cfv (cv x4) cabs) (cfv (cv x3) (cv x2)) cmul)) (λ x4 . cc)) (wral (λ x4 . wbr (cfv (co (cv x3) (cv x4) (cv x0)) (cv x2)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) caddc) cle) (λ x4 . crn (cv x0)))) (λ x3 . crn (cv x0))))) (proof)
Theorem df_va : wceq cpv (ccom c1st c1st) (proof)
Theorem df_ba : wceq cba (cmpt (λ x0 . cvv) (λ x0 . crn (cfv (cv x0) cpv))) (proof)
Theorem df_sm : wceq cns (ccom c2nd c1st) (proof)
Theorem df_0v : wceq cn0v (ccom cgi cpv) (proof)
Theorem df_vs : wceq cnsb (ccom cgs cpv) (proof)
Theorem df_nmcv : wceq cnmcv c2nd (proof)
Theorem df_ims : wceq cims (cmpt (λ x0 . cnv) (λ x0 . ccom (cfv (cv x0) cnmcv) (cfv (cv x0) cnsb))) (proof)