Proofgold Address

Known df_uhgr__df_ushgr__df_upgr__df_umgr__df_uspgr__df_usgr__df_subgr__df_fusgr__df_nbgr__df_uvtx__df_cplgr__df_cusgr__df_vtxdg__df_rgr__df_rusgr__df_ewlks__df_wlks__df_wlkson : ∀ x0 : ο . (wceq cuhgr (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wf (cdm (cv x3)) (cdif (cpw (cv x2)) (csn c0)) (cv x3)) (cfv (cv x1) ciedg)) (cfv (cv x1) cvtx))) ⟶ wceq cushgr (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wf1 (cdm (cv x3)) (cdif (cpw (cv x2)) (csn c0)) (cv x3)) (cfv (cv x1) ciedg)) (cfv (cv x1) cvtx))) ⟶ wceq cupgr (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wf (cdm (cv x3)) (crab (λ x4 . wbr (cfv (cv x4) chash) c2 cle) (λ x4 . cdif (cpw (cv x2)) (csn c0))) (cv x3)) (cfv (cv x1) ciedg)) (cfv (cv x1) cvtx))) ⟶ wceq cumgr (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wf (cdm (cv x3)) (crab (λ x4 . wceq (cfv (cv x4) chash) c2) (λ x4 . cdif (cpw (cv x2)) (csn c0))) (cv x3)) (cfv (cv x1) ciedg)) (cfv (cv x1) cvtx))) ⟶ wceq cuspgr (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wf1 (cdm (cv x3)) (crab (λ x4 . wbr (cfv (cv x4) chash) c2 cle) (λ x4 . cdif (cpw (cv x2)) (csn c0))) (cv x3)) (cfv (cv x1) ciedg)) (cfv (cv x1) cvtx))) ⟶ wceq cusgr (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wf1 (cdm (cv x3)) (crab (λ x4 . wceq (cfv (cv x4) chash) c2) (λ x4 . cdif (cpw (cv x2)) (csn c0))) (cv x3)) (cfv (cv x1) ciedg)) (cfv (cv x1) cvtx))) ⟶ wceq csubgr (copab (λ x1 x2 . w3a (wss (cfv (cv x1) cvtx) (cfv (cv x2) cvtx)) (wceq (cfv (cv x1) ciedg) (cres (cfv (cv x2) ciedg) (cdm (cfv (cv x1) ciedg)))) (wss (cfv (cv x1) cedg) (cpw (cfv (cv x1) cvtx))))) ⟶ wceq cfusgr (crab (λ x1 . wcel (cfv (cv x1) cvtx) cfn) (λ x1 . cusgr)) ⟶ wceq cnbgr (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cfv (cv x1) cvtx) (λ x1 x2 . crab (λ x3 . wrex (λ x4 . wss (cpr (cv x2) (cv x3)) (cv x4)) (λ x4 . cfv (cv x1) cedg)) (λ x3 . cdif (cfv (cv x1) cvtx) (csn (cv x2))))) ⟶ wceq cuvtx (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wcel (cv x3) (co (cv x1) (cv x2) cnbgr)) (λ x3 . cdif (cfv (cv x1) cvtx) (csn (cv x2)))) (λ x2 . cfv (cv x1) cvtx))) ⟶ wceq ccplgr (cab (λ x1 . wceq (cfv (cv x1) cuvtx) (cfv (cv x1) cvtx))) ⟶ wceq ccusgr (cin cusgr ccplgr) ⟶ wceq cvtxdg (cmpt (λ x1 . cvv) (λ x1 . csb (cfv (cv x1) cvtx) (λ x2 . csb (cfv (cv x1) ciedg) (λ x3 . cmpt (λ x4 . cv x2) (λ x4 . co (cfv (crab (λ x5 . wcel (cv x4) (cfv (cv x5) (cv x3))) (λ x5 . cdm (cv x3))) chash) (cfv (crab (λ x5 . wceq (cfv (cv x5) (cv x3)) (csn (cv x4))) (λ x5 . cdm (cv x3))) chash) cxad))))) ⟶ wceq crgr (copab (λ x1 x2 . wa (wcel (cv x2) cxnn0) (wral (λ x3 . wceq (cfv (cv x3) (cfv (cv x1) cvtxdg)) (cv x2)) (λ x3 . cfv (cv x1) cvtx)))) ⟶ wceq crusgr (copab (λ x1 x2 . wa (wcel (cv x1) cusgr) (wbr (cv x1) (cv x2) crgr))) ⟶ wceq cewlks (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cxnn0) (λ x1 x2 . cab (λ x3 . wsbc (λ x4 . wa (wcel (cv x3) (cword (cdm (cv x4)))) (wral (λ x5 . wbr (cv x2) (cfv (cin (cfv (cfv (co (cv x5) c1 cmin) (cv x3)) (cv x4)) (cfv (cfv (cv x5) (cv x3)) (cv x4))) chash) cle) (λ x5 . co c1 (cfv (cv x3) chash) cfzo))) (cfv (cv x1) ciedg)))) ⟶ wceq cwlks (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . w3a (wcel (cv x2) (cword (cdm (cfv (cv x1) ciedg)))) (wf (co cc0 (cfv (cv x2) chash) cfz) (cfv (cv x1) cvtx) (cv x3)) (wral (λ x4 . wif (wceq (cfv (cv x4) (cv x3)) (cfv (co (cv x4) c1 caddc) (cv x3))) (wceq (cfv (cfv (cv x4) (cv x2)) (cfv (cv x1) ciedg)) (csn (cfv (cv x4) (cv x3)))) (wss (cpr (cfv (cv x4) (cv x3)) (cfv (co (cv x4) c1 caddc) (cv x3))) (cfv (cfv (cv x4) (cv x2)) (cfv (cv x1) ciedg)))) (λ x4 . co cc0 (cfv (cv x2) chash) cfzo))))) ⟶ wceq cwlkson (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cvtx) (λ x2 x3 . cfv (cv x1) cvtx) (λ x2 x3 . copab (λ x4 x5 . w3a (wbr (cv x4) (cv x5) (cfv (cv x1) cwlks)) (wceq (cfv cc0 (cv x5)) (cv x2)) (wceq (cfv (cfv (cv x4) chash) (cv x5)) (cv x3)))))) ⟶ x0) ⟶ x0
Theorem df_uhgr : wceq cuhgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf (cdm (cv x2)) (cdif (cpw (cv x1)) (csn c0)) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))) (proof)
Theorem df_ushgr : wceq cushgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf1 (cdm (cv x2)) (cdif (cpw (cv x1)) (csn c0)) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))) (proof)
Theorem df_upgr : wceq cupgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf (cdm (cv x2)) (crab (λ x3 . wbr (cfv (cv x3) chash) c2 cle) (λ x3 . cdif (cpw (cv x1)) (csn c0))) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))) (proof)
Theorem df_umgr : wceq cumgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf (cdm (cv x2)) (crab (λ x3 . wceq (cfv (cv x3) chash) c2) (λ x3 . cdif (cpw (cv x1)) (csn c0))) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))) (proof)
Theorem df_uspgr : wceq cuspgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf1 (cdm (cv x2)) (crab (λ x3 . wbr (cfv (cv x3) chash) c2 cle) (λ x3 . cdif (cpw (cv x1)) (csn c0))) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))) (proof)
Theorem df_usgr : wceq cusgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf1 (cdm (cv x2)) (crab (λ x3 . wceq (cfv (cv x3) chash) c2) (λ x3 . cdif (cpw (cv x1)) (csn c0))) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))) (proof)
Theorem df_subgr : wceq csubgr (copab (λ x0 x1 . w3a (wss (cfv (cv x0) cvtx) (cfv (cv x1) cvtx)) (wceq (cfv (cv x0) ciedg) (cres (cfv (cv x1) ciedg) (cdm (cfv (cv x0) ciedg)))) (wss (cfv (cv x0) cedg) (cpw (cfv (cv x0) cvtx))))) (proof)
Theorem df_fusgr : wceq cfusgr (crab (λ x0 . wcel (cfv (cv x0) cvtx) cfn) (λ x0 . cusgr)) (proof)
Theorem df_nbgr : wceq cnbgr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cfv (cv x0) cvtx) (λ x0 x1 . crab (λ x2 . wrex (λ x3 . wss (cpr (cv x1) (cv x2)) (cv x3)) (λ x3 . cfv (cv x0) cedg)) (λ x2 . cdif (cfv (cv x0) cvtx) (csn (cv x1))))) (proof)
Theorem df_uvtx : wceq cuvtx (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wcel (cv x2) (co (cv x0) (cv x1) cnbgr)) (λ x2 . cdif (cfv (cv x0) cvtx) (csn (cv x1)))) (λ x1 . cfv (cv x0) cvtx))) (proof)
Theorem df_cplgr : wceq ccplgr (cab (λ x0 . wceq (cfv (cv x0) cuvtx) (cfv (cv x0) cvtx))) (proof)
Theorem df_cusgr : wceq ccusgr (cin cusgr ccplgr) (proof)
Theorem df_vtxdg : wceq cvtxdg (cmpt (λ x0 . cvv) (λ x0 . csb (cfv (cv x0) cvtx) (λ x1 . csb (cfv (cv x0) ciedg) (λ x2 . cmpt (λ x3 . cv x1) (λ x3 . co (cfv (crab (λ x4 . wcel (cv x3) (cfv (cv x4) (cv x2))) (λ x4 . cdm (cv x2))) chash) (cfv (crab (λ x4 . wceq (cfv (cv x4) (cv x2)) (csn (cv x3))) (λ x4 . cdm (cv x2))) chash) cxad))))) (proof)
Theorem df_rgr : wceq crgr (copab (λ x0 x1 . wa (wcel (cv x1) cxnn0) (wral (λ x2 . wceq (cfv (cv x2) (cfv (cv x0) cvtxdg)) (cv x1)) (λ x2 . cfv (cv x0) cvtx)))) (proof)
Theorem df_rusgr : wceq crusgr (copab (λ x0 x1 . wa (wcel (cv x0) cusgr) (wbr (cv x0) (cv x1) crgr))) (proof)
Theorem df_ewlks : wceq cewlks (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cxnn0) (λ x0 x1 . cab (λ x2 . wsbc (λ x3 . wa (wcel (cv x2) (cword (cdm (cv x3)))) (wral (λ x4 . wbr (cv x1) (cfv (cin (cfv (cfv (co (cv x4) c1 cmin) (cv x2)) (cv x3)) (cfv (cfv (cv x4) (cv x2)) (cv x3))) chash) cle) (λ x4 . co c1 (cfv (cv x2) chash) cfzo))) (cfv (cv x0) ciedg)))) (proof)
Theorem df_wlks : wceq cwlks (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . w3a (wcel (cv x1) (cword (cdm (cfv (cv x0) ciedg)))) (wf (co cc0 (cfv (cv x1) chash) cfz) (cfv (cv x0) cvtx) (cv x2)) (wral (λ x3 . wif (wceq (cfv (cv x3) (cv x2)) (cfv (co (cv x3) c1 caddc) (cv x2))) (wceq (cfv (cfv (cv x3) (cv x1)) (cfv (cv x0) ciedg)) (csn (cfv (cv x3) (cv x2)))) (wss (cpr (cfv (cv x3) (cv x2)) (cfv (co (cv x3) c1 caddc) (cv x2))) (cfv (cfv (cv x3) (cv x1)) (cfv (cv x0) ciedg)))) (λ x3 . co cc0 (cfv (cv x1) chash) cfzo))))) (proof)
Theorem df_wlkson : wceq cwlkson (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . copab (λ x3 x4 . w3a (wbr (cv x3) (cv x4) (cfv (cv x0) cwlks)) (wceq (cfv cc0 (cv x4)) (cv x1)) (wceq (cfv (cfv (cv x3) chash) (cv x4)) (cv x2)))))) (proof)