Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
cbigo
(
cmpt
(
λ x1 .
co
cr
cr
cpm
)
(
λ x1 .
crab
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wral
(
λ x5 .
wbr
(
cfv
(
cv
x5
)
(
cv
x2
)
)
(
co
(
cv
x4
)
(
cfv
(
cv
x5
)
(
cv
x1
)
)
cmul
)
cle
)
(
λ x5 .
cin
(
cdm
(
cv
x2
)
)
(
co
(
cv
x3
)
cpnf
cico
)
)
)
(
λ x4 .
cr
)
)
(
λ x3 .
cr
)
)
(
λ x2 .
co
cr
cr
cpm
)
)
)
⟶
wceq
cblen
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cif
(
wceq
(
cv
x1
)
cc0
)
c1
(
co
(
cfv
(
co
c2
(
cfv
(
cv
x1
)
cabs
)
clogb
)
cfl
)
c1
caddc
)
)
)
⟶
wceq
cdig
(
cmpt
(
λ x1 .
cn
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cz
)
(
λ x2 x3 .
co
cc0
cpnf
cico
)
(
λ x2 x3 .
co
(
cfv
(
co
(
co
(
cv
x1
)
(
cneg
(
cv
x2
)
)
cexp
)
(
cv
x3
)
cmul
)
cfl
)
(
cv
x1
)
cmo
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
csetrecs
x1
)
(
cuni
(
cab
(
λ x2 .
∀ x3 .
(
∀ x4 .
wss
(
cv
x4
)
(
cv
x2
)
⟶
wss
(
cv
x4
)
(
cv
x3
)
⟶
wss
(
cfv
(
cv
x4
)
x1
)
(
cv
x3
)
)
⟶
wss
(
cv
x2
)
(
cv
x3
)
)
)
)
)
⟶
wceq
cpg
(
csetrecs
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cxp
(
cpw
(
cv
x1
)
)
(
cpw
(
cv
x1
)
)
)
)
)
⟶
wceq
cge_real
(
ccnv
cle
)
⟶
wceq
cgt
(
ccnv
clt
)
⟶
wceq
csinh
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
co
(
cfv
(
co
ci
(
cv
x1
)
cmul
)
csin
)
ci
cdiv
)
)
⟶
wceq
ccosh
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
cfv
(
co
ci
(
cv
x1
)
cmul
)
ccos
)
)
⟶
wceq
ctanh
(
cmpt
(
λ x1 .
cima
(
ccnv
ccosh
)
(
cdif
cc
(
csn
cc0
)
)
)
(
λ x1 .
co
(
cfv
(
co
ci
(
cv
x1
)
cmul
)
ctan
)
ci
cdiv
)
)
⟶
wceq
csec
(
cmpt
(
λ x1 .
crab
(
λ x2 .
wne
(
cfv
(
cv
x2
)
ccos
)
cc0
)
(
λ x2 .
cc
)
)
(
λ x1 .
co
c1
(
cfv
(
cv
x1
)
ccos
)
cdiv
)
)
⟶
wceq
ccsc
(
cmpt
(
λ x1 .
crab
(
λ x2 .
wne
(
cfv
(
cv
x2
)
csin
)
cc0
)
(
λ x2 .
cc
)
)
(
λ x1 .
co
c1
(
cfv
(
cv
x1
)
csin
)
cdiv
)
)
⟶
wceq
ccot
(
cmpt
(
λ x1 .
crab
(
λ x2 .
wne
(
cfv
(
cv
x2
)
csin
)
cc0
)
(
λ x2 .
cc
)
)
(
λ x1 .
co
(
cfv
(
cv
x1
)
ccos
)
(
cfv
(
cv
x1
)
csin
)
cdiv
)
)
⟶
wceq
clog_
(
cmpt
(
λ x1 .
cdif
cc
(
cpr
cc0
c1
)
)
(
λ x1 .
cmpt
(
λ x2 .
cdif
cc
(
csn
cc0
)
)
(
λ x2 .
co
(
cfv
(
cv
x2
)
clog
)
(
cfv
(
cv
x1
)
clog
)
cdiv
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wreflexive
x1
x2
)
(
wa
(
wss
x2
(
cxp
x1
x1
)
)
(
wral
(
λ x3 .
wbr
(
cv
x3
)
(
cv
x3
)
x2
)
(
λ x3 .
x1
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wirreflexive
x1
x2
)
(
wa
(
wss
x2
(
cxp
x1
x1
)
)
(
wral
(
λ x3 .
wn
(
wbr
(
cv
x3
)
(
cv
x3
)
x2
)
)
(
λ x3 .
x1
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
walsi
x1
x2
)
(
wa
(
∀ x3 .
x1
x3
⟶
x2
x3
)
(
wex
x1
)
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
wb
(
walsc
x1
x2
)
(
wa
(
wral
x1
x2
)
(
wex
(
λ x3 .
wcel
(
cv
x3
)
(
x2
x3
)
)
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_bigo__df_blen__df_dig__df_setrecs__df_pg__df_gte__df_gt__df_sinh__df_cosh__df_tanh__df_sec__df_csc__df_cot__df_logbALT__df_reflexive__df_irreflexive__df_alsi__df_alsc
proof
PUV1k..
Megalodon
-
proofgold address
TMJW4..
creator
36224
PrCmT..
/
f7ebc..
owner
36224
PrCmT..
/
f7ebc..
term root
0a153..