Proofgold Address

Known ax_cc__ax_dc__ax_ac__ax_ac2__df_gch__df_wina__df_ina__df_wun__df_wunc__df_tsk__df_gru__ax_groth__df_tskm__df_ni__df_pli__df_mi__df_lti__df_plpq : ∀ x0 : ο . ((∀ x1 . wbr (cv x1) com cen ⟶ wex (λ x2 . wral (λ x3 . wne (cv x3) c0 ⟶ wcel (cfv (cv x3) (cv x2)) (cv x3)) (λ x3 . cv x1))) ⟶ (∀ x1 . wa (wex (λ x2 . wex (λ x3 . wbr (cv x2) (cv x3) (cv x1)))) (wss (crn (cv x1)) (cdm (cv x1))) ⟶ wex (λ x2 . wral (λ x3 . wbr (cfv (cv x3) (cv x2)) (cfv (csuc (cv x3)) (cv x2)) (cv x1)) (λ x3 . com))) ⟶ (∀ x1 . wex (λ x2 . ∀ x3 x4 . wa (wcel (cv x3) (cv x4)) (wcel (cv x4) (cv x1)) ⟶ wex (λ x5 . ∀ x6 . wb (wex (λ x7 . wa (wa (wcel (cv x6) (cv x4)) (wcel (cv x4) (cv x7))) (wa (wcel (cv x6) (cv x7)) (wcel (cv x7) (cv x2))))) (wceq (cv x6) (cv x5))))) ⟶ (∀ x1 . wex (λ x2 . ∀ x3 . wex (λ x4 . ∀ x5 . wo (wa (wcel (cv x2) (cv x1)) (wcel (cv x3) (cv x2) ⟶ wa (wa (wcel (cv x4) (cv x1)) (wn (wceq (cv x2) (cv x4)))) (wcel (cv x3) (cv x4)))) (wa (wn (wcel (cv x2) (cv x1))) (wcel (cv x3) (cv x1) ⟶ wa (wa (wcel (cv x4) (cv x3)) (wcel (cv x4) (cv x2))) (wa (wcel (cv x5) (cv x3)) (wcel (cv x5) (cv x2)) ⟶ wceq (cv x5) (cv x4))))))) ⟶ wceq cgch (cun cfn (cab (λ x1 . ∀ x2 . wn (wa (wbr (cv x1) (cv x2) csdm) (wbr (cv x2) (cpw (cv x1)) csdm))))) ⟶ wceq cwina (cab (λ x1 . w3a (wne (cv x1) c0) (wceq (cfv (cv x1) ccf) (cv x1)) (wral (λ x2 . wrex (λ x3 . wbr (cv x2) (cv x3) csdm) (λ x3 . cv x1)) (λ x2 . cv x1)))) ⟶ wceq cina (cab (λ x1 . w3a (wne (cv x1) c0) (wceq (cfv (cv x1) ccf) (cv x1)) (wral (λ x2 . wbr (cpw (cv x2)) (cv x1) csdm) (λ x2 . cv x1)))) ⟶ wceq cwun (cab (λ x1 . w3a (wtr (cv x1)) (wne (cv x1) c0) (wral (λ x2 . w3a (wcel (cuni (cv x2)) (cv x1)) (wcel (cpw (cv x2)) (cv x1)) (wral (λ x3 . wcel (cpr (cv x2) (cv x3)) (cv x1)) (λ x3 . cv x1))) (λ x2 . cv x1)))) ⟶ wceq cwunm (cmpt (λ x1 . cvv) (λ x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cwun)))) ⟶ wceq ctsk (cab (λ x1 . wa (wral (λ x2 . wa (wss (cpw (cv x2)) (cv x1)) (wrex (λ x3 . wss (cpw (cv x2)) (cv x3)) (λ x3 . cv x1))) (λ x2 . cv x1)) (wral (λ x2 . wo (wbr (cv x2) (cv x1) cen) (wcel (cv x2) (cv x1))) (λ x2 . cpw (cv x1))))) ⟶ wceq cgru (cab (λ x1 . wa (wtr (cv x1)) (wral (λ x2 . w3a (wcel (cpw (cv x2)) (cv x1)) (wral (λ x3 . wcel (cpr (cv x2) (cv x3)) (cv x1)) (λ x3 . cv x1)) (wral (λ x3 . wcel (cuni (crn (cv x3))) (cv x1)) (λ x3 . co (cv x1) (cv x2) cmap))) (λ x2 . cv x1)))) ⟶ (∀ x1 . wex (λ x2 . w3a (wcel (cv x1) (cv x2)) (wral (λ x3 . wa (∀ x4 . wss (cv x4) (cv x3) ⟶ wcel (cv x4) (cv x2)) (wrex (λ x4 . ∀ x5 . wss (cv x5) (cv x3) ⟶ wcel (cv x5) (cv x4)) (λ x4 . cv x2))) (λ x3 . cv x2)) (∀ x3 . wss (cv x3) (cv x2) ⟶ wo (wbr (cv x3) (cv x2) cen) (wcel (cv x3) (cv x2))))) ⟶ wceq ctskm (cmpt (λ x1 . cvv) (λ x1 . cint (crab (λ x2 . wcel (cv x1) (cv x2)) (λ x2 . ctsk)))) ⟶ wceq cnpi (cdif com (csn c0)) ⟶ wceq cpli (cres coa (cxp cnpi cnpi)) ⟶ wceq cmi (cres comu (cxp cnpi cnpi)) ⟶ wceq clti (cin cep (cxp cnpi cnpi)) ⟶ wceq cplpq (cmpt2 (λ x1 x2 . cxp cnpi cnpi) (λ x1 x2 . cxp cnpi cnpi) (λ x1 x2 . cop (co (co (cfv (cv x1) c1st) (cfv (cv x2) c2nd) cmi) (co (cfv (cv x2) c1st) (cfv (cv x1) c2nd) cmi) cpli) (co (cfv (cv x1) c2nd) (cfv (cv x2) c2nd) cmi))) ⟶ x0) ⟶ x0
Theorem ax_cc : ∀ x0 . wbr (cv x0) com cen ⟶ wex (λ x1 . wral (λ x2 . wne (cv x2) c0 ⟶ wcel (cfv (cv x2) (cv x1)) (cv x2)) (λ x2 . cv x0)) (proof)
Theorem ax_dc : ∀ x0 . wa (wex (λ x1 . wex (λ x2 . wbr (cv x1) (cv x2) (cv x0)))) (wss (crn (cv x0)) (cdm (cv x0))) ⟶ wex (λ x1 . wral (λ x2 . wbr (cfv (cv x2) (cv x1)) (cfv (csuc (cv x2)) (cv x1)) (cv x0)) (λ x2 . com)) (proof)
Theorem ax_ac : ∀ x0 . wex (λ x1 . ∀ x2 x3 . wa (wcel (cv x2) (cv x3)) (wcel (cv x3) (cv x0)) ⟶ wex (λ x4 . ∀ x5 . wb (wex (λ x6 . wa (wa (wcel (cv x5) (cv x3)) (wcel (cv x3) (cv x6))) (wa (wcel (cv x5) (cv x6)) (wcel (cv x6) (cv x1))))) (wceq (cv x5) (cv x4)))) (proof)
Theorem ax_ac2 : ∀ x0 . wex (λ x1 . ∀ x2 . wex (λ x3 . ∀ x4 . wo (wa (wcel (cv x1) (cv x0)) (wcel (cv x2) (cv x1) ⟶ wa (wa (wcel (cv x3) (cv x0)) (wn (wceq (cv x1) (cv x3)))) (wcel (cv x2) (cv x3)))) (wa (wn (wcel (cv x1) (cv x0))) (wcel (cv x2) (cv x0) ⟶ wa (wa (wcel (cv x3) (cv x2)) (wcel (cv x3) (cv x1))) (wa (wcel (cv x4) (cv x2)) (wcel (cv x4) (cv x1)) ⟶ wceq (cv x4) (cv x3)))))) (proof)
Theorem df_gch : wceq cgch (cun cfn (cab (λ x0 . ∀ x1 . wn (wa (wbr (cv x0) (cv x1) csdm) (wbr (cv x1) (cpw (cv x0)) csdm))))) (proof)
Theorem df_wina : wceq cwina (cab (λ x0 . w3a (wne (cv x0) c0) (wceq (cfv (cv x0) ccf) (cv x0)) (wral (λ x1 . wrex (λ x2 . wbr (cv x1) (cv x2) csdm) (λ x2 . cv x0)) (λ x1 . cv x0)))) (proof)
Theorem df_ina : wceq cina (cab (λ x0 . w3a (wne (cv x0) c0) (wceq (cfv (cv x0) ccf) (cv x0)) (wral (λ x1 . wbr (cpw (cv x1)) (cv x0) csdm) (λ x1 . cv x0)))) (proof)
Theorem df_wun : wceq cwun (cab (λ x0 . w3a (wtr (cv x0)) (wne (cv x0) c0) (wral (λ x1 . w3a (wcel (cuni (cv x1)) (cv x0)) (wcel (cpw (cv x1)) (cv x0)) (wral (λ x2 . wcel (cpr (cv x1) (cv x2)) (cv x0)) (λ x2 . cv x0))) (λ x1 . cv x0)))) (proof)
Theorem df_wunc : wceq cwunm (cmpt (λ x0 . cvv) (λ x0 . cint (crab (λ x1 . wss (cv x0) (cv x1)) (λ x1 . cwun)))) (proof)
Theorem df_tsk : wceq ctsk (cab (λ x0 . wa (wral (λ x1 . wa (wss (cpw (cv x1)) (cv x0)) (wrex (λ x2 . wss (cpw (cv x1)) (cv x2)) (λ x2 . cv x0))) (λ x1 . cv x0)) (wral (λ x1 . wo (wbr (cv x1) (cv x0) cen) (wcel (cv x1) (cv x0))) (λ x1 . cpw (cv x0))))) (proof)
Theorem df_gru : wceq cgru (cab (λ x0 . wa (wtr (cv x0)) (wral (λ x1 . w3a (wcel (cpw (cv x1)) (cv x0)) (wral (λ x2 . wcel (cpr (cv x1) (cv x2)) (cv x0)) (λ x2 . cv x0)) (wral (λ x2 . wcel (cuni (crn (cv x2))) (cv x0)) (λ x2 . co (cv x0) (cv x1) cmap))) (λ x1 . cv x0)))) (proof)
Theorem ax_groth : ∀ x0 . wex (λ x1 . w3a (wcel (cv x0) (cv x1)) (wral (λ x2 . wa (∀ x3 . wss (cv x3) (cv x2) ⟶ wcel (cv x3) (cv x1)) (wrex (λ x3 . ∀ x4 . wss (cv x4) (cv x2) ⟶ wcel (cv x4) (cv x3)) (λ x3 . cv x1))) (λ x2 . cv x1)) (∀ x2 . wss (cv x2) (cv x1) ⟶ wo (wbr (cv x2) (cv x1) cen) (wcel (cv x2) (cv x1)))) (proof)
Theorem df_tskm : wceq ctskm (cmpt (λ x0 . cvv) (λ x0 . cint (crab (λ x1 . wcel (cv x0) (cv x1)) (λ x1 . ctsk)))) (proof)
Theorem df_ni : wceq cnpi (cdif com (csn c0)) (proof)
Theorem df_pli : wceq cpli (cres coa (cxp cnpi cnpi)) (proof)
Theorem df_mi : wceq cmi (cres comu (cxp cnpi cnpi)) (proof)
Theorem df_lti : wceq clti (cin cep (cxp cnpi cnpi)) (proof)
Theorem df_plpq : wceq cplpq (cmpt2 (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cop (co (co (cfv (cv x0) c1st) (cfv (cv x1) c2nd) cmi) (co (cfv (cv x1) c1st) (cfv (cv x0) c2nd) cmi) cpli) (co (cfv (cv x0) c2nd) (cfv (cv x1) c2nd) cmi))) (proof)