Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
(
∀ x1 x2 :
ι → ο
.
wb
(
wfn
x1
x2
)
(
wa
(
wfun
x1
)
(
wceq
(
cdm
x1
)
x2
)
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wb
(
wf
x1
x2
x3
)
(
wa
(
wfn
x3
x1
)
(
wss
(
crn
x3
)
x2
)
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wb
(
wf1
x1
x2
x3
)
(
wa
(
wf
x1
x2
x3
)
(
wfun
(
ccnv
x3
)
)
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wb
(
wfo
x1
x2
x3
)
(
wa
(
wfn
x3
x1
)
(
wceq
(
crn
x3
)
x2
)
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wb
(
wf1o
x1
x2
x3
)
(
wa
(
wf1
x1
x2
x3
)
(
wfo
x1
x2
x3
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cfv
x1
x2
)
(
cio
(
λ x3 .
wbr
x1
(
cv
x3
)
x2
)
)
)
⟶
(
∀ x1 x2 x3 x4 x5 :
ι → ο
.
wb
(
wiso
x1
x2
x3
x4
x5
)
(
wa
(
wf1o
x1
x2
x5
)
(
wral
(
λ x6 .
wral
(
λ x7 .
wb
(
wbr
(
cv
x6
)
(
cv
x7
)
x3
)
(
wbr
(
cfv
(
cv
x6
)
x5
)
(
cfv
(
cv
x7
)
x5
)
x4
)
)
(
λ x7 .
x1
)
)
(
λ x6 .
x1
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
wceq
(
crio
x1
x2
)
(
cio
(
λ x3 .
wa
(
wcel
(
cv
x3
)
(
x2
x3
)
)
(
x1
x3
)
)
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wceq
(
co
x1
x2
x3
)
(
cfv
(
cop
x1
x2
)
x3
)
)
⟶
(
∀ x1 :
ι →
ι →
ι → ο
.
wceq
(
coprab
x1
)
(
cab
(
λ x2 .
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wa
(
wceq
(
cv
x2
)
(
cop
(
cop
(
cv
x3
)
(
cv
x4
)
)
(
cv
x5
)
)
)
(
x1
x3
x4
x5
)
)
)
)
)
)
)
⟶
(
∀ x1 x2 x3 :
ι →
ι →
ι → ο
.
wceq
(
cmpt2
x1
x2
x3
)
(
coprab
(
λ x4 x5 x6 .
wa
(
wa
(
wcel
(
cv
x4
)
(
x1
x4
x5
)
)
(
wcel
(
cv
x5
)
(
x2
x4
x5
)
)
)
(
wceq
(
cv
x6
)
(
x3
x4
x5
)
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cof
x1
)
(
cmpt2
(
λ x2 x3 .
cvv
)
(
λ x2 x3 .
cvv
)
(
λ x2 x3 .
cmpt
(
λ x4 .
cin
(
cdm
(
cv
x2
)
)
(
cdm
(
cv
x3
)
)
)
(
λ x4 .
co
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x4
)
(
cv
x3
)
)
x1
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cofr
x1
)
(
copab
(
λ x2 x3 .
wral
(
λ x4 .
wbr
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x4
)
(
cv
x3
)
)
x1
)
(
λ x4 .
cin
(
cdm
(
cv
x2
)
)
(
cdm
(
cv
x3
)
)
)
)
)
)
⟶
wceq
crpss
(
copab
(
λ x1 x2 .
wpss
(
cv
x1
)
(
cv
x2
)
)
)
⟶
(
∀ x1 .
wex
(
λ x2 .
∀ x3 .
wex
(
λ x4 .
wa
(
wcel
(
cv
x3
)
(
cv
x4
)
)
(
wcel
(
cv
x4
)
(
cv
x1
)
)
)
⟶
wcel
(
cv
x3
)
(
cv
x2
)
)
)
⟶
wceq
com
(
crab
(
λ x1 .
∀ x2 .
wlim
(
cv
x2
)
⟶
wcel
(
cv
x1
)
(
cv
x2
)
)
(
λ x1 .
con0
)
)
⟶
wceq
c1st
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cuni
(
cdm
(
csn
(
cv
x1
)
)
)
)
)
⟶
wceq
c2nd
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cuni
(
crn
(
csn
(
cv
x1
)
)
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_fn__df_f__df_f1__df_fo__df_f1o__df_fv__df_isom__df_riota__df_ov__df_oprab__df_mpt2__df_of__df_ofr__df_rpss__ax_un__df_om__df_1st__df_2nd
proof
PUV1k..
Megalodon
-
proofgold address
TMF73..
creator
36224
PrCmT..
/
a19a0..
owner
36224
PrCmT..
/
a19a0..
term root
d0ca4..