Proofgold Asset

Known df_kgen__df_tx__df_xko__df_kq__df_hmeo__df_hmph__df_fil__df_ufil__df_ufl__df_fm__df_flim__df_flf__df_fcls__df_fcf__df_cnext__df_tmd__df_tgp__df_tsms : ∀ x0 : ο . (wceq ckgen (cmpt (λ x1 . ctop) (λ x1 . crab (λ x2 . wral (λ x3 . wcel (co (cv x1) (cv x3) crest) ccmp ⟶ wcel (cin (cv x2) (cv x3)) (co (cv x1) (cv x3) crest)) (λ x3 . cpw (cuni (cv x1)))) (λ x2 . cpw (cuni (cv x1))))) ⟶ wceq ctx (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cfv (crn (cmpt2 (λ x3 x4 . cv x1) (λ x3 x4 . cv x2) (λ x3 x4 . cxp (cv x3) (cv x4)))) ctg)) ⟶ wceq cxko (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . ctop) (λ x1 x2 . cfv (cfv (crn (cmpt2 (λ x3 x4 . crab (λ x5 . wcel (co (cv x2) (cv x5) crest) ccmp) (λ x5 . cpw (cuni (cv x2)))) (λ x3 x4 . cv x1) (λ x3 x4 . crab (λ x5 . wss (cima (cv x5) (cv x3)) (cv x4)) (λ x5 . co (cv x2) (cv x1) ccn)))) cfi) ctg)) ⟶ wceq ckq (cmpt (λ x1 . ctop) (λ x1 . co (cv x1) (cmpt (λ x2 . cuni (cv x1)) (λ x2 . crab (λ x3 . wcel (cv x2) (cv x3)) (λ x3 . cv x1))) cqtop)) ⟶ wceq chmeo (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . ctop) (λ x1 x2 . crab (λ x3 . wcel (ccnv (cv x3)) (co (cv x2) (cv x1) ccn)) (λ x3 . co (cv x1) (cv x2) ccn))) ⟶ wceq chmph (cima (ccnv chmeo) (cdif cvv c1o)) ⟶ wceq cfil (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wne (cin (cv x2) (cpw (cv x3))) c0 ⟶ wcel (cv x3) (cv x2)) (λ x3 . cpw (cv x1))) (λ x2 . cfv (cv x1) cfbas))) ⟶ wceq cufil (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wo (wcel (cv x3) (cv x2)) (wcel (cdif (cv x1) (cv x3)) (cv x2))) (λ x3 . cpw (cv x1))) (λ x2 . cfv (cv x1) cfil))) ⟶ wceq cufl (cab (λ x1 . wral (λ x2 . wrex (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cfv (cv x1) cufil)) (λ x2 . cfv (cv x1) cfil))) ⟶ wceq cfm (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (cdm (cv x2)) cfbas) (λ x3 . co (cv x1) (crn (cmpt (λ x4 . cv x3) (λ x4 . cima (cv x2) (cv x4)))) cfg))) ⟶ wceq cflim (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . cuni (crn cfil)) (λ x1 x2 . crab (λ x3 . wa (wss (cfv (csn (cv x3)) (cfv (cv x1) cnei)) (cv x2)) (wss (cv x2) (cpw (cuni (cv x1))))) (λ x3 . cuni (cv x1)))) ⟶ wceq cflf (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . cuni (crn cfil)) (λ x1 x2 . cmpt (λ x3 . co (cuni (cv x1)) (cuni (cv x2)) cmap) (λ x3 . co (cv x1) (cfv (cv x2) (co (cuni (cv x1)) (cv x3) cfm)) cflim))) ⟶ wceq cfcls (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . cuni (crn cfil)) (λ x1 x2 . cif (wceq (cuni (cv x1)) (cuni (cv x2))) (ciin (λ x3 . cv x2) (λ x3 . cfv (cv x3) (cfv (cv x1) ccl))) c0)) ⟶ wceq cfcf (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . cuni (crn cfil)) (λ x1 x2 . cmpt (λ x3 . co (cuni (cv x1)) (cuni (cv x2)) cmap) (λ x3 . co (cv x1) (cfv (cv x2) (co (cuni (cv x1)) (cv x3) cfm)) cfcls))) ⟶ wceq ccnext (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . ctop) (λ x1 x2 . cmpt (λ x3 . co (cuni (cv x2)) (cuni (cv x1)) cpm) (λ x3 . ciun (λ x4 . cfv (cdm (cv x3)) (cfv (cv x1) ccl)) (λ x4 . cxp (csn (cv x4)) (cfv (cv x3) (co (cv x2) (co (cfv (csn (cv x4)) (cfv (cv x1) cnei)) (cdm (cv x3)) crest) cflf)))))) ⟶ wceq ctmd (crab (λ x1 . wsbc (λ x2 . wcel (cfv (cv x1) cplusf) (co (co (cv x2) (cv x2) ctx) (cv x2) ccn)) (cfv (cv x1) ctopn)) (λ x1 . cin cmnd ctps)) ⟶ wceq ctgp (crab (λ x1 . wsbc (λ x2 . wcel (cfv (cv x1) cminusg) (co (cv x2) (cv x2) ccn)) (cfv (cv x1) ctopn)) (λ x1 . cin cgrp ctmd)) ⟶ wceq ctsu (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cin (cpw (cdm (cv x2))) cfn) (λ x3 . cfv (cmpt (λ x4 . cv x3) (λ x4 . co (cv x1) (cres (cv x2) (cv x4)) cgsu)) (co (cfv (cv x1) ctopn) (co (cv x3) (crn (cmpt (λ x4 . cv x3) (λ x4 . crab (λ x5 . wss (cv x4) (cv x5)) (λ x5 . cv x3)))) cfg) cflf)))) ⟶ x0) ⟶ x0
Theorem df_kgen : wceq ckgen (cmpt (λ x0 . ctop) (λ x0 . crab (λ x1 . wral (λ x2 . wcel (co (cv x0) (cv x2) crest) ccmp ⟶ wcel (cin (cv x1) (cv x2)) (co (cv x0) (cv x2) crest)) (λ x2 . cpw (cuni (cv x0)))) (λ x1 . cpw (cuni (cv x0))))) (proof)
Theorem df_tx : wceq ctx (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cfv (crn (cmpt2 (λ x2 x3 . cv x0) (λ x2 x3 . cv x1) (λ x2 x3 . cxp (cv x2) (cv x3)))) ctg)) (proof)
Theorem df_xko : wceq cxko (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . cfv (cfv (crn (cmpt2 (λ x2 x3 . crab (λ x4 . wcel (co (cv x1) (cv x4) crest) ccmp) (λ x4 . cpw (cuni (cv x1)))) (λ x2 x3 . cv x0) (λ x2 x3 . crab (λ x4 . wss (cima (cv x4) (cv x2)) (cv x3)) (λ x4 . co (cv x1) (cv x0) ccn)))) cfi) ctg)) (proof)
Theorem df_kq : wceq ckq (cmpt (λ x0 . ctop) (λ x0 . co (cv x0) (cmpt (λ x1 . cuni (cv x0)) (λ x1 . crab (λ x2 . wcel (cv x1) (cv x2)) (λ x2 . cv x0))) cqtop)) (proof)
Theorem df_hmeo : wceq chmeo (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . crab (λ x2 . wcel (ccnv (cv x2)) (co (cv x1) (cv x0) ccn)) (λ x2 . co (cv x0) (cv x1) ccn))) (proof)
Theorem df_hmph : wceq chmph (cima (ccnv chmeo) (cdif cvv c1o)) (proof)
Theorem df_fil : wceq cfil (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wne (cin (cv x1) (cpw (cv x2))) c0 ⟶ wcel (cv x2) (cv x1)) (λ x2 . cpw (cv x0))) (λ x1 . cfv (cv x0) cfbas))) (proof)
Theorem df_ufil : wceq cufil (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wo (wcel (cv x2) (cv x1)) (wcel (cdif (cv x0) (cv x2)) (cv x1))) (λ x2 . cpw (cv x0))) (λ x1 . cfv (cv x0) cfil))) (proof)
Theorem df_ufl : wceq cufl (cab (λ x0 . wral (λ x1 . wrex (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cfv (cv x0) cufil)) (λ x1 . cfv (cv x0) cfil))) (proof)
Theorem df_fm : wceq cfm (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (cdm (cv x1)) cfbas) (λ x2 . co (cv x0) (crn (cmpt (λ x3 . cv x2) (λ x3 . cima (cv x1) (cv x3)))) cfg))) (proof)
Theorem df_flim : wceq cflim (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (crn cfil)) (λ x0 x1 . crab (λ x2 . wa (wss (cfv (csn (cv x2)) (cfv (cv x0) cnei)) (cv x1)) (wss (cv x1) (cpw (cuni (cv x0))))) (λ x2 . cuni (cv x0)))) (proof)
Theorem df_flf : wceq cflf (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (crn cfil)) (λ x0 x1 . cmpt (λ x2 . co (cuni (cv x0)) (cuni (cv x1)) cmap) (λ x2 . co (cv x0) (cfv (cv x1) (co (cuni (cv x0)) (cv x2) cfm)) cflim))) (proof)
Theorem df_fcls : wceq cfcls (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (crn cfil)) (λ x0 x1 . cif (wceq (cuni (cv x0)) (cuni (cv x1))) (ciin (λ x2 . cv x1) (λ x2 . cfv (cv x2) (cfv (cv x0) ccl))) c0)) (proof)
Theorem df_fcf : wceq cfcf (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (crn cfil)) (λ x0 x1 . cmpt (λ x2 . co (cuni (cv x0)) (cuni (cv x1)) cmap) (λ x2 . co (cv x0) (cfv (cv x1) (co (cuni (cv x0)) (cv x2) cfm)) cfcls))) (proof)
Theorem df_cnext : wceq ccnext (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . cmpt (λ x2 . co (cuni (cv x1)) (cuni (cv x0)) cpm) (λ x2 . ciun (λ x3 . cfv (cdm (cv x2)) (cfv (cv x0) ccl)) (λ x3 . cxp (csn (cv x3)) (cfv (cv x2) (co (cv x1) (co (cfv (csn (cv x3)) (cfv (cv x0) cnei)) (cdm (cv x2)) crest) cflf)))))) (proof)
Theorem df_tmd : wceq ctmd (crab (λ x0 . wsbc (λ x1 . wcel (cfv (cv x0) cplusf) (co (co (cv x1) (cv x1) ctx) (cv x1) ccn)) (cfv (cv x0) ctopn)) (λ x0 . cin cmnd ctps)) (proof)
Theorem df_tgp : wceq ctgp (crab (λ x0 . wsbc (λ x1 . wcel (cfv (cv x0) cminusg) (co (cv x1) (cv x1) ccn)) (cfv (cv x0) ctopn)) (λ x0 . cin cgrp ctmd)) (proof)
Theorem df_tsms : wceq ctsu (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cin (cpw (cdm (cv x1))) cfn) (λ x2 . cfv (cmpt (λ x3 . cv x2) (λ x3 . co (cv x0) (cres (cv x1) (cv x3)) cgsu)) (co (cfv (cv x0) ctopn) (co (cv x2) (crn (cmpt (λ x3 . cv x2) (λ x3 . crab (λ x4 . wss (cv x3) (cv x4)) (λ x4 . cv x2)))) cfg) cflf)))) (proof)