Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ο . (wceq ckgen (cmpt (λ x1 . ctop) (λ x1 . crab (λ x2 . wral (λ x3 . wcel (co (cv x1) (cv x3) crest) ccmpwcel (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))) c0wcel (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
type
prop
theory
SetMM
name
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
proof
PUV1k..
Megalodon
-
proofgold address
TMQtS..
creator
36224 PrCmT../1c038..
owner
36224 PrCmT../1c038..
term root
d6135..