Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
cmin
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
crio
(
λ x3 .
wceq
(
co
(
cv
x2
)
(
cv
x3
)
caddc
)
(
cv
x1
)
)
(
λ x3 .
cc
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cneg
x1
)
(
co
cc0
x1
cmin
)
)
⟶
wceq
cdiv
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cdif
cc
(
csn
cc0
)
)
(
λ x1 x2 .
crio
(
λ x3 .
wceq
(
co
(
cv
x2
)
(
cv
x3
)
cmul
)
(
cv
x1
)
)
(
λ x3 .
cc
)
)
)
⟶
wceq
cn
(
cima
(
crdg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
co
(
cv
x1
)
c1
caddc
)
)
c1
)
com
)
⟶
wceq
c2
(
co
c1
c1
caddc
)
⟶
wceq
c3
(
co
c2
c1
caddc
)
⟶
wceq
c4
(
co
c3
c1
caddc
)
⟶
wceq
c5
(
co
c4
c1
caddc
)
⟶
wceq
c6
(
co
c5
c1
caddc
)
⟶
wceq
c7
(
co
c6
c1
caddc
)
⟶
wceq
c8
(
co
c7
c1
caddc
)
⟶
wceq
c9
(
co
c8
c1
caddc
)
⟶
wceq
c10
(
co
c9
c1
caddc
)
⟶
wceq
cn0
(
cun
cn
(
csn
cc0
)
)
⟶
wceq
cxnn0
(
cun
cn0
(
csn
cpnf
)
)
⟶
wceq
cz
(
crab
(
λ x1 .
w3o
(
wceq
(
cv
x1
)
cc0
)
(
wcel
(
cv
x1
)
cn
)
(
wcel
(
cneg
(
cv
x1
)
)
cn
)
)
(
λ x1 .
cr
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cdc
x1
x2
)
(
co
(
co
(
co
c9
c1
caddc
)
x1
cmul
)
x2
caddc
)
)
⟶
wceq
cuz
(
cmpt
(
λ x1 .
cz
)
(
λ x1 .
crab
(
λ x2 .
wbr
(
cv
x1
)
(
cv
x2
)
cle
)
(
λ x2 .
cz
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_sub__df_neg__df_div__df_nn__df_2__df_3__df_4__df_5__df_6__df_7__df_8__df_9__df_10OLD__df_n0__df_xnn0__df_z__df_dec__df_uz
proof
PUV1k..
Megalodon
-
proofgold address
TMT3w..
creator
36224
PrCmT..
/
a73c5..
owner
36224
PrCmT..
/
a73c5..
term root
2de98..