Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ο . (wceq cmend (cmpt (λ x1 . cvv) (λ x1 . csb (co (cv x1) (cv x1) clmhm) (λ x2 . cun (ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . co (cv x3) (cv x4) (cof (cfv (cv x1) cplusg))))) (cop (cfv cnx cmulr) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . ccom (cv x3) (cv x4))))) (cpr (cop (cfv cnx csca) (cfv (cv x1) csca)) (cop (cfv cnx cvsca) (cmpt2 (λ x3 x4 . cfv (cfv (cv x1) csca) cbs) (λ x3 x4 . cv x2) (λ x3 x4 . co (cxp (cfv (cv x1) cbs) (csn (cv x3))) (cv x4) (cof (cfv (cv x1) cvsca)))))))))wceq csdrg (cmpt (λ x1 . cdr) (λ x1 . crab (λ x2 . wcel (co (cv x1) (cv x2) cress) cdr) (λ x2 . cfv (cv x1) csubrg)))wceq ccytp (cmpt (λ x1 . cn) (λ x1 . co (cfv (cfv ccnfld cpl1) cmgp) (cmpt (λ x2 . cima (ccnv (cfv (co (cfv ccnfld cmgp) (cdif cc (csn cc0)) cress) cod)) (csn (cv x1))) (λ x2 . co (cfv ccnfld cv1) (cfv (cv x2) (cfv (cfv ccnfld cpl1) cascl)) (cfv (cfv ccnfld cpl1) csg))) cgsu))wceq ctopsep (crab (λ x1 . wrex (λ x2 . wa (wbr (cv x2) com cdom) (wceq (cfv (cv x2) (cfv (cv x1) ccl)) (cuni (cv x1)))) (λ x2 . cpw (cuni (cv x1)))) (λ x1 . ctop))wceq ctoplnd (crab (λ x1 . wral (λ x2 . wceq (cuni (cv x1)) (cuni (cv x2))wrex (λ x3 . wa (wbr (cv x3) com cdom) (wceq (cuni (cv x1)) (cuni (cv x3)))) (λ x3 . cpw (cv x1))) (λ x2 . cpw (cv x1))) (λ x1 . ctop))wceq crcl (cmpt (λ x1 . cvv) (λ x1 . cint (cab (λ x2 . wa (wss (cv x1) (cv x2)) (wss (cres cid (cun (cdm (cv x2)) (crn (cv x2)))) (cv x2))))))(∀ x1 x2 : ι → ο . wb (whe x1 x2) (wss (cima x2 x1) x1))(∀ x1 x2 : ο . x1x2x1)(∀ x1 x2 x3 : ο . (x1x2x3)(x1x2)x1x3)(∀ x1 x2 x3 : ο . (x1x2x3)x2x1x3)(∀ x1 x2 : ο . (x1x2)wn x2wn x1)(∀ x1 : ο . wn (wn x1)x1)(∀ x1 : ο . x1wn (wn x1))(∀ x1 x2 x3 x4 : ο . wb x1 x2wif x1 x4 x3wif x2 x4 x3)(∀ x1 : ο . wb x1 x1)(∀ x1 x2 x3 : ο . wa x2 x3wif x1 x2 x3)(∀ x1 : ι → ο . ∀ x2 x3 : ι → ι → ο . ∀ x4 . wceq (x2 x4) (x3 x4)wsbc x1 (x2 x4)wsbc x1 (x3 x4))(∀ x1 : ι → ο . wceq x1 x1)x0)x0
type
prop
theory
SetMM
name
df_mend__df_sdrg__df_cytp__df_topsep__df_toplnd__df_rcl__df_he__ax_frege1__ax_frege2__ax_frege8__ax_frege28__ax_frege31__ax_frege41__ax_frege52a__ax_frege54a__ax_frege58a__ax_frege52c__ax_frege54c
proof
PUV1k..
Megalodon
-
proofgold address
TMMvy..
creator
36224 PrCmT../2c78f..
owner
36224 PrCmT../2c78f..
term root
082ae..