Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
cvrgp
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cv
x1
)
(
λ x2 .
cec
(
cs1
(
cop
(
cv
x2
)
c0
)
)
(
cfv
(
cv
x1
)
cefg
)
)
)
)
⟶
wceq
ccmn
(
crab
(
λ x1 .
wral
(
λ x2 .
wral
(
λ x3 .
wceq
(
co
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cplusg
)
)
(
co
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cplusg
)
)
)
(
λ x3 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x1 .
cmnd
)
)
⟶
wceq
cabl
(
cin
cgrp
ccmn
)
⟶
wceq
ccyg
(
crab
(
λ x1 .
wrex
(
λ x2 .
wceq
(
crn
(
cmpt
(
λ x3 .
cz
)
(
λ x3 .
co
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cmg
)
)
)
)
(
cfv
(
cv
x1
)
cbs
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x1 .
cgrp
)
)
⟶
wceq
cdprd
(
cmpt2
(
λ x1 x2 .
cgrp
)
(
λ x1 x2 .
cab
(
λ x3 .
wa
(
wf
(
cdm
(
cv
x3
)
)
(
cfv
(
cv
x1
)
csubg
)
(
cv
x3
)
)
(
wral
(
λ x4 .
wa
(
wral
(
λ x5 .
wss
(
cfv
(
cv
x4
)
(
cv
x3
)
)
(
cfv
(
cfv
(
cv
x5
)
(
cv
x3
)
)
(
cfv
(
cv
x1
)
ccntz
)
)
)
(
λ x5 .
cdif
(
cdm
(
cv
x3
)
)
(
csn
(
cv
x4
)
)
)
)
(
wceq
(
cin
(
cfv
(
cv
x4
)
(
cv
x3
)
)
(
cfv
(
cuni
(
cima
(
cv
x3
)
(
cdif
(
cdm
(
cv
x3
)
)
(
csn
(
cv
x4
)
)
)
)
)
(
cfv
(
cfv
(
cv
x1
)
csubg
)
cmrc
)
)
)
(
csn
(
cfv
(
cv
x1
)
c0g
)
)
)
)
(
λ x4 .
cdm
(
cv
x3
)
)
)
)
)
(
λ x1 x2 .
crn
(
cmpt
(
λ x3 .
crab
(
λ x4 .
wbr
(
cv
x4
)
(
cfv
(
cv
x1
)
c0g
)
cfsupp
)
(
λ x4 .
cixp
(
λ x5 .
cdm
(
cv
x2
)
)
(
λ x5 .
cfv
(
cv
x5
)
(
cv
x2
)
)
)
)
(
λ x3 .
co
(
cv
x1
)
(
cv
x3
)
cgsu
)
)
)
)
⟶
wceq
cdpj
(
cmpt2
(
λ x1 x2 .
cgrp
)
(
λ x1 x2 .
cima
(
cdm
cdprd
)
(
csn
(
cv
x1
)
)
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cdm
(
cv
x2
)
)
(
λ x3 .
co
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
co
(
cv
x1
)
(
cres
(
cv
x2
)
(
cdif
(
cdm
(
cv
x2
)
)
(
csn
(
cv
x3
)
)
)
)
cdprd
)
(
cfv
(
cv
x1
)
cpj1
)
)
)
)
⟶
wceq
cmgp
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
co
(
cv
x1
)
(
cop
(
cfv
cnx
cplusg
)
(
cfv
(
cv
x1
)
cmulr
)
)
csts
)
)
⟶
wceq
cur
(
ccom
c0g
cmgp
)
⟶
wceq
csrg
(
crab
(
λ x1 .
wa
(
wcel
(
cfv
(
cv
x1
)
cmgp
)
cmnd
)
(
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wsbc
(
λ x4 .
wsbc
(
λ x5 .
wral
(
λ x6 .
wa
(
wral
(
λ x7 .
wral
(
λ x8 .
wa
(
wceq
(
co
(
cv
x6
)
(
co
(
cv
x7
)
(
cv
x8
)
(
cv
x3
)
)
(
cv
x4
)
)
(
co
(
co
(
cv
x6
)
(
cv
x7
)
(
cv
x4
)
)
(
co
(
cv
x6
)
(
cv
x8
)
(
cv
x4
)
)
(
cv
x3
)
)
)
(
wceq
(
co
(
co
(
cv
x6
)
(
cv
x7
)
(
cv
x3
)
)
(
cv
x8
)
(
cv
x4
)
)
(
co
(
co
(
cv
x6
)
(
cv
x8
)
(
cv
x4
)
)
(
co
(
cv
x7
)
(
cv
x8
)
(
cv
x4
)
)
(
cv
x3
)
)
)
)
(
λ x8 .
cv
x2
)
)
(
λ x7 .
cv
x2
)
)
(
wa
(
wceq
(
co
(
cv
x5
)
(
cv
x6
)
(
cv
x4
)
)
(
cv
x5
)
)
(
wceq
(
co
(
cv
x6
)
(
cv
x5
)
(
cv
x4
)
)
(
cv
x5
)
)
)
)
(
λ x6 .
cv
x2
)
)
(
cfv
(
cv
x1
)
c0g
)
)
(
cfv
(
cv
x1
)
cmulr
)
)
(
cfv
(
cv
x1
)
cplusg
)
)
(
cfv
(
cv
x1
)
cbs
)
)
)
(
λ x1 .
ccmn
)
)
⟶
wceq
crg
(
crab
(
λ x1 .
wa
(
wcel
(
cfv
(
cv
x1
)
cmgp
)
cmnd
)
(
wsbc
(
λ x2 .
wsbc
(
λ x3 .
wsbc
(
λ x4 .
wral
(
λ x5 .
wral
(
λ x6 .
wral
(
λ x7 .
wa
(
wceq
(
co
(
cv
x5
)
(
co
(
cv
x6
)
(
cv
x7
)
(
cv
x3
)
)
(
cv
x4
)
)
(
co
(
co
(
cv
x5
)
(
cv
x6
)
(
cv
x4
)
)
(
co
(
cv
x5
)
(
cv
x7
)
(
cv
x4
)
)
(
cv
x3
)
)
)
(
wceq
(
co
(
co
(
cv
x5
)
(
cv
x6
)
(
cv
x3
)
)
(
cv
x7
)
(
cv
x4
)
)
(
co
(
co
(
cv
x5
)
(
cv
x7
)
(
cv
x4
)
)
(
co
(
cv
x6
)
(
cv
x7
)
(
cv
x4
)
)
(
cv
x3
)
)
)
)
(
λ x7 .
cv
x2
)
)
(
λ x6 .
cv
x2
)
)
(
λ x5 .
cv
x2
)
)
(
cfv
(
cv
x1
)
cmulr
)
)
(
cfv
(
cv
x1
)
cplusg
)
)
(
cfv
(
cv
x1
)
cbs
)
)
)
(
λ x1 .
cgrp
)
)
⟶
wceq
ccrg
(
crab
(
λ x1 .
wcel
(
cfv
(
cv
x1
)
cmgp
)
ccmn
)
(
λ x1 .
crg
)
)
⟶
wceq
coppr
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
co
(
cv
x1
)
(
cop
(
cfv
cnx
cmulr
)
(
ctpos
(
cfv
(
cv
x1
)
cmulr
)
)
)
csts
)
)
⟶
wceq
cdsr
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wa
(
wcel
(
cv
x2
)
(
cfv
(
cv
x1
)
cbs
)
)
(
wrex
(
λ x4 .
wceq
(
co
(
cv
x4
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cmulr
)
)
(
cv
x3
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
)
⟶
wceq
cui
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cima
(
ccnv
(
cin
(
cfv
(
cv
x1
)
cdsr
)
(
cfv
(
cfv
(
cv
x1
)
coppr
)
cdsr
)
)
)
(
csn
(
cfv
(
cv
x1
)
cur
)
)
)
)
⟶
wceq
cir
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
csb
(
cdif
(
cfv
(
cv
x1
)
cbs
)
(
cfv
(
cv
x1
)
cui
)
)
(
λ x2 .
crab
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wne
(
co
(
cv
x4
)
(
cv
x5
)
(
cfv
(
cv
x1
)
cmulr
)
)
(
cv
x3
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cv
x2
)
)
(
λ x3 .
cv
x2
)
)
)
)
⟶
wceq
cinvr
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cfv
(
co
(
cfv
(
cv
x1
)
cmgp
)
(
cfv
(
cv
x1
)
cui
)
cress
)
cminusg
)
)
⟶
wceq
cdvr
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cui
)
(
λ x2 x3 .
co
(
cv
x2
)
(
cfv
(
cv
x3
)
(
cfv
(
cv
x1
)
cinvr
)
)
(
cfv
(
cv
x1
)
cmulr
)
)
)
)
⟶
wceq
crpm
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
csb
(
cfv
(
cv
x1
)
cbs
)
(
λ x2 .
crab
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wsbc
(
λ x6 .
wbr
(
cv
x3
)
(
co
(
cv
x4
)
(
cv
x5
)
(
cfv
(
cv
x1
)
cmulr
)
)
(
cv
x6
)
⟶
wo
(
wbr
(
cv
x3
)
(
cv
x4
)
(
cv
x6
)
)
(
wbr
(
cv
x3
)
(
cv
x5
)
(
cv
x6
)
)
)
(
cfv
(
cv
x1
)
cdsr
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cv
x2
)
)
(
λ x3 .
cdif
(
cv
x2
)
(
cun
(
cfv
(
cv
x1
)
cui
)
(
csn
(
cfv
(
cv
x1
)
c0g
)
)
)
)
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_vrgp__df_cmn__df_abl__df_cyg__df_dprd__df_dpj__df_mgp__df_ur__df_srg__df_ring__df_cring__df_oppr__df_dvdsr__df_unit__df_irred__df_invr__df_dvr__df_rprm
proof
PUV1k..
Megalodon
-
proofgold address
TMJQk..
creator
36224
PrCmT..
/
dda2d..
owner
36224
PrCmT..
/
dda2d..
term root
b1bdc..