Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr4wN..
/
4ea21..
PUNFh..
/
0dde6..
vout
Pr4wN..
/
88c9d..
0.10 bars
TMRao..
/
ea9f3..
ownership of
78de9..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMUze..
/
e815f..
ownership of
b1a4d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMbmw..
/
04ce9..
ownership of
ccd37..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMJGK..
/
0cf25..
ownership of
f5d7f..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPV6..
/
72e08..
ownership of
c352a..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcgd..
/
8bdb0..
ownership of
e4db9..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMbBp..
/
17c28..
ownership of
be63d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMTdk..
/
f7558..
ownership of
2a60e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMFvq..
/
725fc..
ownership of
86f75..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMEqN..
/
230c2..
ownership of
ad643..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMRxC..
/
b4415..
ownership of
be6df..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPPb..
/
220d3..
ownership of
247ed..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMXas..
/
858c7..
ownership of
99912..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMYy7..
/
3d22c..
ownership of
a7a93..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMb5U..
/
e63cf..
ownership of
2b841..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMFw7..
/
9db61..
ownership of
17d58..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMW5d..
/
e407f..
ownership of
881a5..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMTzk..
/
ffd52..
ownership of
70729..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMRt6..
/
1e875..
ownership of
a1afb..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMS8P..
/
ed5ea..
ownership of
9056f..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMGt3..
/
1dec0..
ownership of
5be8b..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMWKn..
/
e8ea5..
ownership of
b873f..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcQ8..
/
4a3b2..
ownership of
0e7f0..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQf7..
/
760ca..
ownership of
075b8..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMUC7..
/
a6ae8..
ownership of
18ac8..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMafu..
/
050d1..
ownership of
402f2..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZdX..
/
e1bfc..
ownership of
b6fb9..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcrc..
/
7bf1c..
ownership of
f5ca1..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZjp..
/
a724e..
ownership of
2e021..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMU28..
/
430ee..
ownership of
d2068..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMTYq..
/
7cb7e..
ownership of
b3b64..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMTpT..
/
3f237..
ownership of
e862e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQnX..
/
ce1d0..
ownership of
52257..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMHrA..
/
b9e1b..
ownership of
3fd45..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMNb1..
/
841f5..
ownership of
163bf..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMa7n..
/
1a000..
ownership of
584b5..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
PUbPn..
/
6f7bf..
doc published by
PrCmT..
Known
df_rag__df_perpg__df_hpg__df_mid__df_lmi__df_cgra__df_inag__df_leag__df_eqlg__df_ttg__df_ee__df_btwn__df_cgr__df_eeng__df_edgf__df_vtx__df_iedg__df_edg
:
∀ x0 : ο .
(
wceq
crag
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wa
(
wceq
(
cfv
(
cv
x2
)
chash
)
c3
)
(
wceq
(
co
(
cfv
cc0
(
cv
x2
)
)
(
cfv
c2
(
cv
x2
)
)
(
cfv
(
cv
x1
)
cds
)
)
(
co
(
cfv
cc0
(
cv
x2
)
)
(
cfv
(
cfv
c2
(
cv
x2
)
)
(
cfv
(
cfv
c1
(
cv
x2
)
)
(
cfv
(
cv
x1
)
cmir
)
)
)
(
cfv
(
cv
x1
)
cds
)
)
)
)
(
λ x2 .
cword
(
cfv
(
cv
x1
)
cbs
)
)
)
)
⟶
wceq
cperpg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wa
(
wa
(
wcel
(
cv
x2
)
(
crn
(
cfv
(
cv
x1
)
clng
)
)
)
(
wcel
(
cv
x3
)
(
crn
(
cfv
(
cv
x1
)
clng
)
)
)
)
(
wrex
(
λ x4 .
wral
(
λ x5 .
wral
(
λ x6 .
wcel
(
cs3
(
cv
x5
)
(
cv
x4
)
(
cv
x6
)
)
(
cfv
(
cv
x1
)
crag
)
)
(
λ x6 .
cv
x3
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cin
(
cv
x2
)
(
cv
x3
)
)
)
)
)
)
⟶
wceq
chpg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
crn
(
cfv
(
cv
x1
)
clng
)
)
(
λ x2 .
copab
(
λ x3 x4 .
wsbc
(
λ x5 .
wsbc
(
λ x6 .
wrex
(
λ x7 .
wa
(
wa
(
wa
(
wcel
(
cv
x3
)
(
cdif
(
cv
x5
)
(
cv
x2
)
)
)
(
wcel
(
cv
x7
)
(
cdif
(
cv
x5
)
(
cv
x2
)
)
)
)
(
wrex
(
λ x8 .
wcel
(
cv
x8
)
(
co
(
cv
x3
)
(
cv
x7
)
(
cv
x6
)
)
)
(
λ x8 .
cv
x2
)
)
)
(
wa
(
wa
(
wcel
(
cv
x4
)
(
cdif
(
cv
x5
)
(
cv
x2
)
)
)
(
wcel
(
cv
x7
)
(
cdif
(
cv
x5
)
(
cv
x2
)
)
)
)
(
wrex
(
λ x8 .
wcel
(
cv
x8
)
(
co
(
cv
x4
)
(
cv
x7
)
(
cv
x6
)
)
)
(
λ x8 .
cv
x2
)
)
)
)
(
λ x7 .
cv
x5
)
)
(
cfv
(
cv
x1
)
citv
)
)
(
cfv
(
cv
x1
)
cbs
)
)
)
)
)
⟶
wceq
cmid
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 x3 .
crio
(
λ x4 .
wceq
(
cv
x3
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x1
)
cmir
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
⟶
wceq
clmi
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
crn
(
cfv
(
cv
x1
)
clng
)
)
(
λ x2 .
cmpt
(
λ x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x3 .
crio
(
λ x4 .
wa
(
wcel
(
co
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cmid
)
)
(
cv
x2
)
)
(
wo
(
wbr
(
cv
x2
)
(
co
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
clng
)
)
(
cfv
(
cv
x1
)
cperpg
)
)
(
wceq
(
cv
x3
)
(
cv
x4
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
)
⟶
wceq
ccgra
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wsbc
(
λ x4 .
wsbc
(
λ x5 .
wa
(
wa
(
wcel
(
cv
x2
)
(
co
(
cv
x4
)
(
co
cc0
c3
cfzo
)
cmap
)
)
(
wcel
(
cv
x3
)
(
co
(
cv
x4
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(
wrex
(
λ x6 .
wrex
(
λ x7 .
w3a
(
wbr
(
cv
x2
)
(
cs3
(
cv
x6
)
(
cfv
c1
(
cv
x3
)
)
(
cv
x7
)
)
(
cfv
(
cv
x1
)
ccgrg
)
)
(
wbr
(
cv
x6
)
(
cfv
cc0
(
cv
x3
)
)
(
cfv
(
cfv
c1
(
cv
x3
)
)
(
cv
x5
)
)
)
(
wbr
(
cv
x7
)
(
cfv
c2
(
cv
x3
)
)
(
cfv
(
cfv
c1
(
cv
x3
)
)
(
cv
x5
)
)
)
)
(
λ x7 .
cv
x4
)
)
(
λ x6 .
cv
x4
)
)
)
(
cfv
(
cv
x1
)
chlg
)
)
(
cfv
(
cv
x1
)
cbs
)
)
)
)
⟶
wceq
cinag
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wa
(
wa
(
wcel
(
cv
x2
)
(
cfv
(
cv
x1
)
cbs
)
)
(
wcel
(
cv
x3
)
(
co
(
cfv
(
cv
x1
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(
wa
(
w3a
(
wne
(
cfv
cc0
(
cv
x3
)
)
(
cfv
c1
(
cv
x3
)
)
)
(
wne
(
cfv
c2
(
cv
x3
)
)
(
cfv
c1
(
cv
x3
)
)
)
(
wne
(
cv
x2
)
(
cfv
c1
(
cv
x3
)
)
)
)
(
wrex
(
λ x4 .
wa
(
wcel
(
cv
x4
)
(
co
(
cfv
cc0
(
cv
x3
)
)
(
cfv
c2
(
cv
x3
)
)
(
cfv
(
cv
x1
)
citv
)
)
)
(
wo
(
wceq
(
cv
x4
)
(
cfv
c1
(
cv
x3
)
)
)
(
wbr
(
cv
x4
)
(
cv
x2
)
(
cfv
(
cfv
c1
(
cv
x3
)
)
(
cfv
(
cv
x1
)
chlg
)
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
)
)
⟶
wceq
cleag
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wa
(
wa
(
wcel
(
cv
x2
)
(
co
(
cfv
(
cv
x1
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
(
wcel
(
cv
x3
)
(
co
(
cfv
(
cv
x1
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(
wrex
(
λ x4 .
wa
(
wbr
(
cv
x4
)
(
cs3
(
cfv
cc0
(
cv
x3
)
)
(
cfv
c1
(
cv
x3
)
)
(
cfv
c2
(
cv
x3
)
)
)
(
cfv
(
cv
x1
)
cinag
)
)
(
wbr
(
cs3
(
cfv
cc0
(
cv
x2
)
)
(
cfv
c1
(
cv
x2
)
)
(
cfv
c2
(
cv
x2
)
)
)
(
cs3
(
cfv
cc0
(
cv
x3
)
)
(
cfv
c1
(
cv
x3
)
)
(
cv
x4
)
)
(
cfv
(
cv
x1
)
ccgra
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
)
⟶
wceq
ceqlg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wbr
(
cv
x2
)
(
cs3
(
cfv
c1
(
cv
x2
)
)
(
cfv
c2
(
cv
x2
)
)
(
cfv
cc0
(
cv
x2
)
)
)
(
cfv
(
cv
x1
)
ccgrg
)
)
(
λ x2 .
co
(
cfv
(
cv
x1
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
⟶
wceq
cttg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
csb
(
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 x3 .
crab
(
λ x4 .
wrex
(
λ x5 .
wceq
(
co
(
cv
x4
)
(
cv
x2
)
(
cfv
(
cv
x1
)
csg
)
)
(
co
(
cv
x5
)
(
co
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
csg
)
)
(
cfv
(
cv
x1
)
cvsca
)
)
)
(
λ x5 .
co
cc0
c1
cicc
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
(
λ x2 .
co
(
co
(
cv
x1
)
(
cop
(
cfv
cnx
citv
)
(
cv
x2
)
)
csts
)
(
cop
(
cfv
cnx
clng
)
(
cmpt2
(
λ x3 x4 .
cfv
(
cv
x1
)
cbs
)
(
λ x3 x4 .
cfv
(
cv
x1
)
cbs
)
(
λ x3 x4 .
crab
(
λ x5 .
w3o
(
wcel
(
cv
x5
)
(
co
(
cv
x3
)
(
cv
x4
)
(
cv
x2
)
)
)
(
wcel
(
cv
x3
)
(
co
(
cv
x5
)
(
cv
x4
)
(
cv
x2
)
)
)
(
wcel
(
cv
x4
)
(
co
(
cv
x3
)
(
cv
x5
)
(
cv
x2
)
)
)
)
(
λ x5 .
cfv
(
cv
x1
)
cbs
)
)
)
)
csts
)
)
)
⟶
wceq
cee
(
cmpt
(
λ x1 .
cn
)
(
λ x1 .
co
cr
(
co
c1
(
cv
x1
)
cfz
)
cmap
)
)
⟶
wceq
cbtwn
(
ccnv
(
coprab
(
λ x1 x2 x3 .
wrex
(
λ x4 .
wa
(
w3a
(
wcel
(
cv
x1
)
(
cfv
(
cv
x4
)
cee
)
)
(
wcel
(
cv
x2
)
(
cfv
(
cv
x4
)
cee
)
)
(
wcel
(
cv
x3
)
(
cfv
(
cv
x4
)
cee
)
)
)
(
wrex
(
λ x5 .
wral
(
λ x6 .
wceq
(
cfv
(
cv
x6
)
(
cv
x3
)
)
(
co
(
co
(
co
c1
(
cv
x5
)
cmin
)
(
cfv
(
cv
x6
)
(
cv
x1
)
)
cmul
)
(
co
(
cv
x5
)
(
cfv
(
cv
x6
)
(
cv
x2
)
)
cmul
)
caddc
)
)
(
λ x6 .
co
c1
(
cv
x4
)
cfz
)
)
(
λ x5 .
co
cc0
c1
cicc
)
)
)
(
λ x4 .
cn
)
)
)
)
⟶
wceq
ccgr
(
copab
(
λ x1 x2 .
wrex
(
λ x3 .
wa
(
wa
(
wcel
(
cv
x1
)
(
cxp
(
cfv
(
cv
x3
)
cee
)
(
cfv
(
cv
x3
)
cee
)
)
)
(
wcel
(
cv
x2
)
(
cxp
(
cfv
(
cv
x3
)
cee
)
(
cfv
(
cv
x3
)
cee
)
)
)
)
(
wceq
(
csu
(
co
c1
(
cv
x3
)
cfz
)
(
λ x4 .
co
(
co
(
cfv
(
cv
x4
)
(
cfv
(
cv
x1
)
c1st
)
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x1
)
c2nd
)
)
cmin
)
c2
cexp
)
)
(
csu
(
co
c1
(
cv
x3
)
cfz
)
(
λ x4 .
co
(
co
(
cfv
(
cv
x4
)
(
cfv
(
cv
x2
)
c1st
)
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x2
)
c2nd
)
)
cmin
)
c2
cexp
)
)
)
)
(
λ x3 .
cn
)
)
)
⟶
wceq
ceeng
(
cmpt
(
λ x1 .
cn
)
(
λ x1 .
cun
(
cpr
(
cop
(
cfv
cnx
cbs
)
(
cfv
(
cv
x1
)
cee
)
)
(
cop
(
cfv
cnx
cds
)
(
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
csu
(
co
c1
(
cv
x1
)
cfz
)
(
λ x4 .
co
(
co
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x4
)
(
cv
x3
)
)
cmin
)
c2
cexp
)
)
)
)
)
(
cpr
(
cop
(
cfv
cnx
citv
)
(
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
crab
(
λ x4 .
wbr
(
cv
x4
)
(
cop
(
cv
x2
)
(
cv
x3
)
)
cbtwn
)
(
λ x4 .
cfv
(
cv
x1
)
cee
)
)
)
)
(
cop
(
cfv
cnx
clng
)
(
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
cdif
(
cfv
(
cv
x1
)
cee
)
(
csn
(
cv
x2
)
)
)
(
λ x2 x3 .
crab
(
λ x4 .
w3o
(
wbr
(
cv
x4
)
(
cop
(
cv
x2
)
(
cv
x3
)
)
cbtwn
)
(
wbr
(
cv
x2
)
(
cop
(
cv
x4
)
(
cv
x3
)
)
cbtwn
)
(
wbr
(
cv
x3
)
(
cop
(
cv
x2
)
(
cv
x4
)
)
cbtwn
)
)
(
λ x4 .
cfv
(
cv
x1
)
cee
)
)
)
)
)
)
)
⟶
wceq
cedgf
(
cslot
(
cdc
c1
c8
)
)
⟶
wceq
cvtx
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cif
(
wcel
(
cv
x1
)
(
cxp
cvv
cvv
)
)
(
cfv
(
cv
x1
)
c1st
)
(
cfv
(
cv
x1
)
cbs
)
)
)
⟶
wceq
ciedg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cif
(
wcel
(
cv
x1
)
(
cxp
cvv
cvv
)
)
(
cfv
(
cv
x1
)
c2nd
)
(
cfv
(
cv
x1
)
cedgf
)
)
)
⟶
wceq
cedg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crn
(
cfv
(
cv
x1
)
ciedg
)
)
)
⟶
x0
)
⟶
x0
Theorem
df_rag
:
wceq
crag
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
crab
(
λ x1 .
wa
(
wceq
(
cfv
(
cv
x1
)
chash
)
c3
)
(
wceq
(
co
(
cfv
cc0
(
cv
x1
)
)
(
cfv
c2
(
cv
x1
)
)
(
cfv
(
cv
x0
)
cds
)
)
(
co
(
cfv
cc0
(
cv
x1
)
)
(
cfv
(
cfv
c2
(
cv
x1
)
)
(
cfv
(
cfv
c1
(
cv
x1
)
)
(
cfv
(
cv
x0
)
cmir
)
)
)
(
cfv
(
cv
x0
)
cds
)
)
)
)
(
λ x1 .
cword
(
cfv
(
cv
x0
)
cbs
)
)
)
)
(proof)
Theorem
df_perpg
:
wceq
cperpg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
(
crn
(
cfv
(
cv
x0
)
clng
)
)
)
(
wcel
(
cv
x2
)
(
crn
(
cfv
(
cv
x0
)
clng
)
)
)
)
(
wrex
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wcel
(
cs3
(
cv
x4
)
(
cv
x3
)
(
cv
x5
)
)
(
cfv
(
cv
x0
)
crag
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cv
x1
)
)
(
λ x3 .
cin
(
cv
x1
)
(
cv
x2
)
)
)
)
)
)
(proof)
Theorem
df_hpg
:
wceq
chpg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cmpt
(
λ x1 .
crn
(
cfv
(
cv
x0
)
clng
)
)
(
λ x1 .
copab
(
λ x2 x3 .
wsbc
(
λ x4 .
wsbc
(
λ x5 .
wrex
(
λ x6 .
wa
(
wa
(
wa
(
wcel
(
cv
x2
)
(
cdif
(
cv
x4
)
(
cv
x1
)
)
)
(
wcel
(
cv
x6
)
(
cdif
(
cv
x4
)
(
cv
x1
)
)
)
)
(
wrex
(
λ x7 .
wcel
(
cv
x7
)
(
co
(
cv
x2
)
(
cv
x6
)
(
cv
x5
)
)
)
(
λ x7 .
cv
x1
)
)
)
(
wa
(
wa
(
wcel
(
cv
x3
)
(
cdif
(
cv
x4
)
(
cv
x1
)
)
)
(
wcel
(
cv
x6
)
(
cdif
(
cv
x4
)
(
cv
x1
)
)
)
)
(
wrex
(
λ x7 .
wcel
(
cv
x7
)
(
co
(
cv
x3
)
(
cv
x6
)
(
cv
x5
)
)
)
(
λ x7 .
cv
x1
)
)
)
)
(
λ x6 .
cv
x4
)
)
(
cfv
(
cv
x0
)
citv
)
)
(
cfv
(
cv
x0
)
cbs
)
)
)
)
)
(proof)
Theorem
df_mid
:
wceq
cmid
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cmpt2
(
λ x1 x2 .
cfv
(
cv
x0
)
cbs
)
(
λ x1 x2 .
cfv
(
cv
x0
)
cbs
)
(
λ x1 x2 .
crio
(
λ x3 .
wceq
(
cv
x2
)
(
cfv
(
cv
x1
)
(
cfv
(
cv
x3
)
(
cfv
(
cv
x0
)
cmir
)
)
)
)
(
λ x3 .
cfv
(
cv
x0
)
cbs
)
)
)
)
(proof)
Theorem
df_lmi
:
wceq
clmi
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cmpt
(
λ x1 .
crn
(
cfv
(
cv
x0
)
clng
)
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x0
)
cbs
)
(
λ x2 .
crio
(
λ x3 .
wa
(
wcel
(
co
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x0
)
cmid
)
)
(
cv
x1
)
)
(
wo
(
wbr
(
cv
x1
)
(
co
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x0
)
clng
)
)
(
cfv
(
cv
x0
)
cperpg
)
)
(
wceq
(
cv
x2
)
(
cv
x3
)
)
)
)
(
λ x3 .
cfv
(
cv
x0
)
cbs
)
)
)
)
)
(proof)
Theorem
df_cgra
:
wceq
ccgra
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
copab
(
λ x1 x2 .
wsbc
(
λ x3 .
wsbc
(
λ x4 .
wa
(
wa
(
wcel
(
cv
x1
)
(
co
(
cv
x3
)
(
co
cc0
c3
cfzo
)
cmap
)
)
(
wcel
(
cv
x2
)
(
co
(
cv
x3
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(
wrex
(
λ x5 .
wrex
(
λ x6 .
w3a
(
wbr
(
cv
x1
)
(
cs3
(
cv
x5
)
(
cfv
c1
(
cv
x2
)
)
(
cv
x6
)
)
(
cfv
(
cv
x0
)
ccgrg
)
)
(
wbr
(
cv
x5
)
(
cfv
cc0
(
cv
x2
)
)
(
cfv
(
cfv
c1
(
cv
x2
)
)
(
cv
x4
)
)
)
(
wbr
(
cv
x6
)
(
cfv
c2
(
cv
x2
)
)
(
cfv
(
cfv
c1
(
cv
x2
)
)
(
cv
x4
)
)
)
)
(
λ x6 .
cv
x3
)
)
(
λ x5 .
cv
x3
)
)
)
(
cfv
(
cv
x0
)
chlg
)
)
(
cfv
(
cv
x0
)
cbs
)
)
)
)
(proof)
Theorem
df_inag
:
wceq
cinag
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
(
cfv
(
cv
x0
)
cbs
)
)
(
wcel
(
cv
x2
)
(
co
(
cfv
(
cv
x0
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(
wa
(
w3a
(
wne
(
cfv
cc0
(
cv
x2
)
)
(
cfv
c1
(
cv
x2
)
)
)
(
wne
(
cfv
c2
(
cv
x2
)
)
(
cfv
c1
(
cv
x2
)
)
)
(
wne
(
cv
x1
)
(
cfv
c1
(
cv
x2
)
)
)
)
(
wrex
(
λ x3 .
wa
(
wcel
(
cv
x3
)
(
co
(
cfv
cc0
(
cv
x2
)
)
(
cfv
c2
(
cv
x2
)
)
(
cfv
(
cv
x0
)
citv
)
)
)
(
wo
(
wceq
(
cv
x3
)
(
cfv
c1
(
cv
x2
)
)
)
(
wbr
(
cv
x3
)
(
cv
x1
)
(
cfv
(
cfv
c1
(
cv
x2
)
)
(
cfv
(
cv
x0
)
chlg
)
)
)
)
)
(
λ x3 .
cfv
(
cv
x0
)
cbs
)
)
)
)
)
)
(proof)
Theorem
df_leag
:
wceq
cleag
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
(
co
(
cfv
(
cv
x0
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
(
wcel
(
cv
x2
)
(
co
(
cfv
(
cv
x0
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(
wrex
(
λ x3 .
wa
(
wbr
(
cv
x3
)
(
cs3
(
cfv
cc0
(
cv
x2
)
)
(
cfv
c1
(
cv
x2
)
)
(
cfv
c2
(
cv
x2
)
)
)
(
cfv
(
cv
x0
)
cinag
)
)
(
wbr
(
cs3
(
cfv
cc0
(
cv
x1
)
)
(
cfv
c1
(
cv
x1
)
)
(
cfv
c2
(
cv
x1
)
)
)
(
cs3
(
cfv
cc0
(
cv
x2
)
)
(
cfv
c1
(
cv
x2
)
)
(
cv
x3
)
)
(
cfv
(
cv
x0
)
ccgra
)
)
)
(
λ x3 .
cfv
(
cv
x0
)
cbs
)
)
)
)
)
(proof)
Theorem
df_eqlg
:
wceq
ceqlg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
crab
(
λ x1 .
wbr
(
cv
x1
)
(
cs3
(
cfv
c1
(
cv
x1
)
)
(
cfv
c2
(
cv
x1
)
)
(
cfv
cc0
(
cv
x1
)
)
)
(
cfv
(
cv
x0
)
ccgrg
)
)
(
λ x1 .
co
(
cfv
(
cv
x0
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(proof)
Theorem
df_ttg
:
wceq
cttg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
csb
(
cmpt2
(
λ x1 x2 .
cfv
(
cv
x0
)
cbs
)
(
λ x1 x2 .
cfv
(
cv
x0
)
cbs
)
(
λ x1 x2 .
crab
(
λ x3 .
wrex
(
λ x4 .
wceq
(
co
(
cv
x3
)
(
cv
x1
)
(
cfv
(
cv
x0
)
csg
)
)
(
co
(
cv
x4
)
(
co
(
cv
x2
)
(
cv
x1
)
(
cfv
(
cv
x0
)
csg
)
)
(
cfv
(
cv
x0
)
cvsca
)
)
)
(
λ x4 .
co
cc0
c1
cicc
)
)
(
λ x3 .
cfv
(
cv
x0
)
cbs
)
)
)
(
λ x1 .
co
(
co
(
cv
x0
)
(
cop
(
cfv
cnx
citv
)
(
cv
x1
)
)
csts
)
(
cop
(
cfv
cnx
clng
)
(
cmpt2
(
λ x2 x3 .
cfv
(
cv
x0
)
cbs
)
(
λ x2 x3 .
cfv
(
cv
x0
)
cbs
)
(
λ x2 x3 .
crab
(
λ x4 .
w3o
(
wcel
(
cv
x4
)
(
co
(
cv
x2
)
(
cv
x3
)
(
cv
x1
)
)
)
(
wcel
(
cv
x2
)
(
co
(
cv
x4
)
(
cv
x3
)
(
cv
x1
)
)
)
(
wcel
(
cv
x3
)
(
co
(
cv
x2
)
(
cv
x4
)
(
cv
x1
)
)
)
)
(
λ x4 .
cfv
(
cv
x0
)
cbs
)
)
)
)
csts
)
)
)
(proof)
Theorem
df_ee
:
wceq
cee
(
cmpt
(
λ x0 .
cn
)
(
λ x0 .
co
cr
(
co
c1
(
cv
x0
)
cfz
)
cmap
)
)
(proof)
Theorem
df_btwn
:
wceq
cbtwn
(
ccnv
(
coprab
(
λ x0 x1 x2 .
wrex
(
λ x3 .
wa
(
w3a
(
wcel
(
cv
x0
)
(
cfv
(
cv
x3
)
cee
)
)
(
wcel
(
cv
x1
)
(
cfv
(
cv
x3
)
cee
)
)
(
wcel
(
cv
x2
)
(
cfv
(
cv
x3
)
cee
)
)
)
(
wrex
(
λ x4 .
wral
(
λ x5 .
wceq
(
cfv
(
cv
x5
)
(
cv
x2
)
)
(
co
(
co
(
co
c1
(
cv
x4
)
cmin
)
(
cfv
(
cv
x5
)
(
cv
x0
)
)
cmul
)
(
co
(
cv
x4
)
(
cfv
(
cv
x5
)
(
cv
x1
)
)
cmul
)
caddc
)
)
(
λ x5 .
co
c1
(
cv
x3
)
cfz
)
)
(
λ x4 .
co
cc0
c1
cicc
)
)
)
(
λ x3 .
cn
)
)
)
)
(proof)
Theorem
df_cgr
:
wceq
ccgr
(
copab
(
λ x0 x1 .
wrex
(
λ x2 .
wa
(
wa
(
wcel
(
cv
x0
)
(
cxp
(
cfv
(
cv
x2
)
cee
)
(
cfv
(
cv
x2
)
cee
)
)
)
(
wcel
(
cv
x1
)
(
cxp
(
cfv
(
cv
x2
)
cee
)
(
cfv
(
cv
x2
)
cee
)
)
)
)
(
wceq
(
csu
(
co
c1
(
cv
x2
)
cfz
)
(
λ x3 .
co
(
co
(
cfv
(
cv
x3
)
(
cfv
(
cv
x0
)
c1st
)
)
(
cfv
(
cv
x3
)
(
cfv
(
cv
x0
)
c2nd
)
)
cmin
)
c2
cexp
)
)
(
csu
(
co
c1
(
cv
x2
)
cfz
)
(
λ x3 .
co
(
co
(
cfv
(
cv
x3
)
(
cfv
(
cv
x1
)
c1st
)
)
(
cfv
(
cv
x3
)
(
cfv
(
cv
x1
)
c2nd
)
)
cmin
)
c2
cexp
)
)
)
)
(
λ x2 .
cn
)
)
)
(proof)
Theorem
df_eeng
:
wceq
ceeng
(
cmpt
(
λ x0 .
cn
)
(
λ x0 .
cun
(
cpr
(
cop
(
cfv
cnx
cbs
)
(
cfv
(
cv
x0
)
cee
)
)
(
cop
(
cfv
cnx
cds
)
(
cmpt2
(
λ x1 x2 .
cfv
(
cv
x0
)
cee
)
(
λ x1 x2 .
cfv
(
cv
x0
)
cee
)
(
λ x1 x2 .
csu
(
co
c1
(
cv
x0
)
cfz
)
(
λ x3 .
co
(
co
(
cfv
(
cv
x3
)
(
cv
x1
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
cmin
)
c2
cexp
)
)
)
)
)
(
cpr
(
cop
(
cfv
cnx
citv
)
(
cmpt2
(
λ x1 x2 .
cfv
(
cv
x0
)
cee
)
(
λ x1 x2 .
cfv
(
cv
x0
)
cee
)
(
λ x1 x2 .
crab
(
λ x3 .
wbr
(
cv
x3
)
(
cop
(
cv
x1
)
(
cv
x2
)
)
cbtwn
)
(
λ x3 .
cfv
(
cv
x0
)
cee
)
)
)
)
(
cop
(
cfv
cnx
clng
)
(
cmpt2
(
λ x1 x2 .
cfv
(
cv
x0
)
cee
)
(
λ x1 x2 .
cdif
(
cfv
(
cv
x0
)
cee
)
(
csn
(
cv
x1
)
)
)
(
λ x1 x2 .
crab
(
λ x3 .
w3o
(
wbr
(
cv
x3
)
(
cop
(
cv
x1
)
(
cv
x2
)
)
cbtwn
)
(
wbr
(
cv
x1
)
(
cop
(
cv
x3
)
(
cv
x2
)
)
cbtwn
)
(
wbr
(
cv
x2
)
(
cop
(
cv
x1
)
(
cv
x3
)
)
cbtwn
)
)
(
λ x3 .
cfv
(
cv
x0
)
cee
)
)
)
)
)
)
)
(proof)
Theorem
df_edgf
:
wceq
cedgf
(
cslot
(
cdc
c1
c8
)
)
(proof)
Theorem
df_vtx
:
wceq
cvtx
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cif
(
wcel
(
cv
x0
)
(
cxp
cvv
cvv
)
)
(
cfv
(
cv
x0
)
c1st
)
(
cfv
(
cv
x0
)
cbs
)
)
)
(proof)
Theorem
df_iedg
:
wceq
ciedg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cif
(
wcel
(
cv
x0
)
(
cxp
cvv
cvv
)
)
(
cfv
(
cv
x0
)
c2nd
)
(
cfv
(
cv
x0
)
cedgf
)
)
)
(proof)
Theorem
df_edg
:
wceq
cedg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
crn
(
cfv
(
cv
x0
)
ciedg
)
)
)
(proof)