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..