Proofgold Address

Known df_rag__df_perpg__df_hpg__df_mid__df_lmi__df_cgra__df_inag__df_leag__df_eqlg__df_ttg__df_ee__df_btwn__df_cgr__df_eeng__df_edgf__df_vtx__df_iedg__df_edg : ∀ x0 : ο . (wceq crag (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wceq (cfv (cv x2) chash) c3) (wceq (co (cfv cc0 (cv x2)) (cfv c2 (cv x2)) (cfv (cv x1) cds)) (co (cfv cc0 (cv x2)) (cfv (cfv c2 (cv x2)) (cfv (cfv c1 (cv x2)) (cfv (cv x1) cmir))) (cfv (cv x1) cds)))) (λ x2 . cword (cfv (cv x1) cbs)))) ⟶ wceq cperpg (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (crn (cfv (cv x1) clng))) (wcel (cv x3) (crn (cfv (cv x1) clng)))) (wrex (λ x4 . wral (λ x5 . wral (λ x6 . wcel (cs3 (cv x5) (cv x4) (cv x6)) (cfv (cv x1) crag)) (λ x6 . cv x3)) (λ x5 . cv x2)) (λ x4 . cin (cv x2) (cv x3)))))) ⟶ wceq chpg (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . crn (cfv (cv x1) clng)) (λ x2 . copab (λ x3 x4 . wsbc (λ x5 . wsbc (λ x6 . wrex (λ x7 . wa (wa (wa (wcel (cv x3) (cdif (cv x5) (cv x2))) (wcel (cv x7) (cdif (cv x5) (cv x2)))) (wrex (λ x8 . wcel (cv x8) (co (cv x3) (cv x7) (cv x6))) (λ x8 . cv x2))) (wa (wa (wcel (cv x4) (cdif (cv x5) (cv x2))) (wcel (cv x7) (cdif (cv x5) (cv x2)))) (wrex (λ x8 . wcel (cv x8) (co (cv x4) (cv x7) (cv x6))) (λ x8 . cv x2)))) (λ x7 . cv x5)) (cfv (cv x1) citv)) (cfv (cv x1) cbs))))) ⟶ wceq cmid (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . crio (λ x4 . wceq (cv x3) (cfv (cv x2) (cfv (cv x4) (cfv (cv x1) cmir)))) (λ x4 . cfv (cv x1) cbs)))) ⟶ wceq clmi (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . crn (cfv (cv x1) clng)) (λ x2 . cmpt (λ x3 . cfv (cv x1) cbs) (λ x3 . crio (λ x4 . wa (wcel (co (cv x3) (cv x4) (cfv (cv x1) cmid)) (cv x2)) (wo (wbr (cv x2) (co (cv x3) (cv x4) (cfv (cv x1) clng)) (cfv (cv x1) cperpg)) (wceq (cv x3) (cv x4)))) (λ x4 . cfv (cv x1) cbs))))) ⟶ wceq ccgra (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wsbc (λ x4 . wsbc (λ x5 . wa (wa (wcel (cv x2) (co (cv x4) (co cc0 c3 cfzo) cmap)) (wcel (cv x3) (co (cv x4) (co cc0 c3 cfzo) cmap))) (wrex (λ x6 . wrex (λ x7 . w3a (wbr (cv x2) (cs3 (cv x6) (cfv c1 (cv x3)) (cv x7)) (cfv (cv x1) ccgrg)) (wbr (cv x6) (cfv cc0 (cv x3)) (cfv (cfv c1 (cv x3)) (cv x5))) (wbr (cv x7) (cfv c2 (cv x3)) (cfv (cfv c1 (cv x3)) (cv x5)))) (λ x7 . cv x4)) (λ x6 . cv x4))) (cfv (cv x1) chlg)) (cfv (cv x1) cbs)))) ⟶ wceq cinag (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (cfv (cv x1) cbs)) (wcel (cv x3) (co (cfv (cv x1) cbs) (co cc0 c3 cfzo) cmap))) (wa (w3a (wne (cfv cc0 (cv x3)) (cfv c1 (cv x3))) (wne (cfv c2 (cv x3)) (cfv c1 (cv x3))) (wne (cv x2) (cfv c1 (cv x3)))) (wrex (λ x4 . wa (wcel (cv x4) (co (cfv cc0 (cv x3)) (cfv c2 (cv x3)) (cfv (cv x1) citv))) (wo (wceq (cv x4) (cfv c1 (cv x3))) (wbr (cv x4) (cv x2) (cfv (cfv c1 (cv x3)) (cfv (cv x1) chlg))))) (λ x4 . cfv (cv x1) cbs)))))) ⟶ wceq cleag (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (co (cfv (cv x1) cbs) (co cc0 c3 cfzo) cmap)) (wcel (cv x3) (co (cfv (cv x1) cbs) (co cc0 c3 cfzo) cmap))) (wrex (λ x4 . wa (wbr (cv x4) (cs3 (cfv cc0 (cv x3)) (cfv c1 (cv x3)) (cfv c2 (cv x3))) (cfv (cv x1) cinag)) (wbr (cs3 (cfv cc0 (cv x2)) (cfv c1 (cv x2)) (cfv c2 (cv x2))) (cs3 (cfv cc0 (cv x3)) (cfv c1 (cv x3)) (cv x4)) (cfv (cv x1) ccgra))) (λ x4 . cfv (cv x1) cbs))))) ⟶ wceq ceqlg (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wbr (cv x2) (cs3 (cfv c1 (cv x2)) (cfv c2 (cv x2)) (cfv cc0 (cv x2))) (cfv (cv x1) ccgrg)) (λ x2 . co (cfv (cv x1) cbs) (co cc0 c3 cfzo) cmap))) ⟶ wceq cttg (cmpt (λ x1 . cvv) (λ x1 . csb (cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . crab (λ x4 . wrex (λ x5 . wceq (co (cv x4) (cv x2) (cfv (cv x1) csg)) (co (cv x5) (co (cv x3) (cv x2) (cfv (cv x1) csg)) (cfv (cv x1) cvsca))) (λ x5 . co cc0 c1 cicc)) (λ x4 . cfv (cv x1) cbs))) (λ x2 . co (co (cv x1) (cop (cfv cnx citv) (cv x2)) csts) (cop (cfv cnx clng) (cmpt2 (λ x3 x4 . cfv (cv x1) cbs) (λ x3 x4 . cfv (cv x1) cbs) (λ x3 x4 . crab (λ x5 . w3o (wcel (cv x5) (co (cv x3) (cv x4) (cv x2))) (wcel (cv x3) (co (cv x5) (cv x4) (cv x2))) (wcel (cv x4) (co (cv x3) (cv x5) (cv x2)))) (λ x5 . cfv (cv x1) cbs)))) csts))) ⟶ wceq cee (cmpt (λ x1 . cn) (λ x1 . co cr (co c1 (cv x1) cfz) cmap)) ⟶ wceq cbtwn (ccnv (coprab (λ x1 x2 x3 . wrex (λ x4 . wa (w3a (wcel (cv x1) (cfv (cv x4) cee)) (wcel (cv x2) (cfv (cv x4) cee)) (wcel (cv x3) (cfv (cv x4) cee))) (wrex (λ x5 . wral (λ x6 . wceq (cfv (cv x6) (cv x3)) (co (co (co c1 (cv x5) cmin) (cfv (cv x6) (cv x1)) cmul) (co (cv x5) (cfv (cv x6) (cv x2)) cmul) caddc)) (λ x6 . co c1 (cv x4) cfz)) (λ x5 . co cc0 c1 cicc))) (λ x4 . cn)))) ⟶ wceq ccgr (copab (λ x1 x2 . wrex (λ x3 . wa (wa (wcel (cv x1) (cxp (cfv (cv x3) cee) (cfv (cv x3) cee))) (wcel (cv x2) (cxp (cfv (cv x3) cee) (cfv (cv x3) cee)))) (wceq (csu (co c1 (cv x3) cfz) (λ x4 . co (co (cfv (cv x4) (cfv (cv x1) c1st)) (cfv (cv x4) (cfv (cv x1) c2nd)) cmin) c2 cexp)) (csu (co c1 (cv x3) cfz) (λ x4 . co (co (cfv (cv x4) (cfv (cv x2) c1st)) (cfv (cv x4) (cfv (cv x2) c2nd)) cmin) c2 cexp)))) (λ x3 . cn))) ⟶ wceq ceeng (cmpt (λ x1 . cn) (λ x1 . cun (cpr (cop (cfv cnx cbs) (cfv (cv x1) cee)) (cop (cfv cnx cds) (cmpt2 (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . csu (co c1 (cv x1) cfz) (λ x4 . co (co (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) cmin) c2 cexp))))) (cpr (cop (cfv cnx citv) (cmpt2 (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . crab (λ x4 . wbr (cv x4) (cop (cv x2) (cv x3)) cbtwn) (λ x4 . cfv (cv x1) cee)))) (cop (cfv cnx clng) (cmpt2 (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . cdif (cfv (cv x1) cee) (csn (cv x2))) (λ x2 x3 . crab (λ x4 . w3o (wbr (cv x4) (cop (cv x2) (cv x3)) cbtwn) (wbr (cv x2) (cop (cv x4) (cv x3)) cbtwn) (wbr (cv x3) (cop (cv x2) (cv x4)) cbtwn)) (λ x4 . cfv (cv x1) cee))))))) ⟶ wceq cedgf (cslot (cdc c1 c8)) ⟶ wceq cvtx (cmpt (λ x1 . cvv) (λ x1 . cif (wcel (cv x1) (cxp cvv cvv)) (cfv (cv x1) c1st) (cfv (cv x1) cbs))) ⟶ wceq ciedg (cmpt (λ x1 . cvv) (λ x1 . cif (wcel (cv x1) (cxp cvv cvv)) (cfv (cv x1) c2nd) (cfv (cv x1) cedgf))) ⟶ wceq cedg (cmpt (λ x1 . cvv) (λ x1 . crn (cfv (cv x1) ciedg))) ⟶ x0) ⟶ x0
Theorem df_rag : wceq crag (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wceq (cfv (cv x1) chash) c3) (wceq (co (cfv cc0 (cv x1)) (cfv c2 (cv x1)) (cfv (cv x0) cds)) (co (cfv cc0 (cv x1)) (cfv (cfv c2 (cv x1)) (cfv (cfv c1 (cv x1)) (cfv (cv x0) cmir))) (cfv (cv x0) cds)))) (λ x1 . cword (cfv (cv x0) cbs)))) (proof)
Theorem df_perpg : wceq cperpg (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (crn (cfv (cv x0) clng))) (wcel (cv x2) (crn (cfv (cv x0) clng)))) (wrex (λ x3 . wral (λ x4 . wral (λ x5 . wcel (cs3 (cv x4) (cv x3) (cv x5)) (cfv (cv x0) crag)) (λ x5 . cv x2)) (λ x4 . cv x1)) (λ x3 . cin (cv x1) (cv x2)))))) (proof)
Theorem df_hpg : wceq chpg (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . crn (cfv (cv x0) clng)) (λ x1 . copab (λ x2 x3 . wsbc (λ x4 . wsbc (λ x5 . wrex (λ x6 . wa (wa (wa (wcel (cv x2) (cdif (cv x4) (cv x1))) (wcel (cv x6) (cdif (cv x4) (cv x1)))) (wrex (λ x7 . wcel (cv x7) (co (cv x2) (cv x6) (cv x5))) (λ x7 . cv x1))) (wa (wa (wcel (cv x3) (cdif (cv x4) (cv x1))) (wcel (cv x6) (cdif (cv x4) (cv x1)))) (wrex (λ x7 . wcel (cv x7) (co (cv x3) (cv x6) (cv x5))) (λ x7 . cv x1)))) (λ x6 . cv x4)) (cfv (cv x0) citv)) (cfv (cv x0) cbs))))) (proof)
Theorem df_mid : wceq cmid (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . crio (λ x3 . wceq (cv x2) (cfv (cv x1) (cfv (cv x3) (cfv (cv x0) cmir)))) (λ x3 . cfv (cv x0) cbs)))) (proof)
Theorem df_lmi : wceq clmi (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . crn (cfv (cv x0) clng)) (λ x1 . cmpt (λ x2 . cfv (cv x0) cbs) (λ x2 . crio (λ x3 . wa (wcel (co (cv x2) (cv x3) (cfv (cv x0) cmid)) (cv x1)) (wo (wbr (cv x1) (co (cv x2) (cv x3) (cfv (cv x0) clng)) (cfv (cv x0) cperpg)) (wceq (cv x2) (cv x3)))) (λ x3 . cfv (cv x0) cbs))))) (proof)
Theorem df_cgra : wceq ccgra (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wsbc (λ x3 . wsbc (λ x4 . wa (wa (wcel (cv x1) (co (cv x3) (co cc0 c3 cfzo) cmap)) (wcel (cv x2) (co (cv x3) (co cc0 c3 cfzo) cmap))) (wrex (λ x5 . wrex (λ x6 . w3a (wbr (cv x1) (cs3 (cv x5) (cfv c1 (cv x2)) (cv x6)) (cfv (cv x0) ccgrg)) (wbr (cv x5) (cfv cc0 (cv x2)) (cfv (cfv c1 (cv x2)) (cv x4))) (wbr (cv x6) (cfv c2 (cv x2)) (cfv (cfv c1 (cv x2)) (cv x4)))) (λ x6 . cv x3)) (λ x5 . cv x3))) (cfv (cv x0) chlg)) (cfv (cv x0) cbs)))) (proof)
Theorem df_inag : wceq cinag (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (cfv (cv x0) cbs)) (wcel (cv x2) (co (cfv (cv x0) cbs) (co cc0 c3 cfzo) cmap))) (wa (w3a (wne (cfv cc0 (cv x2)) (cfv c1 (cv x2))) (wne (cfv c2 (cv x2)) (cfv c1 (cv x2))) (wne (cv x1) (cfv c1 (cv x2)))) (wrex (λ x3 . wa (wcel (cv x3) (co (cfv cc0 (cv x2)) (cfv c2 (cv x2)) (cfv (cv x0) citv))) (wo (wceq (cv x3) (cfv c1 (cv x2))) (wbr (cv x3) (cv x1) (cfv (cfv c1 (cv x2)) (cfv (cv x0) chlg))))) (λ x3 . cfv (cv x0) cbs)))))) (proof)
Theorem df_leag : wceq cleag (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (co (cfv (cv x0) cbs) (co cc0 c3 cfzo) cmap)) (wcel (cv x2) (co (cfv (cv x0) cbs) (co cc0 c3 cfzo) cmap))) (wrex (λ x3 . wa (wbr (cv x3) (cs3 (cfv cc0 (cv x2)) (cfv c1 (cv x2)) (cfv c2 (cv x2))) (cfv (cv x0) cinag)) (wbr (cs3 (cfv cc0 (cv x1)) (cfv c1 (cv x1)) (cfv c2 (cv x1))) (cs3 (cfv cc0 (cv x2)) (cfv c1 (cv x2)) (cv x3)) (cfv (cv x0) ccgra))) (λ x3 . cfv (cv x0) cbs))))) (proof)
Theorem df_eqlg : wceq ceqlg (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wbr (cv x1) (cs3 (cfv c1 (cv x1)) (cfv c2 (cv x1)) (cfv cc0 (cv x1))) (cfv (cv x0) ccgrg)) (λ x1 . co (cfv (cv x0) cbs) (co cc0 c3 cfzo) cmap))) (proof)
Theorem df_ttg : wceq cttg (cmpt (λ x0 . cvv) (λ x0 . csb (cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . crab (λ x3 . wrex (λ x4 . wceq (co (cv x3) (cv x1) (cfv (cv x0) csg)) (co (cv x4) (co (cv x2) (cv x1) (cfv (cv x0) csg)) (cfv (cv x0) cvsca))) (λ x4 . co cc0 c1 cicc)) (λ x3 . cfv (cv x0) cbs))) (λ x1 . co (co (cv x0) (cop (cfv cnx citv) (cv x1)) csts) (cop (cfv cnx clng) (cmpt2 (λ x2 x3 . cfv (cv x0) cbs) (λ x2 x3 . cfv (cv x0) cbs) (λ x2 x3 . crab (λ x4 . w3o (wcel (cv x4) (co (cv x2) (cv x3) (cv x1))) (wcel (cv x2) (co (cv x4) (cv x3) (cv x1))) (wcel (cv x3) (co (cv x2) (cv x4) (cv x1)))) (λ x4 . cfv (cv x0) cbs)))) csts))) (proof)
Theorem df_ee : wceq cee (cmpt (λ x0 . cn) (λ x0 . co cr (co c1 (cv x0) cfz) cmap)) (proof)
Theorem df_btwn : wceq cbtwn (ccnv (coprab (λ x0 x1 x2 . wrex (λ x3 . wa (w3a (wcel (cv x0) (cfv (cv x3) cee)) (wcel (cv x1) (cfv (cv x3) cee)) (wcel (cv x2) (cfv (cv x3) cee))) (wrex (λ x4 . wral (λ x5 . wceq (cfv (cv x5) (cv x2)) (co (co (co c1 (cv x4) cmin) (cfv (cv x5) (cv x0)) cmul) (co (cv x4) (cfv (cv x5) (cv x1)) cmul) caddc)) (λ x5 . co c1 (cv x3) cfz)) (λ x4 . co cc0 c1 cicc))) (λ x3 . cn)))) (proof)
Theorem df_cgr : wceq ccgr (copab (λ x0 x1 . wrex (λ x2 . wa (wa (wcel (cv x0) (cxp (cfv (cv x2) cee) (cfv (cv x2) cee))) (wcel (cv x1) (cxp (cfv (cv x2) cee) (cfv (cv x2) cee)))) (wceq (csu (co c1 (cv x2) cfz) (λ x3 . co (co (cfv (cv x3) (cfv (cv x0) c1st)) (cfv (cv x3) (cfv (cv x0) c2nd)) cmin) c2 cexp)) (csu (co c1 (cv x2) cfz) (λ x3 . co (co (cfv (cv x3) (cfv (cv x1) c1st)) (cfv (cv x3) (cfv (cv x1) c2nd)) cmin) c2 cexp)))) (λ x2 . cn))) (proof)
Theorem df_eeng : wceq ceeng (cmpt (λ x0 . cn) (λ x0 . cun (cpr (cop (cfv cnx cbs) (cfv (cv x0) cee)) (cop (cfv cnx cds) (cmpt2 (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . csu (co c1 (cv x0) cfz) (λ x3 . co (co (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) cmin) c2 cexp))))) (cpr (cop (cfv cnx citv) (cmpt2 (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . crab (λ x3 . wbr (cv x3) (cop (cv x1) (cv x2)) cbtwn) (λ x3 . cfv (cv x0) cee)))) (cop (cfv cnx clng) (cmpt2 (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . cdif (cfv (cv x0) cee) (csn (cv x1))) (λ x1 x2 . crab (λ x3 . w3o (wbr (cv x3) (cop (cv x1) (cv x2)) cbtwn) (wbr (cv x1) (cop (cv x3) (cv x2)) cbtwn) (wbr (cv x2) (cop (cv x1) (cv x3)) cbtwn)) (λ x3 . cfv (cv x0) cee))))))) (proof)
Theorem df_edgf : wceq cedgf (cslot (cdc c1 c8)) (proof)
Theorem df_vtx : wceq cvtx (cmpt (λ x0 . cvv) (λ x0 . cif (wcel (cv x0) (cxp cvv cvv)) (cfv (cv x0) c1st) (cfv (cv x0) cbs))) (proof)
Theorem df_iedg : wceq ciedg (cmpt (λ x0 . cvv) (λ x0 . cif (wcel (cv x0) (cxp cvv cvv)) (cfv (cv x0) c2nd) (cfv (cv x0) cedgf))) (proof)
Theorem df_edg : wceq cedg (cmpt (λ x0 . cvv) (λ x0 . crn (cfv (cv x0) ciedg))) (proof)