Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ο . (wceq cops (crab (λ x1 . wa (wa (wcel (cfv (cv x1) cbs) (cdm (cfv (cv x1) club))) (wcel (cfv (cv x1) cbs) (cdm (cfv (cv x1) cglb)))) (wex (λ x2 . wa (wceq (cv x2) (cfv (cv x1) coc)) (wral (λ x3 . wral (λ x4 . w3a (w3a (wcel (cfv (cv x3) (cv x2)) (cfv (cv x1) cbs)) (wceq (cfv (cfv (cv x3) (cv x2)) (cv x2)) (cv x3)) (wbr (cv x3) (cv x4) (cfv (cv x1) cple)wbr (cfv (cv x4) (cv x2)) (cfv (cv x3) (cv x2)) (cfv (cv x1) cple))) (wceq (co (cv x3) (cfv (cv x3) (cv x2)) (cfv (cv x1) cjn)) (cfv (cv x1) cp1)) (wceq (co (cv x3) (cfv (cv x3) (cv x2)) (cfv (cv x1) cmee)) (cfv (cv x1) cp0))) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) cbs))))) (λ x1 . cpo))wceq ccmtN (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . w3a (wcel (cv x2) (cfv (cv x1) cbs)) (wcel (cv x3) (cfv (cv x1) cbs)) (wceq (cv x2) (co (co (cv x2) (cv x3) (cfv (cv x1) cmee)) (co (cv x2) (cfv (cv x3) (cfv (cv x1) coc)) (cfv (cv x1) cmee)) (cfv (cv x1) cjn))))))wceq col (cin clat cops)wceq coml (crab (λ x1 . wral (λ x2 . wral (λ x3 . wbr (cv x2) (cv x3) (cfv (cv x1) cple)wceq (cv x3) (co (cv x2) (co (cv x3) (cfv (cv x2) (cfv (cv x1) coc)) (cfv (cv x1) cmee)) (cfv (cv x1) cjn))) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs)) (λ x1 . col))wceq ccvr (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . w3a (wa (wcel (cv x2) (cfv (cv x1) cbs)) (wcel (cv x3) (cfv (cv x1) cbs))) (wbr (cv x2) (cv x3) (cfv (cv x1) cplt)) (wn (wrex (λ x4 . wa (wbr (cv x2) (cv x4) (cfv (cv x1) cplt)) (wbr (cv x4) (cv x3) (cfv (cv x1) cplt))) (λ x4 . cfv (cv x1) cbs))))))wceq catm (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wbr (cfv (cv x1) cp0) (cv x2) (cfv (cv x1) ccvr)) (λ x2 . cfv (cv x1) cbs)))wceq cal (crab (λ x1 . wa (wcel (cfv (cv x1) cbs) (cdm (cfv (cv x1) cglb))) (wral (λ x2 . wne (cv x2) (cfv (cv x1) cp0)wrex (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) cple)) (λ x3 . cfv (cv x1) catm)) (λ x2 . cfv (cv x1) cbs))) (λ x1 . clat))wceq clc (crab (λ x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wa (wn (wbr (cv x2) (cv x4) (cfv (cv x1) cple))) (wbr (cv x2) (co (cv x4) (cv x3) (cfv (cv x1) cjn)) (cfv (cv x1) cple))wbr (cv x3) (co (cv x4) (cv x2) (cfv (cv x1) cjn)) (cfv (cv x1) cple)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) catm)) (λ x2 . cfv (cv x1) catm)) (λ x1 . cal))wceq chlt (crab (λ x1 . wa (wral (λ x2 . wral (λ x3 . wne (cv x2) (cv x3)wrex (λ x4 . w3a (wne (cv x4) (cv x2)) (wne (cv x4) (cv x3)) (wbr (cv x4) (co (cv x2) (cv x3) (cfv (cv x1) cjn)) (cfv (cv x1) cple))) (λ x4 . cfv (cv x1) catm)) (λ x3 . cfv (cv x1) catm)) (λ x2 . cfv (cv x1) catm)) (wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wa (wa (wbr (cfv (cv x1) cp0) (cv x2) (cfv (cv x1) cplt)) (wbr (cv x2) (cv x3) (cfv (cv x1) cplt))) (wa (wbr (cv x3) (cv x4) (cfv (cv x1) cplt)) (wbr (cv x4) (cfv (cv x1) cp1) (cfv (cv x1) cplt)))) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs))) (λ x1 . cin (cin coml ccla) clc))wceq clln (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wrex (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) ccvr)) (λ x3 . cfv (cv x1) catm)) (λ x2 . cfv (cv x1) cbs)))wceq clpl (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wrex (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) ccvr)) (λ x3 . cfv (cv x1) clln)) (λ x2 . cfv (cv x1) cbs)))wceq clvol (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wrex (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) ccvr)) (λ x3 . cfv (cv x1) clpl)) (λ x2 . cfv (cv x1) cbs)))wceq clines (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wa (wne (cv x3) (cv x4)) (wceq (cv x2) (crab (λ x5 . wbr (cv x5) (co (cv x3) (cv x4) (cfv (cv x1) cjn)) (cfv (cv x1) cple)) (λ x5 . cfv (cv x1) catm)))) (λ x4 . cfv (cv x1) catm)) (λ x3 . cfv (cv x1) catm))))wceq cpointsN (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wrex (λ x3 . wceq (cv x2) (csn (cv x3))) (λ x3 . cfv (cv x1) catm))))wceq cpsubsp (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wa (wss (cv x2) (cfv (cv x1) catm)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wbr (cv x5) (co (cv x3) (cv x4) (cfv (cv x1) cjn)) (cfv (cv x1) cple)wcel (cv x5) (cv x2)) (λ x5 . cfv (cv x1) catm)) (λ x4 . cv x2)) (λ x3 . cv x2)))))wceq cpmap (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . crab (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) cple)) (λ x3 . cfv (cv x1) catm))))wceq cpadd (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cpw (cfv (cv x1) catm)) (λ x2 x3 . cpw (cfv (cv x1) catm)) (λ x2 x3 . cun (cun (cv x2) (cv x3)) (crab (λ x4 . wrex (λ x5 . wrex (λ x6 . wbr (cv x4) (co (cv x5) (cv x6) (cfv (cv x1) cjn)) (cfv (cv x1) cple)) (λ x6 . cv x3)) (λ x5 . cv x2)) (λ x4 . cfv (cv x1) catm)))))wceq cpclN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) catm)) (λ x2 . cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cfv (cv x1) cpsubsp)))))x0)x0
type
prop
theory
SetMM
name
df_oposet__df_cmtN__df_ol__df_oml__df_covers__df_ats__df_atl__df_cvlat__df_hlat__df_llines__df_lplanes__df_lvols__df_lines__df_pointsN__df_psubsp__df_pmap__df_padd__df_pclN
proof
PUV1k..
Megalodon
-
proofgold address
TML28..
creator
36224 PrCmT../cca08..
owner
36224 PrCmT../cca08..
term root
7ba6a..