Proofgold Address

Known df_trg__df_tdrg__df_tlm__df_tvc__df_ust__df_utop__df_uss__df_usp__df_tus__df_ucn__df_cfilu__df_cusp__df_xms__df_ms__df_tms__df_nm__df_ngp__df_tng : ∀ x0 : ο . (wceq ctrg (crab (λ x1 . wcel (cfv (cv x1) cmgp) ctmd) (λ x1 . cin ctgp crg)) ⟶ wceq ctdrg (crab (λ x1 . wcel (co (cfv (cv x1) cmgp) (cfv (cv x1) cui) cress) ctgp) (λ x1 . cin ctrg cdr)) ⟶ wceq ctlm (crab (λ x1 . wa (wcel (cfv (cv x1) csca) ctrg) (wcel (cfv (cv x1) cscaf) (co (co (cfv (cfv (cv x1) csca) ctopn) (cfv (cv x1) ctopn) ctx) (cfv (cv x1) ctopn) ccn))) (λ x1 . cin ctmd clmod)) ⟶ wceq ctvc (crab (λ x1 . wcel (cfv (cv x1) csca) ctdrg) (λ x1 . ctlm)) ⟶ wceq cust (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . w3a (wss (cv x2) (cpw (cxp (cv x1) (cv x1)))) (wcel (cxp (cv x1) (cv x1)) (cv x2)) (wral (λ x3 . w3a (wral (λ x4 . wss (cv x3) (cv x4) ⟶ wcel (cv x4) (cv x2)) (λ x4 . cpw (cxp (cv x1) (cv x1)))) (wral (λ x4 . wcel (cin (cv x3) (cv x4)) (cv x2)) (λ x4 . cv x2)) (w3a (wss (cres cid (cv x1)) (cv x3)) (wcel (ccnv (cv x3)) (cv x2)) (wrex (λ x4 . wss (ccom (cv x4) (cv x4)) (cv x3)) (λ x4 . cv x2)))) (λ x3 . cv x2))))) ⟶ wceq cutop (cmpt (λ x1 . cuni (crn cust)) (λ x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wss (cima (cv x4) (csn (cv x3))) (cv x2)) (λ x4 . cv x1)) (λ x3 . cv x2)) (λ x2 . cpw (cdm (cuni (cv x1)))))) ⟶ wceq cuss (cmpt (λ x1 . cvv) (λ x1 . co (cfv (cv x1) cunif) (cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs)) crest)) ⟶ wceq cusp (cab (λ x1 . wa (wcel (cfv (cv x1) cuss) (cfv (cfv (cv x1) cbs) cust)) (wceq (cfv (cv x1) ctopn) (cfv (cfv (cv x1) cuss) cutop)))) ⟶ wceq ctus (cmpt (λ x1 . cuni (crn cust)) (λ x1 . co (cpr (cop (cfv cnx cbs) (cdm (cuni (cv x1)))) (cop (cfv cnx cunif) (cv x1))) (cop (cfv cnx cts) (cfv (cv x1) cutop)) csts)) ⟶ wceq cucn (cmpt2 (λ x1 x2 . cuni (crn cust)) (λ x1 x2 . cuni (crn cust)) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wrex (λ x5 . wral (λ x6 . wral (λ x7 . wbr (cv x6) (cv x7) (cv x5) ⟶ wbr (cfv (cv x6) (cv x3)) (cfv (cv x7) (cv x3)) (cv x4)) (λ x7 . cdm (cuni (cv x1)))) (λ x6 . cdm (cuni (cv x1)))) (λ x5 . cv x1)) (λ x4 . cv x2)) (λ x3 . co (cdm (cuni (cv x2))) (cdm (cuni (cv x1))) cmap))) ⟶ wceq ccfilu (cmpt (λ x1 . cuni (crn cust)) (λ x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wss (cxp (cv x4) (cv x4)) (cv x3)) (λ x4 . cv x2)) (λ x3 . cv x1)) (λ x2 . cfv (cdm (cuni (cv x1))) cfbas))) ⟶ wceq ccusp (crab (λ x1 . wral (λ x2 . wcel (cv x2) (cfv (cfv (cv x1) cuss) ccfilu) ⟶ wne (co (cfv (cv x1) ctopn) (cv x2) cflim) c0) (λ x2 . cfv (cfv (cv x1) cbs) cfil)) (λ x1 . cusp)) ⟶ wceq cxme (crab (λ x1 . wceq (cfv (cv x1) ctopn) (cfv (cres (cfv (cv x1) cds) (cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs))) cmopn)) (λ x1 . ctps)) ⟶ wceq cmt (crab (λ x1 . wcel (cres (cfv (cv x1) cds) (cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs))) (cfv (cfv (cv x1) cbs) cme)) (λ x1 . cxme)) ⟶ wceq ctmt (cmpt (λ x1 . cuni (crn cxmt)) (λ x1 . co (cpr (cop (cfv cnx cbs) (cdm (cdm (cv x1)))) (cop (cfv cnx cds) (cv x1))) (cop (cfv cnx cts) (cfv (cv x1) cmopn)) csts)) ⟶ wceq cnm (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . co (cv x2) (cfv (cv x1) c0g) (cfv (cv x1) cds)))) ⟶ wceq cngp (crab (λ x1 . wss (ccom (cfv (cv x1) cnm) (cfv (cv x1) csg)) (cfv (cv x1) cds)) (λ x1 . cin cgrp cmt)) ⟶ wceq ctng (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (co (cv x1) (cop (cfv cnx cds) (ccom (cv x2) (cfv (cv x1) csg))) csts) (cop (cfv cnx cts) (cfv (ccom (cv x2) (cfv (cv x1) csg)) cmopn)) csts)) ⟶ x0) ⟶ x0
Theorem df_trg : wceq ctrg (crab (λ x0 . wcel (cfv (cv x0) cmgp) ctmd) (λ x0 . cin ctgp crg)) (proof)
Theorem df_tdrg : wceq ctdrg (crab (λ x0 . wcel (co (cfv (cv x0) cmgp) (cfv (cv x0) cui) cress) ctgp) (λ x0 . cin ctrg cdr)) (proof)
Theorem df_tlm : wceq ctlm (crab (λ x0 . wa (wcel (cfv (cv x0) csca) ctrg) (wcel (cfv (cv x0) cscaf) (co (co (cfv (cfv (cv x0) csca) ctopn) (cfv (cv x0) ctopn) ctx) (cfv (cv x0) ctopn) ccn))) (λ x0 . cin ctmd clmod)) (proof)
Theorem df_tvc : wceq ctvc (crab (λ x0 . wcel (cfv (cv x0) csca) ctdrg) (λ x0 . ctlm)) (proof)
Theorem df_ust : wceq cust (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . w3a (wss (cv x1) (cpw (cxp (cv x0) (cv x0)))) (wcel (cxp (cv x0) (cv x0)) (cv x1)) (wral (λ x2 . w3a (wral (λ x3 . wss (cv x2) (cv x3) ⟶ wcel (cv x3) (cv x1)) (λ x3 . cpw (cxp (cv x0) (cv x0)))) (wral (λ x3 . wcel (cin (cv x2) (cv x3)) (cv x1)) (λ x3 . cv x1)) (w3a (wss (cres cid (cv x0)) (cv x2)) (wcel (ccnv (cv x2)) (cv x1)) (wrex (λ x3 . wss (ccom (cv x3) (cv x3)) (cv x2)) (λ x3 . cv x1)))) (λ x2 . cv x1))))) (proof)
Theorem df_utop : wceq cutop (cmpt (λ x0 . cuni (crn cust)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wss (cima (cv x3) (csn (cv x2))) (cv x1)) (λ x3 . cv x0)) (λ x2 . cv x1)) (λ x1 . cpw (cdm (cuni (cv x0)))))) (proof)
Theorem df_uss : wceq cuss (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cv x0) cunif) (cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs)) crest)) (proof)
Theorem df_usp : wceq cusp (cab (λ x0 . wa (wcel (cfv (cv x0) cuss) (cfv (cfv (cv x0) cbs) cust)) (wceq (cfv (cv x0) ctopn) (cfv (cfv (cv x0) cuss) cutop)))) (proof)
Theorem df_tus : wceq ctus (cmpt (λ x0 . cuni (crn cust)) (λ x0 . co (cpr (cop (cfv cnx cbs) (cdm (cuni (cv x0)))) (cop (cfv cnx cunif) (cv x0))) (cop (cfv cnx cts) (cfv (cv x0) cutop)) csts)) (proof)
Theorem df_ucn : wceq cucn (cmpt2 (λ x0 x1 . cuni (crn cust)) (λ x0 x1 . cuni (crn cust)) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wral (λ x5 . wral (λ x6 . wbr (cv x5) (cv x6) (cv x4) ⟶ wbr (cfv (cv x5) (cv x2)) (cfv (cv x6) (cv x2)) (cv x3)) (λ x6 . cdm (cuni (cv x0)))) (λ x5 . cdm (cuni (cv x0)))) (λ x4 . cv x0)) (λ x3 . cv x1)) (λ x2 . co (cdm (cuni (cv x1))) (cdm (cuni (cv x0))) cmap))) (proof)
Theorem df_cfilu : wceq ccfilu (cmpt (λ x0 . cuni (crn cust)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wss (cxp (cv x3) (cv x3)) (cv x2)) (λ x3 . cv x1)) (λ x2 . cv x0)) (λ x1 . cfv (cdm (cuni (cv x0))) cfbas))) (proof)
Theorem df_cusp : wceq ccusp (crab (λ x0 . wral (λ x1 . wcel (cv x1) (cfv (cfv (cv x0) cuss) ccfilu) ⟶ wne (co (cfv (cv x0) ctopn) (cv x1) cflim) c0) (λ x1 . cfv (cfv (cv x0) cbs) cfil)) (λ x0 . cusp)) (proof)
Theorem df_xms : wceq cxme (crab (λ x0 . wceq (cfv (cv x0) ctopn) (cfv (cres (cfv (cv x0) cds) (cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs))) cmopn)) (λ x0 . ctps)) (proof)
Theorem df_ms : wceq cmt (crab (λ x0 . wcel (cres (cfv (cv x0) cds) (cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs))) (cfv (cfv (cv x0) cbs) cme)) (λ x0 . cxme)) (proof)
Theorem df_tms : wceq ctmt (cmpt (λ x0 . cuni (crn cxmt)) (λ x0 . co (cpr (cop (cfv cnx cbs) (cdm (cdm (cv x0)))) (cop (cfv cnx cds) (cv x0))) (cop (cfv cnx cts) (cfv (cv x0) cmopn)) csts)) (proof)
Theorem df_nm : wceq cnm (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . co (cv x1) (cfv (cv x0) c0g) (cfv (cv x0) cds)))) (proof)
Theorem df_ngp : wceq cngp (crab (λ x0 . wss (ccom (cfv (cv x0) cnm) (cfv (cv x0) csg)) (cfv (cv x0) cds)) (λ x0 . cin cgrp cmt)) (proof)
Theorem df_tng : wceq ctng (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cv x0) (cop (cfv cnx cds) (ccom (cv x1) (cfv (cv x0) csg))) csts) (cop (cfv cnx cts) (cfv (ccom (cv x1) (cfv (cv x0) csg)) cmopn)) csts)) (proof)