Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr4bV..
/
28367..
PUWLF..
/
468cb..
vout
Pr4bV..
/
83bd5..
0.10 bars
TMF7d..
/
c458b..
ownership of
7f293..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMPyg..
/
744ab..
ownership of
67138..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMU91..
/
89a9e..
ownership of
5927b..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMP1z..
/
707e0..
ownership of
7f600..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMMfg..
/
f0221..
ownership of
4ada7..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMXQH..
/
941eb..
ownership of
621fe..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMXvR..
/
6e868..
ownership of
ffb27..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMMTQ..
/
28c02..
ownership of
d9a31..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMFJu..
/
e021c..
ownership of
0b148..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMNHU..
/
15c41..
ownership of
577c5..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMHk5..
/
c3e10..
ownership of
3d4dd..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMF5W..
/
66b99..
ownership of
837c4..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMRTr..
/
ace12..
ownership of
13692..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMWhi..
/
7b5e5..
ownership of
625e4..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMRkC..
/
612be..
ownership of
3973a..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMXmA..
/
4530e..
ownership of
ed56f..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMLGs..
/
4578c..
ownership of
1824f..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMXxA..
/
b22a4..
ownership of
fdc76..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMdYU..
/
a6ada..
ownership of
7af19..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMaQa..
/
ddcc9..
ownership of
9f963..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMNVf..
/
89a53..
ownership of
854e7..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMJej..
/
87c10..
ownership of
f4e6e..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMKZn..
/
b4701..
ownership of
d2e87..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMRWX..
/
b688b..
ownership of
b21b2..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMa6i..
/
70ace..
ownership of
4a691..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMFZF..
/
1f4ce..
ownership of
05613..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMUiW..
/
3b3d4..
ownership of
6c047..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMNHg..
/
3faab..
ownership of
fef60..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMa2Q..
/
a775d..
ownership of
d0dcf..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMciu..
/
74ae1..
ownership of
f1ff8..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMGg2..
/
b8127..
ownership of
6c5dd..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMGdW..
/
4536b..
ownership of
e634a..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMaA6..
/
2f04f..
ownership of
772b2..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMSJb..
/
f0014..
ownership of
0db48..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMdyY..
/
b92d2..
ownership of
79d56..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
TMNa2..
/
f353c..
ownership of
96beb..
as prop with payaddr
PrCmT..
rightscost 0.00 controlledby
PrCmT..
upto 0
PUfy1..
/
dc74c..
doc published by
PrCmT..
Known
df_odz__df_phi__df_pc__df_gz__df_vdwap__df_vdwmc__df_vdwpc__df_ram__df_prmo__df_struct__df_ndx__df_slot__df_base__df_sets__df_ress__df_plusg__df_mulr__df_starv
:
∀ x0 : ο .
(
wceq
codz
(
cmpt
(
λ x1 .
cn
)
(
λ x1 .
cmpt
(
λ x2 .
crab
(
λ x3 .
wceq
(
co
(
cv
x3
)
(
cv
x1
)
cgcd
)
c1
)
(
λ x3 .
cz
)
)
(
λ x2 .
cinf
(
crab
(
λ x3 .
wbr
(
cv
x1
)
(
co
(
co
(
cv
x2
)
(
cv
x3
)
cexp
)
c1
cmin
)
cdvds
)
(
λ x3 .
cn
)
)
cr
clt
)
)
)
⟶
wceq
cphi
(
cmpt
(
λ x1 .
cn
)
(
λ x1 .
cfv
(
crab
(
λ x2 .
wceq
(
co
(
cv
x2
)
(
cv
x1
)
cgcd
)
c1
)
(
λ x2 .
co
c1
(
cv
x1
)
cfz
)
)
chash
)
)
⟶
wceq
cpc
(
cmpt2
(
λ x1 x2 .
cprime
)
(
λ x1 x2 .
cq
)
(
λ x1 x2 .
cif
(
wceq
(
cv
x2
)
cc0
)
cpnf
(
cio
(
λ x3 .
wrex
(
λ x4 .
wrex
(
λ x5 .
wa
(
wceq
(
cv
x2
)
(
co
(
cv
x4
)
(
cv
x5
)
cdiv
)
)
(
wceq
(
cv
x3
)
(
co
(
csup
(
crab
(
λ x6 .
wbr
(
co
(
cv
x1
)
(
cv
x6
)
cexp
)
(
cv
x4
)
cdvds
)
(
λ x6 .
cn0
)
)
cr
clt
)
(
csup
(
crab
(
λ x6 .
wbr
(
co
(
cv
x1
)
(
cv
x6
)
cexp
)
(
cv
x5
)
cdvds
)
(
λ x6 .
cn0
)
)
cr
clt
)
cmin
)
)
)
(
λ x5 .
cn
)
)
(
λ x4 .
cz
)
)
)
)
)
⟶
wceq
cgz
(
crab
(
λ x1 .
wa
(
wcel
(
cfv
(
cv
x1
)
cre
)
cz
)
(
wcel
(
cfv
(
cv
x1
)
cim
)
cz
)
)
(
λ x1 .
cc
)
)
⟶
wceq
cvdwa
(
cmpt
(
λ x1 .
cn0
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cn
)
(
λ x2 x3 .
cn
)
(
λ x2 x3 .
crn
(
cmpt
(
λ x4 .
co
cc0
(
co
(
cv
x1
)
c1
cmin
)
cfz
)
(
λ x4 .
co
(
cv
x2
)
(
co
(
cv
x4
)
(
cv
x3
)
cmul
)
caddc
)
)
)
)
)
⟶
wceq
cvdwm
(
copab
(
λ x1 x2 .
wex
(
λ x3 .
wne
(
cin
(
crn
(
cfv
(
cv
x1
)
cvdwa
)
)
(
cpw
(
cima
(
ccnv
(
cv
x2
)
)
(
csn
(
cv
x3
)
)
)
)
)
c0
)
)
)
⟶
wceq
cvdwp
(
coprab
(
λ x1 x2 x3 .
wrex
(
λ x4 .
wrex
(
λ x5 .
wa
(
wral
(
λ x6 .
wss
(
co
(
co
(
cv
x4
)
(
cfv
(
cv
x6
)
(
cv
x5
)
)
caddc
)
(
cfv
(
cv
x6
)
(
cv
x5
)
)
(
cfv
(
cv
x2
)
cvdwa
)
)
(
cima
(
ccnv
(
cv
x3
)
)
(
csn
(
cfv
(
co
(
cv
x4
)
(
cfv
(
cv
x6
)
(
cv
x5
)
)
caddc
)
(
cv
x3
)
)
)
)
)
(
λ x6 .
co
c1
(
cv
x1
)
cfz
)
)
(
wceq
(
cfv
(
crn
(
cmpt
(
λ x6 .
co
c1
(
cv
x1
)
cfz
)
(
λ x6 .
cfv
(
co
(
cv
x4
)
(
cfv
(
cv
x6
)
(
cv
x5
)
)
caddc
)
(
cv
x3
)
)
)
)
chash
)
(
cv
x1
)
)
)
(
λ x5 .
co
cn
(
co
c1
(
cv
x1
)
cfz
)
cmap
)
)
(
λ x4 .
cn
)
)
)
⟶
wceq
cram
(
cmpt2
(
λ x1 x2 .
cn0
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cinf
(
crab
(
λ x3 .
∀ x4 .
wbr
(
cv
x3
)
(
cfv
(
cv
x4
)
chash
)
cle
⟶
wral
(
λ x5 .
wrex
(
λ x6 .
wrex
(
λ x7 .
wa
(
wbr
(
cfv
(
cv
x6
)
(
cv
x2
)
)
(
cfv
(
cv
x7
)
chash
)
cle
)
(
wral
(
λ x8 .
wceq
(
cfv
(
cv
x8
)
chash
)
(
cv
x1
)
⟶
wceq
(
cfv
(
cv
x8
)
(
cv
x5
)
)
(
cv
x6
)
)
(
λ x8 .
cpw
(
cv
x7
)
)
)
)
(
λ x7 .
cpw
(
cv
x4
)
)
)
(
λ x6 .
cdm
(
cv
x2
)
)
)
(
λ x5 .
co
(
cdm
(
cv
x2
)
)
(
crab
(
λ x6 .
wceq
(
cfv
(
cv
x6
)
chash
)
(
cv
x1
)
)
(
λ x6 .
cpw
(
cv
x4
)
)
)
cmap
)
)
(
λ x3 .
cn0
)
)
cxr
clt
)
)
⟶
wceq
cprmo
(
cmpt
(
λ x1 .
cn0
)
(
λ x1 .
cprod
(
λ x2 .
co
c1
(
cv
x1
)
cfz
)
(
λ x2 .
cif
(
wcel
(
cv
x2
)
cprime
)
(
cv
x2
)
c1
)
)
)
⟶
wceq
cstr
(
copab
(
λ x1 x2 .
w3a
(
wcel
(
cv
x2
)
(
cin
cle
(
cxp
cn
cn
)
)
)
(
wfun
(
cdif
(
cv
x1
)
(
csn
c0
)
)
)
(
wss
(
cdm
(
cv
x1
)
)
(
cfv
(
cv
x2
)
cfz
)
)
)
)
⟶
wceq
cnx
(
cres
cid
cn
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cslot
x1
)
(
cmpt
(
λ x2 .
cvv
)
(
λ x2 .
cfv
x1
(
cv
x2
)
)
)
)
⟶
wceq
cbs
(
cslot
c1
)
⟶
wceq
csts
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cun
(
cres
(
cv
x1
)
(
cdif
cvv
(
cdm
(
csn
(
cv
x2
)
)
)
)
)
(
csn
(
cv
x2
)
)
)
)
⟶
wceq
cress
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cif
(
wss
(
cfv
(
cv
x1
)
cbs
)
(
cv
x2
)
)
(
cv
x1
)
(
co
(
cv
x1
)
(
cop
(
cfv
cnx
cbs
)
(
cin
(
cv
x2
)
(
cfv
(
cv
x1
)
cbs
)
)
)
csts
)
)
)
⟶
wceq
cplusg
(
cslot
c2
)
⟶
wceq
cmulr
(
cslot
c3
)
⟶
wceq
cstv
(
cslot
c4
)
⟶
x0
)
⟶
x0
Theorem
df_odz
:
wceq
codz
(
cmpt
(
λ x0 .
cn
)
(
λ x0 .
cmpt
(
λ x1 .
crab
(
λ x2 .
wceq
(
co
(
cv
x2
)
(
cv
x0
)
cgcd
)
c1
)
(
λ x2 .
cz
)
)
(
λ x1 .
cinf
(
crab
(
λ x2 .
wbr
(
cv
x0
)
(
co
(
co
(
cv
x1
)
(
cv
x2
)
cexp
)
c1
cmin
)
cdvds
)
(
λ x2 .
cn
)
)
cr
clt
)
)
)
(proof)
Theorem
df_phi
:
wceq
cphi
(
cmpt
(
λ x0 .
cn
)
(
λ x0 .
cfv
(
crab
(
λ x1 .
wceq
(
co
(
cv
x1
)
(
cv
x0
)
cgcd
)
c1
)
(
λ x1 .
co
c1
(
cv
x0
)
cfz
)
)
chash
)
)
(proof)
Theorem
df_pc
:
wceq
cpc
(
cmpt2
(
λ x0 x1 .
cprime
)
(
λ x0 x1 .
cq
)
(
λ x0 x1 .
cif
(
wceq
(
cv
x1
)
cc0
)
cpnf
(
cio
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wa
(
wceq
(
cv
x1
)
(
co
(
cv
x3
)
(
cv
x4
)
cdiv
)
)
(
wceq
(
cv
x2
)
(
co
(
csup
(
crab
(
λ x5 .
wbr
(
co
(
cv
x0
)
(
cv
x5
)
cexp
)
(
cv
x3
)
cdvds
)
(
λ x5 .
cn0
)
)
cr
clt
)
(
csup
(
crab
(
λ x5 .
wbr
(
co
(
cv
x0
)
(
cv
x5
)
cexp
)
(
cv
x4
)
cdvds
)
(
λ x5 .
cn0
)
)
cr
clt
)
cmin
)
)
)
(
λ x4 .
cn
)
)
(
λ x3 .
cz
)
)
)
)
)
(proof)
Theorem
df_gz
:
wceq
cgz
(
crab
(
λ x0 .
wa
(
wcel
(
cfv
(
cv
x0
)
cre
)
cz
)
(
wcel
(
cfv
(
cv
x0
)
cim
)
cz
)
)
(
λ x0 .
cc
)
)
(proof)
Theorem
df_vdwap
:
wceq
cvdwa
(
cmpt
(
λ x0 .
cn0
)
(
λ x0 .
cmpt2
(
λ x1 x2 .
cn
)
(
λ x1 x2 .
cn
)
(
λ x1 x2 .
crn
(
cmpt
(
λ x3 .
co
cc0
(
co
(
cv
x0
)
c1
cmin
)
cfz
)
(
λ x3 .
co
(
cv
x1
)
(
co
(
cv
x3
)
(
cv
x2
)
cmul
)
caddc
)
)
)
)
)
(proof)
Theorem
df_vdwmc
:
wceq
cvdwm
(
copab
(
λ x0 x1 .
wex
(
λ x2 .
wne
(
cin
(
crn
(
cfv
(
cv
x0
)
cvdwa
)
)
(
cpw
(
cima
(
ccnv
(
cv
x1
)
)
(
csn
(
cv
x2
)
)
)
)
)
c0
)
)
)
(proof)
Theorem
df_vdwpc
:
wceq
cvdwp
(
coprab
(
λ x0 x1 x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wa
(
wral
(
λ x5 .
wss
(
co
(
co
(
cv
x3
)
(
cfv
(
cv
x5
)
(
cv
x4
)
)
caddc
)
(
cfv
(
cv
x5
)
(
cv
x4
)
)
(
cfv
(
cv
x1
)
cvdwa
)
)
(
cima
(
ccnv
(
cv
x2
)
)
(
csn
(
cfv
(
co
(
cv
x3
)
(
cfv
(
cv
x5
)
(
cv
x4
)
)
caddc
)
(
cv
x2
)
)
)
)
)
(
λ x5 .
co
c1
(
cv
x0
)
cfz
)
)
(
wceq
(
cfv
(
crn
(
cmpt
(
λ x5 .
co
c1
(
cv
x0
)
cfz
)
(
λ x5 .
cfv
(
co
(
cv
x3
)
(
cfv
(
cv
x5
)
(
cv
x4
)
)
caddc
)
(
cv
x2
)
)
)
)
chash
)
(
cv
x0
)
)
)
(
λ x4 .
co
cn
(
co
c1
(
cv
x0
)
cfz
)
cmap
)
)
(
λ x3 .
cn
)
)
)
(proof)
Theorem
df_ram
:
wceq
cram
(
cmpt2
(
λ x0 x1 .
cn0
)
(
λ x0 x1 .
cvv
)
(
λ x0 x1 .
cinf
(
crab
(
λ x2 .
∀ x3 .
wbr
(
cv
x2
)
(
cfv
(
cv
x3
)
chash
)
cle
⟶
wral
(
λ x4 .
wrex
(
λ x5 .
wrex
(
λ x6 .
wa
(
wbr
(
cfv
(
cv
x5
)
(
cv
x1
)
)
(
cfv
(
cv
x6
)
chash
)
cle
)
(
wral
(
λ x7 .
wceq
(
cfv
(
cv
x7
)
chash
)
(
cv
x0
)
⟶
wceq
(
cfv
(
cv
x7
)
(
cv
x4
)
)
(
cv
x5
)
)
(
λ x7 .
cpw
(
cv
x6
)
)
)
)
(
λ x6 .
cpw
(
cv
x3
)
)
)
(
λ x5 .
cdm
(
cv
x1
)
)
)
(
λ x4 .
co
(
cdm
(
cv
x1
)
)
(
crab
(
λ x5 .
wceq
(
cfv
(
cv
x5
)
chash
)
(
cv
x0
)
)
(
λ x5 .
cpw
(
cv
x3
)
)
)
cmap
)
)
(
λ x2 .
cn0
)
)
cxr
clt
)
)
(proof)
Theorem
df_prmo
:
wceq
cprmo
(
cmpt
(
λ x0 .
cn0
)
(
λ x0 .
cprod
(
λ x1 .
co
c1
(
cv
x0
)
cfz
)
(
λ x1 .
cif
(
wcel
(
cv
x1
)
cprime
)
(
cv
x1
)
c1
)
)
)
(proof)
Theorem
df_struct
:
wceq
cstr
(
copab
(
λ x0 x1 .
w3a
(
wcel
(
cv
x1
)
(
cin
cle
(
cxp
cn
cn
)
)
)
(
wfun
(
cdif
(
cv
x0
)
(
csn
c0
)
)
)
(
wss
(
cdm
(
cv
x0
)
)
(
cfv
(
cv
x1
)
cfz
)
)
)
)
(proof)
Theorem
df_ndx
:
wceq
cnx
(
cres
cid
cn
)
(proof)
Theorem
df_slot
:
∀ x0 :
ι → ο
.
wceq
(
cslot
x0
)
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cfv
x0
(
cv
x1
)
)
)
(proof)
Theorem
df_base
:
wceq
cbs
(
cslot
c1
)
(proof)
Theorem
df_sets
:
wceq
csts
(
cmpt2
(
λ x0 x1 .
cvv
)
(
λ x0 x1 .
cvv
)
(
λ x0 x1 .
cun
(
cres
(
cv
x0
)
(
cdif
cvv
(
cdm
(
csn
(
cv
x1
)
)
)
)
)
(
csn
(
cv
x1
)
)
)
)
(proof)
Theorem
df_ress
:
wceq
cress
(
cmpt2
(
λ x0 x1 .
cvv
)
(
λ x0 x1 .
cvv
)
(
λ x0 x1 .
cif
(
wss
(
cfv
(
cv
x0
)
cbs
)
(
cv
x1
)
)
(
cv
x0
)
(
co
(
cv
x0
)
(
cop
(
cfv
cnx
cbs
)
(
cin
(
cv
x1
)
(
cfv
(
cv
x0
)
cbs
)
)
)
csts
)
)
)
(proof)
Theorem
df_plusg
:
wceq
cplusg
(
cslot
c2
)
(proof)
Theorem
df_mulr
:
wceq
cmulr
(
cslot
c3
)
(proof)
Theorem
df_starv
:
wceq
cstv
(
cslot
c4
)
(proof)