Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
cuhgr
(
cab
(
λ x1 .
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wf
(
cdm
(
cv
x3
)
)
(
cdif
(
cpw
(
cv
x2
)
)
(
csn
c0
)
)
(
cv
x3
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
(
cfv
(
cv
x1
)
cvtx
)
)
)
⟶
wceq
cushgr
(
cab
(
λ x1 .
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wf1
(
cdm
(
cv
x3
)
)
(
cdif
(
cpw
(
cv
x2
)
)
(
csn
c0
)
)
(
cv
x3
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
(
cfv
(
cv
x1
)
cvtx
)
)
)
⟶
wceq
cupgr
(
cab
(
λ x1 .
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wf
(
cdm
(
cv
x3
)
)
(
crab
(
λ x4 .
wbr
(
cfv
(
cv
x4
)
chash
)
c2
cle
)
(
λ x4 .
cdif
(
cpw
(
cv
x2
)
)
(
csn
c0
)
)
)
(
cv
x3
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
(
cfv
(
cv
x1
)
cvtx
)
)
)
⟶
wceq
cumgr
(
cab
(
λ x1 .
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wf
(
cdm
(
cv
x3
)
)
(
crab
(
λ x4 .
wceq
(
cfv
(
cv
x4
)
chash
)
c2
)
(
λ x4 .
cdif
(
cpw
(
cv
x2
)
)
(
csn
c0
)
)
)
(
cv
x3
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
(
cfv
(
cv
x1
)
cvtx
)
)
)
⟶
wceq
cuspgr
(
cab
(
λ x1 .
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wf1
(
cdm
(
cv
x3
)
)
(
crab
(
λ x4 .
wbr
(
cfv
(
cv
x4
)
chash
)
c2
cle
)
(
λ x4 .
cdif
(
cpw
(
cv
x2
)
)
(
csn
c0
)
)
)
(
cv
x3
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
(
cfv
(
cv
x1
)
cvtx
)
)
)
⟶
wceq
cusgr
(
cab
(
λ x1 .
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wf1
(
cdm
(
cv
x3
)
)
(
crab
(
λ x4 .
wceq
(
cfv
(
cv
x4
)
chash
)
c2
)
(
λ x4 .
cdif
(
cpw
(
cv
x2
)
)
(
csn
c0
)
)
)
(
cv
x3
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
(
cfv
(
cv
x1
)
cvtx
)
)
)
⟶
wceq
csubgr
(
copab
(
λ x1 x2 .
w3a
(
wss
(
cfv
(
cv
x1
)
cvtx
)
(
cfv
(
cv
x2
)
cvtx
)
)
(
wceq
(
cfv
(
cv
x1
)
ciedg
)
(
cres
(
cfv
(
cv
x2
)
ciedg
)
(
cdm
(
cfv
(
cv
x1
)
ciedg
)
)
)
)
(
wss
(
cfv
(
cv
x1
)
cedg
)
(
cpw
(
cfv
(
cv
x1
)
cvtx
)
)
)
)
)
⟶
wceq
cfusgr
(
crab
(
λ x1 .
wcel
(
cfv
(
cv
x1
)
cvtx
)
cfn
)
(
λ x1 .
cusgr
)
)
⟶
wceq
cnbgr
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cfv
(
cv
x1
)
cvtx
)
(
λ x1 x2 .
crab
(
λ x3 .
wrex
(
λ x4 .
wss
(
cpr
(
cv
x2
)
(
cv
x3
)
)
(
cv
x4
)
)
(
λ x4 .
cfv
(
cv
x1
)
cedg
)
)
(
λ x3 .
cdif
(
cfv
(
cv
x1
)
cvtx
)
(
csn
(
cv
x2
)
)
)
)
)
⟶
wceq
cuvtx
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wral
(
λ x3 .
wcel
(
cv
x3
)
(
co
(
cv
x1
)
(
cv
x2
)
cnbgr
)
)
(
λ x3 .
cdif
(
cfv
(
cv
x1
)
cvtx
)
(
csn
(
cv
x2
)
)
)
)
(
λ x2 .
cfv
(
cv
x1
)
cvtx
)
)
)
⟶
wceq
ccplgr
(
cab
(
λ x1 .
wceq
(
cfv
(
cv
x1
)
cuvtx
)
(
cfv
(
cv
x1
)
cvtx
)
)
)
⟶
wceq
ccusgr
(
cin
cusgr
ccplgr
)
⟶
wceq
cvtxdg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
csb
(
cfv
(
cv
x1
)
cvtx
)
(
λ x2 .
csb
(
cfv
(
cv
x1
)
ciedg
)
(
λ x3 .
cmpt
(
λ x4 .
cv
x2
)
(
λ x4 .
co
(
cfv
(
crab
(
λ x5 .
wcel
(
cv
x4
)
(
cfv
(
cv
x5
)
(
cv
x3
)
)
)
(
λ x5 .
cdm
(
cv
x3
)
)
)
chash
)
(
cfv
(
crab
(
λ x5 .
wceq
(
cfv
(
cv
x5
)
(
cv
x3
)
)
(
csn
(
cv
x4
)
)
)
(
λ x5 .
cdm
(
cv
x3
)
)
)
chash
)
cxad
)
)
)
)
)
⟶
wceq
crgr
(
copab
(
λ x1 x2 .
wa
(
wcel
(
cv
x2
)
cxnn0
)
(
wral
(
λ x3 .
wceq
(
cfv
(
cv
x3
)
(
cfv
(
cv
x1
)
cvtxdg
)
)
(
cv
x2
)
)
(
λ x3 .
cfv
(
cv
x1
)
cvtx
)
)
)
)
⟶
wceq
crusgr
(
copab
(
λ x1 x2 .
wa
(
wcel
(
cv
x1
)
cusgr
)
(
wbr
(
cv
x1
)
(
cv
x2
)
crgr
)
)
)
⟶
wceq
cewlks
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cxnn0
)
(
λ x1 x2 .
cab
(
λ x3 .
wsbc
(
λ x4 .
wa
(
wcel
(
cv
x3
)
(
cword
(
cdm
(
cv
x4
)
)
)
)
(
wral
(
λ x5 .
wbr
(
cv
x2
)
(
cfv
(
cin
(
cfv
(
cfv
(
co
(
cv
x5
)
c1
cmin
)
(
cv
x3
)
)
(
cv
x4
)
)
(
cfv
(
cfv
(
cv
x5
)
(
cv
x3
)
)
(
cv
x4
)
)
)
chash
)
cle
)
(
λ x5 .
co
c1
(
cfv
(
cv
x3
)
chash
)
cfzo
)
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
)
)
⟶
wceq
cwlks
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
w3a
(
wcel
(
cv
x2
)
(
cword
(
cdm
(
cfv
(
cv
x1
)
ciedg
)
)
)
)
(
wf
(
co
cc0
(
cfv
(
cv
x2
)
chash
)
cfz
)
(
cfv
(
cv
x1
)
cvtx
)
(
cv
x3
)
)
(
wral
(
λ x4 .
wif
(
wceq
(
cfv
(
cv
x4
)
(
cv
x3
)
)
(
cfv
(
co
(
cv
x4
)
c1
caddc
)
(
cv
x3
)
)
)
(
wceq
(
cfv
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
(
csn
(
cfv
(
cv
x4
)
(
cv
x3
)
)
)
)
(
wss
(
cpr
(
cfv
(
cv
x4
)
(
cv
x3
)
)
(
cfv
(
co
(
cv
x4
)
c1
caddc
)
(
cv
x3
)
)
)
(
cfv
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
)
)
(
λ x4 .
co
cc0
(
cfv
(
cv
x2
)
chash
)
cfzo
)
)
)
)
)
⟶
wceq
cwlkson
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cvtx
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cvtx
)
(
λ x2 x3 .
copab
(
λ x4 x5 .
w3a
(
wbr
(
cv
x4
)
(
cv
x5
)
(
cfv
(
cv
x1
)
cwlks
)
)
(
wceq
(
cfv
cc0
(
cv
x5
)
)
(
cv
x2
)
)
(
wceq
(
cfv
(
cfv
(
cv
x4
)
chash
)
(
cv
x5
)
)
(
cv
x3
)
)
)
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_uhgr__df_ushgr__df_upgr__df_umgr__df_uspgr__df_usgr__df_subgr__df_fusgr__df_nbgr__df_uvtx__df_cplgr__df_cusgr__df_vtxdg__df_rgr__df_rusgr__df_ewlks__df_wlks__df_wlkson
proof
PUV1k..
Megalodon
-
proofgold address
TMM8F..
creator
36224
PrCmT..
/
0c86e..
owner
36224
PrCmT..
/
0c86e..
term root
0f971..