Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
(
∀ x1 x2 x3 :
ι →
ι → ο
.
∀ x4 .
wceq
(
cdit
x1
x2
x3
)
(
cif
(
wbr
(
x1
x4
)
(
x2
x4
)
cle
)
(
citg
(
λ x5 .
co
(
x1
x5
)
(
x2
x5
)
cioo
)
x3
)
(
cneg
(
citg
(
λ x5 .
co
(
x2
x5
)
(
x1
x5
)
cioo
)
x3
)
)
)
)
⟶
wceq
climc
(
cmpt2
(
λ x1 x2 .
co
cc
cc
cpm
)
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cab
(
λ x3 .
wsbc
(
λ x4 .
wcel
(
cmpt
(
λ x5 .
cun
(
cdm
(
cv
x1
)
)
(
csn
(
cv
x2
)
)
)
(
λ x5 .
cif
(
wceq
(
cv
x5
)
(
cv
x2
)
)
(
cv
x3
)
(
cfv
(
cv
x5
)
(
cv
x1
)
)
)
)
(
cfv
(
cv
x2
)
(
co
(
co
(
cv
x4
)
(
cun
(
cdm
(
cv
x1
)
)
(
csn
(
cv
x2
)
)
)
crest
)
(
cv
x4
)
ccnp
)
)
)
(
cfv
ccnfld
ctopn
)
)
)
)
⟶
wceq
cdv
(
cmpt2
(
λ x1 x2 .
cpw
cc
)
(
λ x1 x2 .
co
cc
(
cv
x1
)
cpm
)
(
λ x1 x2 .
ciun
(
λ x3 .
cfv
(
cdm
(
cv
x2
)
)
(
cfv
(
co
(
cfv
ccnfld
ctopn
)
(
cv
x1
)
crest
)
cnt
)
)
(
λ x3 .
cxp
(
csn
(
cv
x3
)
)
(
co
(
cmpt
(
λ x4 .
cdif
(
cdm
(
cv
x2
)
)
(
csn
(
cv
x3
)
)
)
(
λ x4 .
co
(
co
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
cmin
)
(
co
(
cv
x4
)
(
cv
x3
)
cmin
)
cdiv
)
)
(
cv
x3
)
climc
)
)
)
)
⟶
wceq
cdvn
(
cmpt2
(
λ x1 x2 .
cpw
cc
)
(
λ x1 x2 .
co
cc
(
cv
x1
)
cpm
)
(
λ x1 x2 .
cseq
(
ccom
(
cmpt
(
λ x3 .
cvv
)
(
λ x3 .
co
(
cv
x1
)
(
cv
x3
)
cdv
)
)
c1st
)
(
cxp
cn0
(
csn
(
cv
x2
)
)
)
cc0
)
)
⟶
wceq
ccpn
(
cmpt
(
λ x1 .
cpw
cc
)
(
λ x1 .
cmpt
(
λ x2 .
cn0
)
(
λ x2 .
crab
(
λ x3 .
wcel
(
cfv
(
cv
x2
)
(
co
(
cv
x1
)
(
cv
x3
)
cdvn
)
)
(
co
(
cdm
(
cv
x3
)
)
cc
ccncf
)
)
(
λ x3 .
co
cc
(
cv
x1
)
cpm
)
)
)
)
⟶
wceq
cmdg
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cmpl
)
cbs
)
(
λ x3 .
csup
(
crn
(
cmpt
(
λ x4 .
co
(
cv
x3
)
(
cfv
(
cv
x2
)
c0g
)
csupp
)
(
λ x4 .
co
ccnfld
(
cv
x4
)
cgsu
)
)
)
cxr
clt
)
)
)
⟶
wceq
cdg1
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
co
c1o
(
cv
x1
)
cmdg
)
)
⟶
wceq
cmn1
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wa
(
wne
(
cv
x2
)
(
cfv
(
cfv
(
cv
x1
)
cpl1
)
c0g
)
)
(
wceq
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdg1
)
)
(
cfv
(
cv
x2
)
cco1
)
)
(
cfv
(
cv
x1
)
cur
)
)
)
(
λ x2 .
cfv
(
cfv
(
cv
x1
)
cpl1
)
cbs
)
)
)
⟶
wceq
cuc1p
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wa
(
wne
(
cv
x2
)
(
cfv
(
cfv
(
cv
x1
)
cpl1
)
c0g
)
)
(
wcel
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdg1
)
)
(
cfv
(
cv
x2
)
cco1
)
)
(
cfv
(
cv
x1
)
cui
)
)
)
(
λ x2 .
cfv
(
cfv
(
cv
x1
)
cpl1
)
cbs
)
)
)
⟶
wceq
cq1p
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
csb
(
cfv
(
cv
x1
)
cpl1
)
(
λ x2 .
csb
(
cfv
(
cv
x2
)
cbs
)
(
λ x3 .
cmpt2
(
λ x4 x5 .
cv
x3
)
(
λ x4 x5 .
cv
x3
)
(
λ x4 x5 .
crio
(
λ x6 .
wbr
(
cfv
(
co
(
cv
x4
)
(
co
(
cv
x6
)
(
cv
x5
)
(
cfv
(
cv
x2
)
cmulr
)
)
(
cfv
(
cv
x2
)
csg
)
)
(
cfv
(
cv
x1
)
cdg1
)
)
(
cfv
(
cv
x5
)
(
cfv
(
cv
x1
)
cdg1
)
)
clt
)
(
λ x6 .
cv
x3
)
)
)
)
)
)
⟶
wceq
cr1p
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
csb
(
cfv
(
cfv
(
cv
x1
)
cpl1
)
cbs
)
(
λ x2 .
cmpt2
(
λ x3 x4 .
cv
x2
)
(
λ x3 x4 .
cv
x2
)
(
λ x3 x4 .
co
(
cv
x3
)
(
co
(
co
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cq1p
)
)
(
cv
x4
)
(
cfv
(
cfv
(
cv
x1
)
cpl1
)
cmulr
)
)
(
cfv
(
cfv
(
cv
x1
)
cpl1
)
csg
)
)
)
)
)
⟶
wceq
cig1p
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cfv
(
cv
x1
)
cpl1
)
clidl
)
(
λ x2 .
cif
(
wceq
(
cv
x2
)
(
csn
(
cfv
(
cfv
(
cv
x1
)
cpl1
)
c0g
)
)
)
(
cfv
(
cfv
(
cv
x1
)
cpl1
)
c0g
)
(
crio
(
λ x3 .
wceq
(
cfv
(
cv
x3
)
(
cfv
(
cv
x1
)
cdg1
)
)
(
cinf
(
cima
(
cfv
(
cv
x1
)
cdg1
)
(
cdif
(
cv
x2
)
(
csn
(
cfv
(
cfv
(
cv
x1
)
cpl1
)
c0g
)
)
)
)
cr
clt
)
)
(
λ x3 .
cin
(
cv
x2
)
(
cfv
(
cv
x1
)
cmn1
)
)
)
)
)
)
⟶
wceq
cply
(
cmpt
(
λ x1 .
cpw
cc
)
(
λ x1 .
cab
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wceq
(
cv
x2
)
(
cmpt
(
λ x5 .
cc
)
(
λ x5 .
csu
(
co
cc0
(
cv
x3
)
cfz
)
(
λ x6 .
co
(
cfv
(
cv
x6
)
(
cv
x4
)
)
(
co
(
cv
x5
)
(
cv
x6
)
cexp
)
cmul
)
)
)
)
(
λ x4 .
co
(
cun
(
cv
x1
)
(
csn
cc0
)
)
cn0
cmap
)
)
(
λ x3 .
cn0
)
)
)
)
⟶
wceq
cidp
(
cres
cid
cc
)
⟶
wceq
ccoe
(
cmpt
(
λ x1 .
cfv
cc
cply
)
(
λ x1 .
crio
(
λ x2 .
wrex
(
λ x3 .
wa
(
wceq
(
cima
(
cv
x2
)
(
cfv
(
co
(
cv
x3
)
c1
caddc
)
cuz
)
)
(
csn
cc0
)
)
(
wceq
(
cv
x1
)
(
cmpt
(
λ x4 .
cc
)
(
λ x4 .
csu
(
co
cc0
(
cv
x3
)
cfz
)
(
λ x5 .
co
(
cfv
(
cv
x5
)
(
cv
x2
)
)
(
co
(
cv
x4
)
(
cv
x5
)
cexp
)
cmul
)
)
)
)
)
(
λ x3 .
cn0
)
)
(
λ x2 .
co
cc
cn0
cmap
)
)
)
⟶
wceq
cdgr
(
cmpt
(
λ x1 .
cfv
cc
cply
)
(
λ x1 .
csup
(
cima
(
ccnv
(
cfv
(
cv
x1
)
ccoe
)
)
(
cdif
cc
(
csn
cc0
)
)
)
cn0
clt
)
)
⟶
wceq
cquot
(
cmpt2
(
λ x1 x2 .
cfv
cc
cply
)
(
λ x1 x2 .
cdif
(
cfv
cc
cply
)
(
csn
c0p
)
)
(
λ x1 x2 .
crio
(
λ x3 .
wsbc
(
λ x4 .
wo
(
wceq
(
cv
x4
)
c0p
)
(
wbr
(
cfv
(
cv
x4
)
cdgr
)
(
cfv
(
cv
x2
)
cdgr
)
clt
)
)
(
co
(
cv
x1
)
(
co
(
cv
x2
)
(
cv
x3
)
(
cof
cmul
)
)
(
cof
cmin
)
)
)
(
λ x3 .
cfv
cc
cply
)
)
)
⟶
wceq
caa
(
ciun
(
λ x1 .
cdif
(
cfv
cz
cply
)
(
csn
c0p
)
)
(
λ x1 .
cima
(
ccnv
(
cv
x1
)
)
(
csn
cc0
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_ditg__df_limc__df_dv__df_dvn__df_cpn__df_mdeg__df_deg1__df_mon1__df_uc1p__df_q1p__df_r1p__df_ig1p__df_ply__df_idp__df_coe__df_dgr__df_quot__df_aa
proof
PUV1k..
Megalodon
-
proofgold address
TMVbL..
creator
36224
PrCmT..
/
77173..
owner
36224
PrCmT..
/
77173..
term root
d0b52..