Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
clvec
(
crab
(
λ x1 .
wcel
(
cfv
(
cv
x1
)
csca
)
cdr
)
(
λ x1 .
clmod
)
)
⟶
wceq
csra
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cpw
(
cfv
(
cv
x1
)
cbs
)
)
(
λ x2 .
co
(
co
(
co
(
cv
x1
)
(
cop
(
cfv
cnx
csca
)
(
co
(
cv
x1
)
(
cv
x2
)
cress
)
)
csts
)
(
cop
(
cfv
cnx
cvsca
)
(
cfv
(
cv
x1
)
cmulr
)
)
csts
)
(
cop
(
cfv
cnx
cip
)
(
cfv
(
cv
x1
)
cmulr
)
)
csts
)
)
)
⟶
wceq
crglmod
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cfv
(
cfv
(
cv
x1
)
cbs
)
(
cfv
(
cv
x1
)
csra
)
)
)
⟶
wceq
clidl
(
ccom
clss
crglmod
)
⟶
wceq
crsp
(
ccom
clspn
crglmod
)
⟶
wceq
c2idl
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cin
(
cfv
(
cv
x1
)
clidl
)
(
cfv
(
cfv
(
cv
x1
)
coppr
)
clidl
)
)
)
⟶
wceq
clpidl
(
cmpt
(
λ x1 .
crg
)
(
λ x1 .
ciun
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 .
csn
(
cfv
(
csn
(
cv
x2
)
)
(
cfv
(
cv
x1
)
crsp
)
)
)
)
)
⟶
wceq
clpir
(
crab
(
λ x1 .
wceq
(
cfv
(
cv
x1
)
clidl
)
(
cfv
(
cv
x1
)
clpidl
)
)
(
λ x1 .
crg
)
)
⟶
wceq
cnzr
(
crab
(
λ x1 .
wne
(
cfv
(
cv
x1
)
cur
)
(
cfv
(
cv
x1
)
c0g
)
)
(
λ x1 .
crg
)
)
⟶
wceq
crlreg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wral
(
λ x3 .
wceq
(
co
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cmulr
)
)
(
cfv
(
cv
x1
)
c0g
)
⟶
wceq
(
cv
x3
)
(
cfv
(
cv
x1
)
c0g
)
)
(
λ x3 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
)
⟶
wceq
cdomn
(
crab
(
λ x1 .
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wceq
(
co
(
cv
x4
)
(
cv
x5
)
(
cfv
(
cv
x1
)
cmulr
)
)
(
cv
x3
)
⟶
wo
(
wceq
(
cv
x4
)
(
cv
x3
)
)
(
wceq
(
cv
x5
)
(
cv
x3
)
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cv
x2
)
)
(
cfv
(
cv
x1
)
c0g
)
)
(
cfv
(
cv
x1
)
cbs
)
)
(
λ x1 .
cnzr
)
)
⟶
wceq
cidom
(
cin
ccrg
cdomn
)
⟶
wceq
cpid
(
cin
cidom
clpir
)
⟶
wceq
casa
(
crab
(
λ x1 .
wsbc
(
λ x2 .
wa
(
wcel
(
cv
x2
)
ccrg
)
(
wral
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wsbc
(
λ x6 .
wsbc
(
λ x7 .
wa
(
wceq
(
co
(
co
(
cv
x3
)
(
cv
x4
)
(
cv
x6
)
)
(
cv
x5
)
(
cv
x7
)
)
(
co
(
cv
x3
)
(
co
(
cv
x4
)
(
cv
x5
)
(
cv
x7
)
)
(
cv
x6
)
)
)
(
wceq
(
co
(
cv
x4
)
(
co
(
cv
x3
)
(
cv
x5
)
(
cv
x6
)
)
(
cv
x7
)
)
(
co
(
cv
x3
)
(
co
(
cv
x4
)
(
cv
x5
)
(
cv
x7
)
)
(
cv
x6
)
)
)
)
(
cfv
(
cv
x1
)
cmulr
)
)
(
cfv
(
cv
x1
)
cvsca
)
)
(
λ x5 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x3 .
cfv
(
cv
x2
)
cbs
)
)
)
(
cfv
(
cv
x1
)
csca
)
)
(
λ x1 .
cin
clmod
crg
)
)
⟶
wceq
casp
(
cmpt
(
λ x1 .
casa
)
(
λ x1 .
cmpt
(
λ x2 .
cpw
(
cfv
(
cv
x1
)
cbs
)
)
(
λ x2 .
cint
(
crab
(
λ x3 .
wss
(
cv
x2
)
(
cv
x3
)
)
(
λ x3 .
cin
(
cfv
(
cv
x1
)
csubrg
)
(
cfv
(
cv
x1
)
clss
)
)
)
)
)
)
⟶
wceq
cascl
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cfv
(
cv
x1
)
csca
)
cbs
)
(
λ x2 .
co
(
cv
x2
)
(
cfv
(
cv
x1
)
cur
)
(
cfv
(
cv
x1
)
cvsca
)
)
)
)
⟶
wceq
cmps
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
csb
(
crab
(
λ x3 .
wcel
(
cima
(
ccnv
(
cv
x3
)
)
cn
)
cfn
)
(
λ x3 .
co
cn0
(
cv
x1
)
cmap
)
)
(
λ x3 .
csb
(
co
(
cfv
(
cv
x2
)
cbs
)
(
cv
x3
)
cmap
)
(
λ x4 .
cun
(
ctp
(
cop
(
cfv
cnx
cbs
)
(
cv
x4
)
)
(
cop
(
cfv
cnx
cplusg
)
(
cres
(
cof
(
cfv
(
cv
x2
)
cplusg
)
)
(
cxp
(
cv
x4
)
(
cv
x4
)
)
)
)
(
cop
(
cfv
cnx
cmulr
)
(
cmpt2
(
λ x5 x6 .
cv
x4
)
(
λ x5 x6 .
cv
x4
)
(
λ x5 x6 .
cmpt
(
λ x7 .
cv
x3
)
(
λ x7 .
co
(
cv
x2
)
(
cmpt
(
λ x8 .
crab
(
λ x9 .
wbr
(
cv
x9
)
(
cv
x7
)
(
cofr
cle
)
)
(
λ x9 .
cv
x3
)
)
(
λ x8 .
co
(
cfv
(
cv
x8
)
(
cv
x5
)
)
(
cfv
(
co
(
cv
x7
)
(
cv
x8
)
(
cof
cmin
)
)
(
cv
x6
)
)
(
cfv
(
cv
x2
)
cmulr
)
)
)
cgsu
)
)
)
)
)
(
ctp
(
cop
(
cfv
cnx
csca
)
(
cv
x2
)
)
(
cop
(
cfv
cnx
cvsca
)
(
cmpt2
(
λ x5 x6 .
cfv
(
cv
x2
)
cbs
)
(
λ x5 x6 .
cv
x4
)
(
λ x5 x6 .
co
(
cxp
(
cv
x3
)
(
csn
(
cv
x5
)
)
)
(
cv
x6
)
(
cof
(
cfv
(
cv
x2
)
cmulr
)
)
)
)
)
(
cop
(
cfv
cnx
cts
)
(
cfv
(
cxp
(
cv
x3
)
(
csn
(
cfv
(
cv
x2
)
ctopn
)
)
)
cpt
)
)
)
)
)
)
)
⟶
wceq
cmvr
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cv
x1
)
(
λ x3 .
cmpt
(
λ x4 .
crab
(
λ x5 .
wcel
(
cima
(
ccnv
(
cv
x5
)
)
cn
)
cfn
)
(
λ x5 .
co
cn0
(
cv
x1
)
cmap
)
)
(
λ x4 .
cif
(
wceq
(
cv
x4
)
(
cmpt
(
λ x5 .
cv
x1
)
(
λ x5 .
cif
(
wceq
(
cv
x5
)
(
cv
x3
)
)
c1
cc0
)
)
)
(
cfv
(
cv
x2
)
cur
)
(
cfv
(
cv
x2
)
c0g
)
)
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_lvec__df_sra__df_rgmod__df_lidl__df_rsp__df_2idl__df_lpidl__df_lpir__df_nzr__df_rlreg__df_domn__df_idom__df_pid__df_assa__df_asp__df_ascl__df_psr__df_mvr
proof
PUV1k..
Megalodon
-
proofgold address
TMPD4..
creator
36224
PrCmT..
/
74c62..
owner
36224
PrCmT..
/
74c62..
term root
b7d9f..