Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
(
∀ x1 x2 x3 :
ι → ο
.
wceq
(
cstrset
x1
x2
x3
)
(
cun
(
cres
x3
(
cdif
cvv
(
csn
(
cfv
cnx
x1
)
)
)
)
(
csn
(
cop
(
cfv
cnx
x1
)
x2
)
)
)
)
⟶
wceq
cdiag2
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cin
cid
(
cxp
(
cv
x1
)
(
cv
x1
)
)
)
)
⟶
wceq
cinftyexpi
(
cmpt
(
λ x1 .
co
(
cneg
cpi
)
cpi
cioc
)
(
λ x1 .
cop
(
cv
x1
)
cc
)
)
⟶
wceq
cccinfty
(
crn
cinftyexpi
)
⟶
wceq
cccbar
(
cun
cc
cccinfty
)
⟶
wceq
cpinfty
(
cfv
cc0
cinftyexpi
)
⟶
wceq
cminfty
(
cfv
cpi
cinftyexpi
)
⟶
wceq
crrbar
(
cun
cr
(
cpr
cminfty
cpinfty
)
)
⟶
wceq
cinfty
(
cpw
(
cuni
cc
)
)
⟶
wceq
ccchat
(
cun
cc
(
csn
cinfty
)
)
⟶
wceq
crrhat
(
cun
cr
(
csn
cinfty
)
)
⟶
wceq
caddcc
(
cmpt
(
λ x1 .
cun
(
cun
(
cxp
cc
cccbar
)
(
cxp
cccbar
cc
)
)
(
cun
(
cxp
ccchat
ccchat
)
(
cfv
cccinfty
cdiag2
)
)
)
(
λ x1 .
cif
(
wo
(
wceq
(
cfv
(
cv
x1
)
c1st
)
cinfty
)
(
wceq
(
cfv
(
cv
x1
)
c2nd
)
cinfty
)
)
cinfty
(
cif
(
wcel
(
cfv
(
cv
x1
)
c1st
)
cc
)
(
cif
(
wcel
(
cfv
(
cv
x1
)
c2nd
)
cc
)
(
co
(
cfv
(
cv
x1
)
c1st
)
(
cfv
(
cv
x1
)
c2nd
)
caddc
)
(
cfv
(
cv
x1
)
c2nd
)
)
(
cfv
(
cv
x1
)
c1st
)
)
)
)
⟶
wceq
coppcc
(
cmpt
(
λ x1 .
cun
cccbar
ccchat
)
(
λ x1 .
cif
(
wceq
(
cv
x1
)
cinfty
)
cinfty
(
cif
(
wcel
(
cv
x1
)
cc
)
(
cneg
(
cv
x1
)
)
(
cfv
(
cif
(
wbr
cc0
(
cfv
(
cv
x1
)
c1st
)
clt
)
(
co
(
cfv
(
cv
x1
)
c1st
)
cpi
cmin
)
(
co
(
cfv
(
cv
x1
)
c1st
)
cpi
caddc
)
)
cinftyexpi
)
)
)
)
⟶
wceq
cprcpal
(
cmpt
(
λ x1 .
cr
)
(
λ x1 .
co
(
co
(
cv
x1
)
(
co
c2
cpi
cmul
)
cmo
)
(
cif
(
wbr
(
co
(
cv
x1
)
(
co
c2
cpi
cmul
)
cmo
)
cpi
cle
)
cc0
(
co
c2
cpi
cmul
)
)
cmin
)
)
⟶
wceq
carg
(
cmpt
(
λ x1 .
cdif
cccbar
(
csn
cc0
)
)
(
λ x1 .
cif
(
wcel
(
cv
x1
)
cc
)
(
cfv
(
cfv
(
cv
x1
)
clog
)
cim
)
(
cfv
(
cv
x1
)
c1st
)
)
)
⟶
wceq
cmulc
(
cmpt
(
λ x1 .
cun
(
cxp
cccbar
cccbar
)
(
cxp
ccchat
ccchat
)
)
(
λ x1 .
cif
(
wo
(
wceq
(
cfv
(
cv
x1
)
c1st
)
cc0
)
(
wceq
(
cfv
(
cv
x1
)
c2nd
)
cc0
)
)
cc0
(
cif
(
wo
(
wceq
(
cfv
(
cv
x1
)
c1st
)
cinfty
)
(
wceq
(
cfv
(
cv
x1
)
c2nd
)
cinfty
)
)
cinfty
(
cif
(
wcel
(
cv
x1
)
(
cxp
cc
cc
)
)
(
co
(
cfv
(
cv
x1
)
c1st
)
(
cfv
(
cv
x1
)
c2nd
)
cmul
)
(
cfv
(
cfv
(
co
(
cfv
(
cfv
(
cv
x1
)
c1st
)
carg
)
(
cfv
(
cfv
(
cv
x1
)
c2nd
)
carg
)
caddc
)
cprcpal
)
cinftyexpi
)
)
)
)
)
⟶
wceq
cinvc
(
cmpt
(
λ x1 .
cun
cccbar
ccchat
)
(
λ x1 .
cif
(
wceq
(
cv
x1
)
cc0
)
cinfty
(
cif
(
wcel
(
cv
x1
)
cc
)
(
co
c1
(
cv
x1
)
cdiv
)
cc0
)
)
)
⟶
wceq
cfinsum
(
cmpt
(
λ x1 .
copab
(
λ x2 x3 .
wa
(
wcel
(
cv
x2
)
ccmn
)
(
wrex
(
λ x4 .
wf
(
cv
x4
)
(
cfv
(
cv
x2
)
cbs
)
(
cv
x3
)
)
(
λ x4 .
cfn
)
)
)
)
(
λ x1 .
cio
(
λ x2 .
wrex
(
λ x3 .
wex
(
λ x4 .
wa
(
wf1o
(
co
c1
(
cv
x3
)
cfz
)
(
cdm
(
cfv
(
cv
x1
)
c2nd
)
)
(
cv
x4
)
)
(
wceq
(
cv
x2
)
(
cfv
(
cv
x3
)
(
cseq
(
cfv
(
cfv
(
cv
x1
)
c1st
)
cplusg
)
(
cmpt
(
λ x5 .
cn
)
(
λ x5 .
cfv
(
cfv
(
cv
x5
)
(
cv
x4
)
)
(
cfv
(
cv
x1
)
c2nd
)
)
)
c1
)
)
)
)
)
(
λ x3 .
cn0
)
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_strset__df_bj_diag__df_bj_inftyexpi__df_bj_ccinfty__df_bj_ccbar__df_bj_pinfty__df_bj_minfty__df_bj_rrbar__df_bj_infty__df_bj_cchat__df_bj_rrhat__df_bj_addc__df_bj_oppc__df_bj_prcpal__df_bj_arg__df_bj_mulc__df_bj_invc__df_bj_finsum
proof
PUV1k..
Megalodon
-
proofgold address
TMSKS..
creator
36224
PrCmT..
/
5c8e8..
owner
36224
PrCmT..
/
5c8e8..
term root
90174..