Proofgold Address

Known df_retr__df_pconn__df_sconn__df_cvm__df_goel__df_gona__df_goal__df_sat__df_sate__df_fmla__df_gonot__df_goan__df_goim__df_goor__df_gobi__df_goeq__df_goex__df_prv : ∀ x0 : ο . (wceq cretr (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . ctop) (λ x1 x2 . crab (λ x3 . wrex (λ x4 . wne (co (ccom (cv x3) (cv x4)) (cres cid (cuni (cv x1))) (co (cv x1) (cv x1) chtpy)) c0) (λ x4 . co (cv x2) (cv x1) ccn)) (λ x3 . co (cv x1) (cv x2) ccn))) ⟶ wceq cpconn (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wa (wceq (cfv cc0 (cv x4)) (cv x2)) (wceq (cfv c1 (cv x4)) (cv x3))) (λ x4 . co cii (cv x1) ccn)) (λ x3 . cuni (cv x1))) (λ x2 . cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq csconn (crab (λ x1 . wral (λ x2 . wceq (cfv cc0 (cv x2)) (cfv c1 (cv x2)) ⟶ wbr (cv x2) (cxp (co cc0 c1 cicc) (csn (cfv cc0 (cv x2)))) (cfv (cv x1) cphtpc)) (λ x2 . co cii (cv x1) ccn)) (λ x1 . cpconn)) ⟶ wceq ccvm (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . ctop) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wrex (λ x5 . wa (wcel (cv x4) (cv x5)) (wrex (λ x6 . wa (wceq (cuni (cv x6)) (cima (ccnv (cv x3)) (cv x5))) (wral (λ x7 . wa (wral (λ x8 . wceq (cin (cv x7) (cv x8)) c0) (λ x8 . cdif (cv x6) (csn (cv x7)))) (wcel (cres (cv x3) (cv x7)) (co (co (cv x1) (cv x7) crest) (co (cv x2) (cv x5) crest) chmeo))) (λ x7 . cv x6))) (λ x6 . cdif (cpw (cv x1)) (csn c0)))) (λ x5 . cv x2)) (λ x4 . cuni (cv x2))) (λ x3 . co (cv x1) (cv x2) ccn))) ⟶ wceq cgoe (cmpt (λ x1 . cxp com com) (λ x1 . cop c0 (cv x1))) ⟶ wceq cgna (cmpt (λ x1 . cxp cvv cvv) (λ x1 . cop c1o (cv x1))) ⟶ (∀ x1 x2 : ι → ο . wceq (cgol x1 x2) (cop c2o (cop x2 x1))) ⟶ wceq csat (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cres (crdg (cmpt (λ x3 . cvv) (λ x3 . cun (cv x3) (copab (λ x4 x5 . wrex (λ x6 . wo (wrex (λ x7 . wa (wceq (cv x4) (co (cfv (cv x6) c1st) (cfv (cv x7) c1st) cgna)) (wceq (cv x5) (cdif (co (cv x1) com cmap) (cin (cfv (cv x6) c2nd) (cfv (cv x7) c2nd))))) (λ x7 . cv x3)) (wrex (λ x7 . wa (wceq (cv x4) (cgol (cfv (cv x6) c1st) (cv x7))) (wceq (cv x5) (crab (λ x8 . wral (λ x9 . wcel (cun (csn (cop (cv x7) (cv x9))) (cres (cv x8) (cdif com (csn (cv x7))))) (cfv (cv x6) c2nd)) (λ x9 . cv x1)) (λ x8 . co (cv x1) com cmap)))) (λ x7 . com))) (λ x6 . cv x3))))) (copab (λ x3 x4 . wrex (λ x5 . wrex (λ x6 . wa (wceq (cv x3) (co (cv x5) (cv x6) cgoe)) (wceq (cv x4) (crab (λ x7 . wbr (cfv (cv x5) (cv x7)) (cfv (cv x6) (cv x7)) (cv x2)) (λ x7 . co (cv x1) com cmap)))) (λ x6 . com)) (λ x5 . com)))) (csuc com))) ⟶ wceq csate (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cfv (cv x2) (cfv com (co (cv x1) (cin cep (cxp (cv x1) (cv x1))) csat)))) ⟶ wceq cfmla (cmpt (λ x1 . csuc com) (λ x1 . cdm (cfv (cv x1) (co c0 c0 csat)))) ⟶ (∀ x1 : ι → ο . wceq (cgon x1) (co x1 x1 cgna)) ⟶ wceq cgoa (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cgon (co (cv x1) (cv x2) cgna))) ⟶ wceq cgoi (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (cv x1) (cgon (cv x2)) cgna)) ⟶ wceq cgoo (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (cgon (cv x1)) (cv x2) cgoi)) ⟶ wceq cgob (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (co (cv x1) (cv x2) cgoi) (co (cv x2) (cv x1) cgoi) cgoa)) ⟶ wceq cgoq (cmpt2 (λ x1 x2 . com) (λ x1 x2 . com) (λ x1 x2 . csb (csuc (cun (cv x1) (cv x2))) (λ x3 . cgol (co (co (cv x3) (cv x1) cgoe) (co (cv x3) (cv x2) cgoe) cgob) (cv x3)))) ⟶ (∀ x1 x2 : ι → ο . wceq (cgox x1 x2) (cgon (cgol (cgon x1) x2))) ⟶ wceq cprv (copab (λ x1 x2 . wceq (co (cv x1) (cv x2) csate) (co (cv x1) com cmap))) ⟶ x0) ⟶ x0
Theorem df_retr : wceq cretr (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . crab (λ x2 . wrex (λ x3 . wne (co (ccom (cv x2) (cv x3)) (cres cid (cuni (cv x0))) (co (cv x0) (cv x0) chtpy)) c0) (λ x3 . co (cv x1) (cv x0) ccn)) (λ x2 . co (cv x0) (cv x1) ccn))) (proof)
Theorem df_pconn : wceq cpconn (crab (λ x0 . wral (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wceq (cfv cc0 (cv x3)) (cv x1)) (wceq (cfv c1 (cv x3)) (cv x2))) (λ x3 . co cii (cv x0) ccn)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_sconn : wceq csconn (crab (λ x0 . wral (λ x1 . wceq (cfv cc0 (cv x1)) (cfv c1 (cv x1)) ⟶ wbr (cv x1) (cxp (co cc0 c1 cicc) (csn (cfv cc0 (cv x1)))) (cfv (cv x0) cphtpc)) (λ x1 . co cii (cv x0) ccn)) (λ x0 . cpconn)) (proof)
Theorem df_cvm : wceq ccvm (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wa (wcel (cv x3) (cv x4)) (wrex (λ x5 . wa (wceq (cuni (cv x5)) (cima (ccnv (cv x2)) (cv x4))) (wral (λ x6 . wa (wral (λ x7 . wceq (cin (cv x6) (cv x7)) c0) (λ x7 . cdif (cv x5) (csn (cv x6)))) (wcel (cres (cv x2) (cv x6)) (co (co (cv x0) (cv x6) crest) (co (cv x1) (cv x4) crest) chmeo))) (λ x6 . cv x5))) (λ x5 . cdif (cpw (cv x0)) (csn c0)))) (λ x4 . cv x1)) (λ x3 . cuni (cv x1))) (λ x2 . co (cv x0) (cv x1) ccn))) (proof)
Theorem df_goel : wceq cgoe (cmpt (λ x0 . cxp com com) (λ x0 . cop c0 (cv x0))) (proof)
Theorem df_gona : wceq cgna (cmpt (λ x0 . cxp cvv cvv) (λ x0 . cop c1o (cv x0))) (proof)
Theorem df_goal : ∀ x0 x1 : ι → ο . wceq (cgol x0 x1) (cop c2o (cop x1 x0)) (proof)
Theorem df_sat : wceq csat (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cres (crdg (cmpt (λ x2 . cvv) (λ x2 . cun (cv x2) (copab (λ x3 x4 . wrex (λ x5 . wo (wrex (λ x6 . wa (wceq (cv x3) (co (cfv (cv x5) c1st) (cfv (cv x6) c1st) cgna)) (wceq (cv x4) (cdif (co (cv x0) com cmap) (cin (cfv (cv x5) c2nd) (cfv (cv x6) c2nd))))) (λ x6 . cv x2)) (wrex (λ x6 . wa (wceq (cv x3) (cgol (cfv (cv x5) c1st) (cv x6))) (wceq (cv x4) (crab (λ x7 . wral (λ x8 . wcel (cun (csn (cop (cv x6) (cv x8))) (cres (cv x7) (cdif com (csn (cv x6))))) (cfv (cv x5) c2nd)) (λ x8 . cv x0)) (λ x7 . co (cv x0) com cmap)))) (λ x6 . com))) (λ x5 . cv x2))))) (copab (λ x2 x3 . wrex (λ x4 . wrex (λ x5 . wa (wceq (cv x2) (co (cv x4) (cv x5) cgoe)) (wceq (cv x3) (crab (λ x6 . wbr (cfv (cv x4) (cv x6)) (cfv (cv x5) (cv x6)) (cv x1)) (λ x6 . co (cv x0) com cmap)))) (λ x5 . com)) (λ x4 . com)))) (csuc com))) (proof)
Theorem df_sate : wceq csate (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cfv (cv x1) (cfv com (co (cv x0) (cin cep (cxp (cv x0) (cv x0))) csat)))) (proof)
Theorem df_fmla : wceq cfmla (cmpt (λ x0 . csuc com) (λ x0 . cdm (cfv (cv x0) (co c0 c0 csat)))) (proof)
Theorem df_gonot : ∀ x0 : ι → ο . wceq (cgon x0) (co x0 x0 cgna) (proof)
Theorem df_goan : wceq cgoa (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cgon (co (cv x0) (cv x1) cgna))) (proof)
Theorem df_goim : wceq cgoi (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (cv x0) (cgon (cv x1)) cgna)) (proof)
Theorem df_goor : wceq cgoo (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (cgon (cv x0)) (cv x1) cgoi)) (proof)
Theorem df_gobi : wceq cgob (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cv x0) (cv x1) cgoi) (co (cv x1) (cv x0) cgoi) cgoa)) (proof)
Theorem df_goeq : wceq cgoq (cmpt2 (λ x0 x1 . com) (λ x0 x1 . com) (λ x0 x1 . csb (csuc (cun (cv x0) (cv x1))) (λ x2 . cgol (co (co (cv x2) (cv x0) cgoe) (co (cv x2) (cv x1) cgoe) cgob) (cv x2)))) (proof)
Theorem df_goex : ∀ x0 x1 : ι → ο . wceq (cgox x0 x1) (cgon (cgol (cgon x0) x1)) (proof)
Theorem df_prv : wceq cprv (copab (λ x0 x1 . wceq (co (cv x0) (cv x1) csate) (co (cv x0) com cmap))) (proof)