Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
cifs
(
copab
(
λ x1 x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wrex
(
λ x5 .
wrex
(
λ x6 .
wrex
(
λ x7 .
wrex
(
λ x8 .
wrex
(
λ x9 .
wrex
(
λ x10 .
wrex
(
λ x11 .
w3a
(
wceq
(
cv
x1
)
(
cop
(
cop
(
cv
x4
)
(
cv
x5
)
)
(
cop
(
cv
x6
)
(
cv
x7
)
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
cop
(
cv
x8
)
(
cv
x9
)
)
(
cop
(
cv
x10
)
(
cv
x11
)
)
)
)
(
w3a
(
wa
(
wbr
(
cv
x5
)
(
cop
(
cv
x4
)
(
cv
x6
)
)
cbtwn
)
(
wbr
(
cv
x9
)
(
cop
(
cv
x8
)
(
cv
x10
)
)
cbtwn
)
)
(
wa
(
wbr
(
cop
(
cv
x4
)
(
cv
x6
)
)
(
cop
(
cv
x8
)
(
cv
x10
)
)
ccgr
)
(
wbr
(
cop
(
cv
x5
)
(
cv
x6
)
)
(
cop
(
cv
x9
)
(
cv
x10
)
)
ccgr
)
)
(
wa
(
wbr
(
cop
(
cv
x4
)
(
cv
x7
)
)
(
cop
(
cv
x8
)
(
cv
x11
)
)
ccgr
)
(
wbr
(
cop
(
cv
x6
)
(
cv
x7
)
)
(
cop
(
cv
x10
)
(
cv
x11
)
)
ccgr
)
)
)
)
(
λ x11 .
cfv
(
cv
x3
)
cee
)
)
(
λ x10 .
cfv
(
cv
x3
)
cee
)
)
(
λ x9 .
cfv
(
cv
x3
)
cee
)
)
(
λ x8 .
cfv
(
cv
x3
)
cee
)
)
(
λ x7 .
cfv
(
cv
x3
)
cee
)
)
(
λ x6 .
cfv
(
cv
x3
)
cee
)
)
(
λ x5 .
cfv
(
cv
x3
)
cee
)
)
(
λ x4 .
cfv
(
cv
x3
)
cee
)
)
(
λ x3 .
cn
)
)
)
⟶
wceq
ccgr3
(
copab
(
λ x1 x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wrex
(
λ x5 .
wrex
(
λ x6 .
wrex
(
λ x7 .
wrex
(
λ x8 .
wrex
(
λ x9 .
w3a
(
wceq
(
cv
x1
)
(
cop
(
cv
x4
)
(
cop
(
cv
x5
)
(
cv
x6
)
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
cv
x7
)
(
cop
(
cv
x8
)
(
cv
x9
)
)
)
)
(
w3a
(
wbr
(
cop
(
cv
x4
)
(
cv
x5
)
)
(
cop
(
cv
x7
)
(
cv
x8
)
)
ccgr
)
(
wbr
(
cop
(
cv
x4
)
(
cv
x6
)
)
(
cop
(
cv
x7
)
(
cv
x9
)
)
ccgr
)
(
wbr
(
cop
(
cv
x5
)
(
cv
x6
)
)
(
cop
(
cv
x8
)
(
cv
x9
)
)
ccgr
)
)
)
(
λ x9 .
cfv
(
cv
x3
)
cee
)
)
(
λ x8 .
cfv
(
cv
x3
)
cee
)
)
(
λ x7 .
cfv
(
cv
x3
)
cee
)
)
(
λ x6 .
cfv
(
cv
x3
)
cee
)
)
(
λ x5 .
cfv
(
cv
x3
)
cee
)
)
(
λ x4 .
cfv
(
cv
x3
)
cee
)
)
(
λ x3 .
cn
)
)
)
⟶
wceq
cfs
(
copab
(
λ x1 x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wrex
(
λ x5 .
wrex
(
λ x6 .
wrex
(
λ x7 .
wrex
(
λ x8 .
wrex
(
λ x9 .
wrex
(
λ x10 .
wrex
(
λ x11 .
w3a
(
wceq
(
cv
x1
)
(
cop
(
cop
(
cv
x4
)
(
cv
x5
)
)
(
cop
(
cv
x6
)
(
cv
x7
)
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
cop
(
cv
x8
)
(
cv
x9
)
)
(
cop
(
cv
x10
)
(
cv
x11
)
)
)
)
(
w3a
(
wbr
(
cv
x4
)
(
cop
(
cv
x5
)
(
cv
x6
)
)
ccolin
)
(
wbr
(
cop
(
cv
x4
)
(
cop
(
cv
x5
)
(
cv
x6
)
)
)
(
cop
(
cv
x8
)
(
cop
(
cv
x9
)
(
cv
x10
)
)
)
ccgr3
)
(
wa
(
wbr
(
cop
(
cv
x4
)
(
cv
x7
)
)
(
cop
(
cv
x8
)
(
cv
x11
)
)
ccgr
)
(
wbr
(
cop
(
cv
x5
)
(
cv
x7
)
)
(
cop
(
cv
x9
)
(
cv
x11
)
)
ccgr
)
)
)
)
(
λ x11 .
cfv
(
cv
x3
)
cee
)
)
(
λ x10 .
cfv
(
cv
x3
)
cee
)
)
(
λ x9 .
cfv
(
cv
x3
)
cee
)
)
(
λ x8 .
cfv
(
cv
x3
)
cee
)
)
(
λ x7 .
cfv
(
cv
x3
)
cee
)
)
(
λ x6 .
cfv
(
cv
x3
)
cee
)
)
(
λ x5 .
cfv
(
cv
x3
)
cee
)
)
(
λ x4 .
cfv
(
cv
x3
)
cee
)
)
(
λ x3 .
cn
)
)
)
⟶
wceq
csegle
(
copab
(
λ x1 x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wrex
(
λ x5 .
wrex
(
λ x6 .
wrex
(
λ x7 .
w3a
(
wceq
(
cv
x1
)
(
cop
(
cv
x4
)
(
cv
x5
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
cv
x6
)
(
cv
x7
)
)
)
(
wrex
(
λ x8 .
wa
(
wbr
(
cv
x8
)
(
cop
(
cv
x6
)
(
cv
x7
)
)
cbtwn
)
(
wbr
(
cop
(
cv
x4
)
(
cv
x5
)
)
(
cop
(
cv
x6
)
(
cv
x8
)
)
ccgr
)
)
(
λ x8 .
cfv
(
cv
x3
)
cee
)
)
)
(
λ x7 .
cfv
(
cv
x3
)
cee
)
)
(
λ x6 .
cfv
(
cv
x3
)
cee
)
)
(
λ x5 .
cfv
(
cv
x3
)
cee
)
)
(
λ x4 .
cfv
(
cv
x3
)
cee
)
)
(
λ x3 .
cn
)
)
)
⟶
wceq
coutsideof
(
cdif
ccolin
cbtwn
)
⟶
wceq
cline2
(
coprab
(
λ x1 x2 x3 .
wrex
(
λ x4 .
wa
(
w3a
(
wcel
(
cv
x1
)
(
cfv
(
cv
x4
)
cee
)
)
(
wcel
(
cv
x2
)
(
cfv
(
cv
x4
)
cee
)
)
(
wne
(
cv
x1
)
(
cv
x2
)
)
)
(
wceq
(
cv
x3
)
(
cec
(
cop
(
cv
x1
)
(
cv
x2
)
)
(
ccnv
ccolin
)
)
)
)
(
λ x4 .
cn
)
)
)
⟶
wceq
cray
(
coprab
(
λ x1 x2 x3 .
wrex
(
λ x4 .
wa
(
w3a
(
wcel
(
cv
x1
)
(
cfv
(
cv
x4
)
cee
)
)
(
wcel
(
cv
x2
)
(
cfv
(
cv
x4
)
cee
)
)
(
wne
(
cv
x1
)
(
cv
x2
)
)
)
(
wceq
(
cv
x3
)
(
crab
(
λ x5 .
wbr
(
cv
x1
)
(
cop
(
cv
x2
)
(
cv
x5
)
)
coutsideof
)
(
λ x5 .
cfv
(
cv
x4
)
cee
)
)
)
)
(
λ x4 .
cn
)
)
)
⟶
wceq
clines2
(
crn
cline2
)
⟶
wceq
cfwddif
(
cmpt
(
λ x1 .
co
cc
cc
cpm
)
(
λ x1 .
cmpt
(
λ x2 .
crab
(
λ x3 .
wcel
(
co
(
cv
x3
)
c1
caddc
)
(
cdm
(
cv
x1
)
)
)
(
λ x3 .
cdm
(
cv
x1
)
)
)
(
λ x2 .
co
(
cfv
(
co
(
cv
x2
)
c1
caddc
)
(
cv
x1
)
)
(
cfv
(
cv
x2
)
(
cv
x1
)
)
cmin
)
)
)
⟶
wceq
cfwddifn
(
cmpt2
(
λ x1 x2 .
cn0
)
(
λ x1 x2 .
co
cc
cc
cpm
)
(
λ x1 x2 .
cmpt
(
λ x3 .
crab
(
λ x4 .
wral
(
λ x5 .
wcel
(
co
(
cv
x4
)
(
cv
x5
)
caddc
)
(
cdm
(
cv
x2
)
)
)
(
λ x5 .
co
cc0
(
cv
x1
)
cfz
)
)
(
λ x4 .
cc
)
)
(
λ x3 .
csu
(
co
cc0
(
cv
x1
)
cfz
)
(
λ x4 .
co
(
co
(
cv
x1
)
(
cv
x4
)
cbc
)
(
co
(
co
(
cneg
c1
)
(
co
(
cv
x1
)
(
cv
x4
)
cmin
)
cexp
)
(
cfv
(
co
(
cv
x3
)
(
cv
x4
)
caddc
)
(
cv
x2
)
)
cmul
)
cmul
)
)
)
)
⟶
wceq
chf
(
cuni
(
cima
cr1
com
)
)
⟶
wceq
cfne
(
copab
(
λ x1 x2 .
wa
(
wceq
(
cuni
(
cv
x1
)
)
(
cuni
(
cv
x2
)
)
)
(
wral
(
λ x3 .
wss
(
cv
x3
)
(
cuni
(
cin
(
cv
x2
)
(
cpw
(
cv
x3
)
)
)
)
)
(
λ x3 .
cv
x1
)
)
)
)
⟶
(
∀ x1 x2 x3 : ο .
wb
(
w3nand
x1
x2
x3
)
(
x1
⟶
x2
⟶
wn
x3
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cgcdOLD
x1
x2
)
(
csup
(
crab
(
λ x3 .
wa
(
wcel
(
co
x1
(
cv
x3
)
cdiv
)
cn
)
(
wcel
(
co
x2
(
cv
x3
)
cdiv
)
cn
)
)
(
λ x3 .
cn
)
)
cn
clt
)
)
⟶
(
∀ x1 : ο .
x1
⟶
cprvb
x1
)
⟶
(
∀ x1 x2 : ο .
cprvb
(
x1
⟶
x2
)
⟶
cprvb
x1
⟶
cprvb
x2
)
⟶
(
∀ x1 : ο .
cprvb
x1
⟶
cprvb
(
cprvb
x1
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 .
wb
(
wssb
x1
x2
)
(
∀ x3 .
wceq
(
cv
x3
)
(
cv
x2
)
⟶
∀ x4 .
wceq
(
cv
x4
)
(
cv
x3
)
⟶
x1
x4
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_ifs__df_cgr3__df_fs__df_segle__df_outsideof__df_line2__df_ray__df_lines2__df_fwddif__df_fwddifn__df_hf__df_fne__df_3nand__df_gcdOLD__ax_prv1__ax_prv2__ax_prv3__df_ssb
proof
PUV1k..
Megalodon
-
proofgold address
TMV4u..
creator
36224
PrCmT..
/
0a38c..
owner
36224
PrCmT..
/
0a38c..
term root
a916a..