Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ο . (wceq cpolN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) catm)) (λ x2 . cin (cfv (cv x1) catm) (ciin (λ x3 . cv x2) (λ x3 . cfv (cfv (cv x3) (cfv (cv x1) coc)) (cfv (cv x1) cpmap))))))wceq cpscN (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wa (wss (cv x2) (cfv (cv x1) catm)) (wceq (cfv (cfv (cv x2) (cfv (cv x1) cpolN)) (cfv (cv x1) cpolN)) (cv x2)))))wceq clh (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wbr (cv x2) (cfv (cv x1) cp1) (cfv (cv x1) ccvr)) (λ x2 . cfv (cv x1) cbs)))wceq claut (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wa (wf1o (cfv (cv x1) cbs) (cfv (cv x1) cbs) (cv x2)) (wral (λ x3 . wral (λ x4 . wb (wbr (cv x3) (cv x4) (cfv (cv x1) cple)) (wbr (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x1) cple))) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) cbs)))))wceq cwpointsN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) catm) (λ x2 . cdif (cfv (cv x1) catm) (cfv (csn (cv x2)) (cfv (cv x1) cpolN)))))wceq cpautN (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wa (wf1o (cfv (cv x1) cpsubsp) (cfv (cv x1) cpsubsp) (cv x2)) (wral (λ x3 . wral (λ x4 . wb (wss (cv x3) (cv x4)) (wss (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)))) (λ x4 . cfv (cv x1) cpsubsp)) (λ x3 . cfv (cv x1) cpsubsp)))))wceq cldil (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . crab (λ x3 . wral (λ x4 . wbr (cv x4) (cv x2) (cfv (cv x1) cple)wceq (cfv (cv x4) (cv x3)) (cv x4)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) claut))))wceq cltrn (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wa (wn (wbr (cv x4) (cv x2) (cfv (cv x1) cple))) (wn (wbr (cv x5) (cv x2) (cfv (cv x1) cple)))wceq (co (co (cv x4) (cfv (cv x4) (cv x3)) (cfv (cv x1) cjn)) (cv x2) (cfv (cv x1) cmee)) (co (co (cv x5) (cfv (cv x5) (cv x3)) (cfv (cv x1) cjn)) (cv x2) (cfv (cv x1) cmee))) (λ x5 . cfv (cv x1) catm)) (λ x4 . cfv (cv x1) catm)) (λ x3 . cfv (cv x2) (cfv (cv x1) cldil)))))wceq cdilN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) catm) (λ x2 . crab (λ x3 . wral (λ x4 . wss (cv x4) (cfv (cv x2) (cfv (cv x1) cwpointsN))wceq (cfv (cv x4) (cv x3)) (cv x4)) (λ x4 . cfv (cv x1) cpsubsp)) (λ x3 . cfv (cv x1) cpautN))))wceq ctrnN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) catm) (λ x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wceq (cin (co (cv x4) (cfv (cv x4) (cv x3)) (cfv (cv x1) cpadd)) (cfv (csn (cv x2)) (cfv (cv x1) cpolN))) (cin (co (cv x5) (cfv (cv x5) (cv x3)) (cfv (cv x1) cpadd)) (cfv (csn (cv x2)) (cfv (cv x1) cpolN)))) (λ x5 . cfv (cv x2) (cfv (cv x1) cwpointsN))) (λ x4 . cfv (cv x2) (cfv (cv x1) cwpointsN))) (λ x3 . cfv (cv x2) (cfv (cv x1) cdilN)))))wceq ctrl (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 . crio (λ x4 . wral (λ x5 . wn (wbr (cv x5) (cv x2) (cfv (cv x1) cple))wceq (cv x4) (co (co (cv x5) (cfv (cv x5) (cv x3)) (cfv (cv x1) cjn)) (cv x2) (cfv (cv x1) cmee))) (λ x5 . cfv (cv x1) catm)) (λ x4 . cfv (cv x1) cbs)))))wceq ctgrp (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cpr (cop (cfv cnx cbs) (cfv (cv x2) (cfv (cv x1) cltrn))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . ccom (cv x3) (cv x4)))))))wceq ctendo (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cab (λ x3 . w3a (wf (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) cltrn)) (cv x3)) (wral (λ x4 . wral (λ x5 . wceq (cfv (ccom (cv x4) (cv x5)) (cv x3)) (ccom (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)))) (λ x5 . cfv (cv x2) (cfv (cv x1) cltrn))) (λ x4 . cfv (cv x2) (cfv (cv x1) cltrn))) (wral (λ x4 . wbr (cfv (cfv (cv x4) (cv x3)) (cfv (cv x2) (cfv (cv x1) ctrl))) (cfv (cv x4) (cfv (cv x2) (cfv (cv x1) ctrl))) (cfv (cv x1) cple)) (λ x4 . cfv (cv x2) (cfv (cv x1) cltrn)))))))wceq cedring_rN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . ctp (cop (cfv cnx cbs) (cfv (cv x2) (cfv (cv x1) ctendo))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cmpt (λ x5 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x5 . ccom (cfv (cv x5) (cv x3)) (cfv (cv x5) (cv x4)))))) (cop (cfv cnx cmulr) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . ccom (cv x4) (cv x3)))))))wceq cedring (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . ctp (cop (cfv cnx cbs) (cfv (cv x2) (cfv (cv x1) ctendo))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cmpt (λ x5 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x5 . ccom (cfv (cv x5) (cv x3)) (cfv (cv x5) (cv x4)))))) (cop (cfv cnx cmulr) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . ccom (cv x3) (cv x4)))))))wceq cdveca (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cun (ctp (cop (cfv cnx cbs) (cfv (cv x2) (cfv (cv x1) cltrn))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . ccom (cv x3) (cv x4)))) (cop (cfv cnx csca) (cfv (cv x2) (cfv (cv x1) cedring)))) (csn (cop (cfv cnx cvsca) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . cfv (cv x4) (cv x3))))))))wceq cdia (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . crab (λ x4 . wbr (cv x4) (cv x2) (cfv (cv x1) cple)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . crab (λ x4 . wbr (cfv (cv x4) (cfv (cv x2) (cfv (cv x1) ctrl))) (cv x3) (cfv (cv x1) cple)) (λ x4 . cfv (cv x2) (cfv (cv x1) cltrn))))))wceq cdvh (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cun (ctp (cop (cfv cnx cbs) (cxp (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) ctendo)))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cxp (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) ctendo))) (λ x3 x4 . cxp (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) ctendo))) (λ x3 x4 . cop (ccom (cfv (cv x3) c1st) (cfv (cv x4) c1st)) (cmpt (λ x5 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x5 . ccom (cfv (cv x5) (cfv (cv x3) c2nd)) (cfv (cv x5) (cfv (cv x4) c2nd))))))) (cop (cfv cnx csca) (cfv (cv x2) (cfv (cv x1) cedring)))) (csn (cop (cfv cnx cvsca) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cxp (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) ctendo))) (λ x3 x4 . cop (cfv (cfv (cv x4) c1st) (cv x3)) (ccom (cv x3) (cfv (cv x4) c2nd)))))))))x0)x0
type
prop
theory
SetMM
name
df_polarityN__df_psubclN__df_lhyp__df_laut__df_watsN__df_pautN__df_ldil__df_ltrn__df_dilN__df_trnN__df_trl__df_tgrp__df_tendo__df_edring_rN__df_edring__df_dveca__df_disoa__df_dvech
proof
PUV1k..
Megalodon
-
proofgold address
TMcqa..
creator
36224 PrCmT../156f8..
owner
36224 PrCmT../156f8..
term root
5367c..