Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
cq
(
cima
cdiv
(
cxp
cz
cn
)
)
⟶
wceq
crp
(
crab
(
λ x1 .
wbr
cc0
(
cv
x1
)
clt
)
(
λ x1 .
cr
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cxne
x1
)
(
cif
(
wceq
x1
cpnf
)
cmnf
(
cif
(
wceq
x1
cmnf
)
cpnf
(
cneg
x1
)
)
)
)
⟶
wceq
cxad
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cif
(
wceq
(
cv
x1
)
cpnf
)
(
cif
(
wceq
(
cv
x2
)
cmnf
)
cc0
cpnf
)
(
cif
(
wceq
(
cv
x1
)
cmnf
)
(
cif
(
wceq
(
cv
x2
)
cpnf
)
cc0
cmnf
)
(
cif
(
wceq
(
cv
x2
)
cpnf
)
cpnf
(
cif
(
wceq
(
cv
x2
)
cmnf
)
cmnf
(
co
(
cv
x1
)
(
cv
x2
)
caddc
)
)
)
)
)
)
⟶
wceq
cxmu
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cif
(
wo
(
wceq
(
cv
x1
)
cc0
)
(
wceq
(
cv
x2
)
cc0
)
)
cc0
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x2
)
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
(
wa
(
wbr
(
cv
x2
)
cc0
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x2
)
cpnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x2
)
cmnf
)
)
)
)
cpnf
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x2
)
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
(
wa
(
wbr
(
cv
x2
)
cc0
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x2
)
cmnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x2
)
cpnf
)
)
)
)
cmnf
(
co
(
cv
x1
)
(
cv
x2
)
cmul
)
)
)
)
)
⟶
wceq
cioo
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
clt
)
(
wbr
(
cv
x3
)
(
cv
x2
)
clt
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cioc
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
clt
)
(
wbr
(
cv
x3
)
(
cv
x2
)
cle
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cico
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
cle
)
(
wbr
(
cv
x3
)
(
cv
x2
)
clt
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cicc
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
cle
)
(
wbr
(
cv
x3
)
(
cv
x2
)
cle
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cfz
(
cmpt2
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
cle
)
(
wbr
(
cv
x3
)
(
cv
x2
)
cle
)
)
(
λ x3 .
cz
)
)
)
⟶
wceq
cfzo
(
cmpt2
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
co
(
cv
x1
)
(
co
(
cv
x2
)
c1
cmin
)
cfz
)
)
⟶
wceq
cfl
(
cmpt
(
λ x1 .
cr
)
(
λ x1 .
crio
(
λ x2 .
wa
(
wbr
(
cv
x2
)
(
cv
x1
)
cle
)
(
wbr
(
cv
x1
)
(
co
(
cv
x2
)
c1
caddc
)
clt
)
)
(
λ x2 .
cz
)
)
)
⟶
wceq
cceil
(
cmpt
(
λ x1 .
cr
)
(
λ x1 .
cneg
(
cfv
(
cneg
(
cv
x1
)
)
cfl
)
)
)
⟶
wceq
cmo
(
cmpt2
(
λ x1 x2 .
cr
)
(
λ x1 x2 .
crp
)
(
λ x1 x2 .
co
(
cv
x1
)
(
co
(
cv
x2
)
(
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cdiv
)
cfl
)
cmul
)
cmin
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wceq
(
cseq
x1
x2
x3
)
(
cima
(
crdg
(
cmpt2
(
λ x4 x5 .
cvv
)
(
λ x4 x5 .
cvv
)
(
λ x4 x5 .
cop
(
co
(
cv
x4
)
c1
caddc
)
(
co
(
cv
x5
)
(
cfv
(
co
(
cv
x4
)
c1
caddc
)
x2
)
x1
)
)
)
(
cop
x3
(
cfv
x3
x2
)
)
)
com
)
)
⟶
wceq
cexp
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cif
(
wceq
(
cv
x2
)
cc0
)
c1
(
cif
(
wbr
cc0
(
cv
x2
)
clt
)
(
cfv
(
cv
x2
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x1
)
)
)
c1
)
)
(
co
c1
(
cfv
(
cneg
(
cv
x2
)
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x1
)
)
)
c1
)
)
cdiv
)
)
)
)
⟶
wceq
cfa
(
cun
(
csn
(
cop
cc0
c1
)
)
(
cseq
cmul
cid
c1
)
)
⟶
wceq
cbc
(
cmpt2
(
λ x1 x2 .
cn0
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cif
(
wcel
(
cv
x2
)
(
co
cc0
(
cv
x1
)
cfz
)
)
(
co
(
cfv
(
cv
x1
)
cfa
)
(
co
(
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cmin
)
cfa
)
(
cfv
(
cv
x2
)
cfa
)
cmul
)
cdiv
)
cc0
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_q__df_rp__df_xneg__df_xadd__df_xmul__df_ioo__df_ioc__df_ico__df_icc__df_fz__df_fzo__df_fl__df_ceil__df_mod__df_seq__df_exp__df_fac__df_bc
proof
PUV1k..
Megalodon
-
proofgold address
TMVLS..
creator
36224
PrCmT..
/
c628b..
owner
36224
PrCmT..
/
c628b..
term root
243c6..