Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
(
∀ x1 :
ι → ο
.
∀ x2 .
(
∀ x3 .
x1
x3
)
⟶
wsb
x1
x2
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 .
(
∀ x3 .
x1
x3
)
⟶
wsb
x1
x2
)
⟶
wceq
cbcc
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cn0
)
(
λ x1 x2 .
co
(
co
(
cv
x1
)
(
cv
x2
)
cfallfac
)
(
cfv
(
cv
x2
)
cfa
)
cdiv
)
)
⟶
wceq
cplusr
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cr
)
(
λ x3 .
co
(
cfv
(
cv
x3
)
(
cv
x1
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
caddc
)
)
)
⟶
wceq
cminusr
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cr
)
(
λ x3 .
co
(
cfv
(
cv
x3
)
(
cv
x1
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
cmin
)
)
)
⟶
wceq
ctimesr
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cr
)
(
λ x3 .
co
(
cv
x1
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
cmul
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cptdfc
x1
x2
)
(
cmpt
(
λ x3 .
cr
)
(
λ x3 .
cima
(
co
(
co
(
cv
x3
)
(
co
x2
x1
cminusr
)
ctimesr
)
x1
cpv
)
(
ctp
c1
c2
c3
)
)
)
)
⟶
wceq
crr3c
(
co
cr
(
ctp
c1
c2
c3
)
cmap
)
⟶
wceq
cline3
(
crab
(
λ x1 .
wa
(
wbr
c2o
(
cv
x1
)
cdom
)
(
wral
(
λ x2 .
wral
(
λ x3 .
wne
(
cv
x3
)
(
cv
x2
)
⟶
wceq
(
crn
(
cptdfc
(
cv
x2
)
(
cv
x3
)
)
)
(
cv
x1
)
)
(
λ x3 .
cv
x1
)
)
(
λ x2 .
cv
x1
)
)
)
(
λ x1 .
cpw
crr3c
)
)
⟶
(
∀ x1 x2 : ο .
wb
(
wvd1
x1
x2
)
(
x1
⟶
x2
)
)
⟶
(
∀ x1 x2 x3 : ο .
wb
(
wvd2
x1
x2
x3
)
(
wa
x1
x2
⟶
x3
)
)
⟶
(
∀ x1 x2 : ο .
wb
(
wvhc2
x1
x2
)
(
wa
x1
x2
)
)
⟶
(
∀ x1 x2 x3 : ο .
wb
(
wvhc3
x1
x2
x3
)
(
w3a
x1
x2
x3
)
)
⟶
(
∀ x1 x2 x3 x4 : ο .
wb
(
wvd3
x1
x2
x3
x4
)
(
w3a
x1
x2
x3
⟶
x4
)
)
⟶
wceq
clsi
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
csup
(
crn
(
cmpt
(
λ x2 .
cr
)
(
λ x2 .
cinf
(
cin
(
cima
(
cv
x1
)
(
co
(
cv
x2
)
cpnf
cico
)
)
cxr
)
cxr
clt
)
)
)
cxr
clt
)
)
⟶
wceq
clsxlim
(
cfv
(
cfv
cle
cordt
)
clm
)
⟶
wceq
csalg
(
cab
(
λ x1 .
w3a
(
wcel
c0
(
cv
x1
)
)
(
wral
(
λ x2 .
wcel
(
cdif
(
cuni
(
cv
x1
)
)
(
cv
x2
)
)
(
cv
x1
)
)
(
λ x2 .
cv
x1
)
)
(
wral
(
λ x2 .
wbr
(
cv
x2
)
com
cdom
⟶
wcel
(
cuni
(
cv
x2
)
)
(
cv
x1
)
)
(
λ x2 .
cpw
(
cv
x1
)
)
)
)
)
⟶
wceq
csalon
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wceq
(
cuni
(
cv
x2
)
)
(
cv
x1
)
)
(
λ x2 .
csalg
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
ax_frege58b__ax_frege58b_b__df_bcc__df_addr__df_subr__df_mulv__df_ptdf__df_rr3__df_line3__df_vd1__df_vd2__df_vhc2__df_vhc3__df_vd3__df_liminf__df_xlim__df_salg__df_salon
proof
PUV1k..
Megalodon
-
proofgold address
TMGeN..
creator
36224
PrCmT..
/
47110..
owner
36224
PrCmT..
/
47110..
term root
f4d31..