Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ο . (wceq cmfsh (cslot c8)wceq cmevl (cslot c9)wceq cmvl (cmpt (λ x1 . cvv) (λ x1 . cixp (λ x2 . cfv (cv x1) cmvar) (λ x2 . cima (cfv (cv x1) cmuv) (csn (cfv (cv x2) (cfv (cv x1) cmty))))))wceq cmvsb (cmpt (λ x1 . cvv) (λ x1 . coprab (λ x2 x3 x4 . w3a (wa (wcel (cv x2) (crn (cfv (cv x1) cmsub))) (wcel (cv x3) (cfv (cv x1) cmvl))) (wral (λ x5 . wbr (cv x3) (cfv (cfv (cv x5) (cfv (cv x1) cmvh)) (cv x2)) (cdm (cfv (cv x1) cmevl))) (λ x5 . cfv (cv x1) cmvar)) (wceq (cv x4) (cmpt (λ x5 . cfv (cv x1) cmvar) (λ x5 . co (cv x3) (cfv (cfv (cv x5) (cfv (cv x1) cmvh)) (cv x2)) (cfv (cv x1) cmevl)))))))wceq cmfr (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wceq (ccnv (cv x2)) (cv x2)) (wral (λ x3 . wral (λ x4 . wrex (λ x5 . wss (cv x4) (cima (cv x2) (csn (cv x5)))) (λ x5 . cima (cfv (cv x1) cmuv) (csn (cv x3)))) (λ x4 . cin (cpw (cfv (cv x1) cmuv)) cfn)) (λ x3 . cfv (cv x1) cmvt))) (λ x2 . cpw (cxp (cfv (cv x1) cmuv) (cfv (cv x1) cmuv)))))wceq cmdl (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wa (w3a (wss (cv x2) (cxp (cfv (cv x1) cmtc) cvv)) (wcel (cv x6) (cfv (cv x1) cmfr)) (wcel (cv x5) (co (cv x2) (cxp (cv x4) (cfv (cv x1) cmex)) cpm))) (wral (λ x7 . wa (w3a (wral (λ x8 . wss (cima (cv x5) (csn (cop (cv x7) (cv x8)))) (cima (cv x2) (csn (cfv (cv x8) c1st)))) (λ x8 . cv x3)) (wral (λ x8 . wbr (cop (cv x7) (cfv (cv x8) (cfv (cv x1) cmvh))) (cfv (cv x8) (cv x7)) (cv x5)) (λ x8 . cfv (cv x1) cmvar)) (∀ x8 x9 x10 . wcel (cotp (cv x8) (cv x9) (cv x10)) (cfv (cv x1) cmax)wa (∀ x11 x12 . wbr (cv x11) (cv x12) (cv x8)wbr (cfv (cv x11) (cv x7)) (cfv (cv x12) (cv x7)) (cv x6)) (wss (cv x9) (cima (cdm (cv x5)) (csn (cv x7))))wbr (cv x7) (cv x10) (cdm (cv x5)))) (w3a (wral (λ x8 . wral (λ x9 . ∀ x10 . wbr (cop (cv x8) (cv x7)) (cv x10) (cfv (cv x1) cmvsb)wceq (cima (cv x5) (csn (cop (cv x7) (cfv (cv x9) (cv x8))))) (cima (cv x5) (csn (cop (cv x10) (cv x9))))) (λ x9 . cfv (cv x1) cmex)) (λ x8 . crn (cfv (cv x1) cmsub))) (wral (λ x8 . wral (λ x9 . wceq (cres (cv x7) (cfv (cv x9) (cfv (cv x1) cmvrs))) (cres (cv x8) (cfv (cv x9) (cfv (cv x1) cmvrs)))wceq (cima (cv x5) (csn (cop (cv x7) (cv x9)))) (cima (cv x5) (csn (cop (cv x8) (cv x9))))) (λ x9 . cv x3)) (λ x8 . cv x4)) (wral (λ x8 . wral (λ x9 . wss (cima (cv x7) (cfv (cv x9) (cfv (cv x1) cmvrs))) (cima (cv x6) (csn (cv x8)))wss (cima (cv x5) (csn (cop (cv x7) (cv x9)))) (cima (cv x6) (csn (cv x8)))) (λ x9 . cv x3)) (λ x8 . cv x2)))) (λ x7 . cv x4))) (cfv (cv x1) cmfsh)) (cfv (cv x1) cmevl)) (cfv (cv x1) cmvl)) (cfv (cv x1) cmex)) (cfv (cv x1) cmuv)) (λ x1 . cmfs))wceq cusyn (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cmuv) (λ x2 . cop (cfv (cfv (cv x2) c1st) (cfv (cv x1) cmsy)) (cfv (cv x2) c2nd))))(∀ x1 . wceq cgmdl (crab (λ x2 . w3a (wral (λ x3 . wss (cima (cfv (cv x2) cmuv) (csn (cv x3))) (cima (cfv (cv x2) cmuv) (csn (cfv (cv x3) (cfv (cv x2) cmsy))))) (λ x3 . cfv (cv x2) cmtc)) (wral (λ x3 . wral (λ x4 . wb (wbr (cv x3) (cv x4) (cfv (cv x2) cmfsh)) (wbr (cv x3) (cfv (cv x4) (cfv (cv x2) cusyn)) (cfv (cv x2) cmfsh))) (λ x4 . cfv (cv x1) cmuv)) (λ x3 . cfv (cv x1) cmuv)) (wral (λ x3 . wral (λ x4 . wceq (cima (cfv (cv x2) cmevl) (csn (cop (cv x3) (cv x4)))) (cin (cima (cfv (cv x2) cmevl) (csn (cop (cv x3) (cfv (cv x4) (cfv (cv x2) cmesy))))) (cima (cfv (cv x2) cmuv) (csn (cfv (cv x4) c1st))))) (λ x4 . cfv (cv x2) cmex)) (λ x3 . cfv (cv x2) cmvl))) (λ x2 . cin cmgfs cmdl)))wceq cmitp (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cmsa) (λ x2 . cmpt (λ x3 . cixp (λ x4 . cfv (cv x2) (cfv (cv x1) cmvrs)) (λ x4 . cima (cfv (cv x1) cmuv) (csn (cfv (cv x4) (cfv (cv x1) cmty))))) (λ x3 . cio (λ x4 . wrex (λ x5 . wa (wceq (cv x3) (cres (cv x5) (cfv (cv x2) (cfv (cv x1) cmvrs)))) (wceq (cv x4) (co (cv x5) (cv x2) (cfv (cv x1) cmevl)))) (λ x5 . cfv (cv x1) cmvl))))))wceq cmfitp (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cixp (λ x3 . cfv (cv x1) cmsa) (λ x3 . co (cima (cfv (cv x1) cmuv) (csn (cfv (cv x3) (cfv (cv x1) c1st)))) (cixp (λ x4 . cfv (cv x3) (cfv (cv x1) cmvrs)) (λ x4 . cima (cfv (cv x1) cmuv) (csn (cfv (cv x4) (cfv (cv x1) cmty))))) cmap)) (λ x2 . crio (λ x3 . wral (λ x4 . w3a (wral (λ x5 . wbr (cop (cv x4) (cfv (cv x5) (cfv (cv x1) cmvh))) (cfv (cv x5) (cv x4)) (cv x3)) (λ x5 . cfv (cv x1) cmvar)) (∀ x5 x6 x7 . wbr (cv x5) (cop (cv x6) (cv x7)) (cfv (cv x1) cmst)wbr (cop (cv x4) (cv x5)) (cfv (cmpt (λ x8 . cfv (cv x6) (cfv (cv x1) cmvrs)) (λ x8 . co (cv x4) (cfv (cfv (cv x8) (cfv (cv x1) cmvh)) (cv x7)) (cv x3))) (cv x2)) (cv x3)) (wral (λ x5 . wceq (cima (cv x3) (csn (cop (cv x4) (cv x5)))) (cin (cima (cv x3) (csn (cop (cv x4) (cfv (cv x5) (cfv (cv x1) cmesy))))) (cima (cfv (cv x1) cmuv) (csn (cfv (cv x5) c1st))))) (λ x5 . cfv (cv x1) cmex))) (λ x4 . cfv (cv x1) cmvl)) (λ x3 . co (cfv (cv x1) cmuv) (cxp (cfv (cv x1) cmvl) (cfv (cv x1) cmex)) cpm))))wceq citr (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . ciun (λ x3 . cfv (co (cv x1) (cv x2) cress) cmn1) (λ x3 . cima (ccnv (cv x3)) (csn (cfv (cv x1) c0g)))))wceq ccpms (cmpt (λ x1 . cvv) (λ x1 . csb (co (co (cv x1) cn cpws) (cfv (cfv (cv x1) cds) cca) cress) (λ x2 . csb (cfv (cv x2) cbs) (λ x3 . csb (copab (λ x4 x5 . wa (wss (cpr (cv x4) (cv x5)) (cv x3)) (wral (λ x6 . wrex (λ x7 . wf (cfv (cv x7) cuz) (co (cfv (cv x7) (cv x5)) (cv x6) (cfv (cfv (cv x1) cds) cbl)) (cres (cv x4) (cfv (cv x7) cuz))) (λ x7 . cz)) (λ x6 . crp)))) (λ x4 . co (co (cv x2) (cv x4) cqus) (csn (cop (cfv cnx cds) (coprab (λ x5 x6 x7 . wrex (λ x8 . wrex (λ x9 . wa (wa (wceq (cv x5) (cec (cv x8) (cv x4))) (wceq (cv x6) (cec (cv x9) (cv x4)))) (wbr (co (cv x8) (cv x9) (cof (cfv (cv x2) cds))) (cv x7) cli)) (λ x9 . cv x3)) (λ x8 . cv x3))))) csts)))))wceq chlb (cmpt (λ x1 . cvv) (λ x1 . csb (ciun (λ x2 . cn) (λ x2 . cxp (csn (cv x2)) (cdm (cfv (cv x2) (cv x1))))) (λ x2 . csb (cint (cab (λ x3 . wa (wer (cv x2) (cv x3)) (wss (cmpt (λ x4 . cv x2) (λ x4 . cop (co (cfv (cv x4) c1st) c1 caddc) (cfv (cfv (cv x4) c2nd) (cfv (cfv (cv x4) c1st) (cv x1))))) (cv x3))))) (λ x3 . cop (cqs (cv x2) (cv x3)) (cmpt (λ x4 . cn) (λ x4 . cmpt (λ x5 . cdm (cfv (cv x4) (cv x1))) (λ x5 . cec (cop (cv x4) (cv x5)) (cv x3))))))))wceq chlim (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cv x2) chlb) (λ x3 . csb (cfv (cv x3) c1st) (λ x4 . csb (cfv (cv x3) c2nd) (λ x5 . cun (ctp (cop (cfv cnx cbs) (cv x4)) (cop (cfv cnx cplusg) (ciun (λ x6 . cn) (λ x6 . crn (cmpt2 (λ x7 x8 . cdm (cfv (cv x6) (cv x5))) (λ x7 x8 . cdm (cfv (cv x6) (cv x5))) (λ x7 x8 . cop (cop (cfv (cv x7) (cfv (cv x6) (cv x5))) (cfv (cv x8) (cfv (cv x6) (cv x5)))) (cfv (co (cv x7) (cv x8) (cfv (cfv (cv x6) (cv x1)) cplusg)) (cfv (cv x6) (cv x5)))))))) (cop (cfv cnx cmulr) (ciun (λ x6 . cn) (λ x6 . crn (cmpt2 (λ x7 x8 . cdm (cfv (cv x6) (cv x5))) (λ x7 x8 . cdm (cfv (cv x6) (cv x5))) (λ x7 x8 . cop (cop (cfv (cv x7) (cfv (cv x6) (cv x5))) (cfv (cv x8) (cfv (cv x6) (cv x5)))) (cfv (co (cv x7) (cv x8) (cfv (cfv (cv x6) (cv x1)) cmulr)) (cfv (cv x6) (cv x5))))))))) (ctp (cop (cfv cnx ctopn) (crab (λ x6 . wral (λ x7 . wcel (cima (ccnv (cfv (cv x7) (cv x5))) (cv x6)) (cfv (cfv (cv x7) (cv x1)) ctopn)) (λ x7 . cn)) (λ x6 . cpw (cv x4)))) (cop (cfv cnx cds) (ciun (λ x6 . cn) (λ x6 . crn (cmpt2 (λ x7 x8 . cdm (cfv (cv x6) (cfv (cv x6) (cv x5)))) (λ x7 x8 . cdm (cfv (cv x6) (cfv (cv x6) (cv x5)))) (λ x7 x8 . cop (cop (cfv (cv x7) (cfv (cv x6) (cv x5))) (cfv (cv x8) (cfv (cv x6) (cv x5)))) (co (cv x7) (cv x8) (cfv (cfv (cv x6) (cv x1)) cds))))))) (cop (cfv cnx cple) (ciun (λ x6 . cn) (λ x6 . ccom (ccnv (cfv (cv x6) (cv x5))) (ccom (cfv (cfv (cv x6) (cv x1)) cple) (cfv (cv x6) (cv x5))))))))))))wceq cpfl (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cv x1) cpl1) (λ x3 . csb (cfv (csn (cv x2)) (cfv (cv x3) crsp)) (λ x4 . csb (cmpt (λ x5 . cfv (cv x1) cbs) (λ x5 . cec (co (cv x5) (cfv (cv x3) cur) (cfv (cv x3) cvsca)) (co (cv x3) (cv x4) cqg))) (λ x5 . cop (csb (co (cv x3) (co (cv x3) (cv x4) cqg) cqus) (λ x6 . co (co (cv x6) (crio (λ x7 . wceq (ccom (cv x7) (cv x5)) (cfv (cv x1) cnm)) (λ x7 . cfv (cv x6) cabv)) ctng) (cop (cfv cnx cple) (csb (cmpt (λ x7 . cfv (cv x6) cbs) (λ x7 . crio (λ x8 . wbr (co (cv x1) (cv x8) cdg1) (co (cv x1) (cv x2) cdg1) clt) (λ x8 . cv x7))) (λ x7 . ccom (ccnv (cv x7)) (ccom (cfv (cv x3) cple) (cv x7))))) csts)) (cv x5))))))wceq csf1 (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (cv x1) cpl1) (λ x3 . cfv (cfv (co c1 (co (cv x1) (cv x3) cdg1) cfz) ccrd) (crdg (cmpt2 (λ x4 x5 . cvv) (λ x4 x5 . cvv) (λ x4 x5 . csb (cfv (cv x4) cmpl) (λ x6 . csb (crab (λ x7 . wa (wbr (cv x7) (ccom (cv x3) (cv x5)) (cfv (cv x6) cdsr)) (wbr c1 (co (cv x4) (cv x7) cdg1) clt)) (λ x7 . cin (cfv (cv x4) cmn1) (cfv (cv x6) cir))) (λ x7 . cif (wo (wceq (ccom (cv x3) (cv x5)) (cfv (cv x6) c0g)) (wceq (cv x7) c0)) (cop (cv x4) (cv x5)) (csb (cfv (cv x7) cglb) (λ x8 . csb (co (cv x4) (cv x8) cpfl) (λ x9 . cop (cfv (cv x9) c1st) (ccom (cv x5) (cfv (cv x9) c2nd))))))))) (cv x2)))))wceq csf (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cio (λ x3 . wex (λ x4 . wa (wiso (co c1 (cfv (cv x2) chash) cfz) (cv x2) clt (cfv (cv x1) cplt) (cv x4)) (wceq (cv x3) (cfv (cfv (cv x2) chash) (cseq (cmpt2 (λ x5 x6 . cvv) (λ x5 x6 . cvv) (λ x5 x6 . cfv (cv x6) (co (cv x1) (cv x5) csf1))) (cun (cv x4) (csn (cop cc0 (cop (cv x1) (cres cid (cfv (cv x1) cbs)))))) cc0)))))))wceq cpsl (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . co (cin (cpw (cfv (cv x1) cbs)) cfn) cn cmap) (λ x1 x2 . csb (ccom c1st (cseq (cmpt2 (λ x3 x4 . cvv) (λ x3 x4 . cvv) (λ x3 x4 . csb (cfv (cv x3) c1st) (λ x5 . csb (cfv (cv x5) c1st) (λ x6 . csb (co (cv x6) (crn (cmpt (λ x7 . cv x4) (λ x7 . ccom (cv x7) (cfv (cv x3) c2nd)))) csf) (λ x7 . cop (cv x7) (ccom (cfv (cv x3) c2nd) (cfv (cv x7) c2nd))))))) (cun (cv x2) (csn (cop cc0 (cop (cop (cv x1) c0) (cres cid (cfv (cv x1) cbs)))))) cc0)) (λ x3 . co (ccom c1st (co (cv x3) c1 cshi)) (ccom c2nd (cv x3)) chlim)))x0)x0
type
prop
theory
SetMM
name
df_mfsh__df_mevl__df_mvl__df_mvsb__df_mfrel__df_mdl__df_musyn__df_gmdl__df_mitp__df_mfitp__df_irng__df_cplmet__df_homlimb__df_homlim__df_plfl__df_sfl1__df_sfl__df_psl
proof
PUV1k..
Megalodon
-
proofgold address
TMLG8..
creator
36224 PrCmT../c5356..
owner
36224 PrCmT../c5356..
term root
8b55d..