Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrK3Y..
/
5a4a4..
PUasL..
/
a337d..
vout
PrK3Y..
/
ae248..
0.10 bars
TMdKs..
/
dd943..
ownership of
45291..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMbpz..
/
236d8..
ownership of
b1fb5..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMUfC..
/
1e58a..
ownership of
c1e60..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMRDP..
/
46090..
ownership of
cac7e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZfH..
/
ef6e9..
ownership of
b0346..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMK32..
/
67d25..
ownership of
d7000..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcTn..
/
b653c..
ownership of
02fad..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVPV..
/
d5271..
ownership of
74503..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMMqL..
/
c13e0..
ownership of
1bbc4..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMUtE..
/
d05ec..
ownership of
045d2..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMFg2..
/
e863b..
ownership of
1572e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMHjJ..
/
6afe2..
ownership of
f30f8..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMXvq..
/
db2b8..
ownership of
436d8..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcQM..
/
6c0a2..
ownership of
4e530..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMWwZ..
/
d6ed1..
ownership of
6485f..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMWt3..
/
1c7f3..
ownership of
3a69b..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMdzv..
/
2c876..
ownership of
f0f1c..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcNS..
/
81c59..
ownership of
8a731..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMG8F..
/
e667e..
ownership of
4e5bf..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMN6r..
/
7807a..
ownership of
6480b..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMYCG..
/
5d3c8..
ownership of
6cacf..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQSr..
/
af3a2..
ownership of
0ac72..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMa2g..
/
8df07..
ownership of
08827..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMb4w..
/
0ad21..
ownership of
fc1af..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMbaS..
/
9bed7..
ownership of
642fd..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMFL2..
/
b792d..
ownership of
da69e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZVY..
/
1a350..
ownership of
7393f..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMNaW..
/
f2ec5..
ownership of
0cb26..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMYQc..
/
4ace6..
ownership of
3465e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPMD..
/
c5841..
ownership of
c40c9..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMULV..
/
d4fd8..
ownership of
f2f61..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMbmf..
/
409cf..
ownership of
dc0c7..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMEmq..
/
c4ced..
ownership of
77e68..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQ6C..
/
19663..
ownership of
ea85a..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMHuF..
/
2affc..
ownership of
ace13..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQyZ..
/
b202a..
ownership of
0aec9..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
PUc2k..
/
aa62f..
doc published by
PrCmT..
Known
df_mpq__df_ltpq__df_enq__df_nq__df_erq__df_plq__df_mq__df_1nq__df_rq__df_ltnq__df_np__df_1p__df_plp__df_mp__df_ltp__df_enr__df_nr__df_plr
:
∀ x0 : ο .
(
wceq
cmpq
(
cmpt2
(
λ x1 x2 .
cxp
cnpi
cnpi
)
(
λ x1 x2 .
cxp
cnpi
cnpi
)
(
λ x1 x2 .
cop
(
co
(
cfv
(
cv
x1
)
c1st
)
(
cfv
(
cv
x2
)
c1st
)
cmi
)
(
co
(
cfv
(
cv
x1
)
c2nd
)
(
cfv
(
cv
x2
)
c2nd
)
cmi
)
)
)
⟶
wceq
cltpq
(
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
(
cxp
cnpi
cnpi
)
)
(
wcel
(
cv
x2
)
(
cxp
cnpi
cnpi
)
)
)
(
wbr
(
co
(
cfv
(
cv
x1
)
c1st
)
(
cfv
(
cv
x2
)
c2nd
)
cmi
)
(
co
(
cfv
(
cv
x2
)
c1st
)
(
cfv
(
cv
x1
)
c2nd
)
cmi
)
clti
)
)
)
⟶
wceq
ceq
(
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
(
cxp
cnpi
cnpi
)
)
(
wcel
(
cv
x2
)
(
cxp
cnpi
cnpi
)
)
)
(
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wex
(
λ x6 .
wa
(
wa
(
wceq
(
cv
x1
)
(
cop
(
cv
x3
)
(
cv
x4
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
cv
x5
)
(
cv
x6
)
)
)
)
(
wceq
(
co
(
cv
x3
)
(
cv
x6
)
cmi
)
(
co
(
cv
x4
)
(
cv
x5
)
cmi
)
)
)
)
)
)
)
)
)
⟶
wceq
cnq
(
crab
(
λ x1 .
wral
(
λ x2 .
wbr
(
cv
x1
)
(
cv
x2
)
ceq
⟶
wn
(
wbr
(
cfv
(
cv
x2
)
c2nd
)
(
cfv
(
cv
x1
)
c2nd
)
clti
)
)
(
λ x2 .
cxp
cnpi
cnpi
)
)
(
λ x1 .
cxp
cnpi
cnpi
)
)
⟶
wceq
cerq
(
cin
ceq
(
cxp
(
cxp
cnpi
cnpi
)
cnq
)
)
⟶
wceq
cplq
(
cres
(
ccom
cerq
cplpq
)
(
cxp
cnq
cnq
)
)
⟶
wceq
cmq
(
cres
(
ccom
cerq
cmpq
)
(
cxp
cnq
cnq
)
)
⟶
wceq
c1q
(
cop
c1o
c1o
)
⟶
wceq
crq
(
cima
(
ccnv
cmq
)
(
csn
c1q
)
)
⟶
wceq
cltq
(
cin
cltpq
(
cxp
cnq
cnq
)
)
⟶
wceq
cnp
(
cab
(
λ x1 .
wa
(
wa
(
wpss
c0
(
cv
x1
)
)
(
wpss
(
cv
x1
)
cnq
)
)
(
wral
(
λ x2 .
wa
(
∀ x3 .
wbr
(
cv
x3
)
(
cv
x2
)
cltq
⟶
wcel
(
cv
x3
)
(
cv
x1
)
)
(
wrex
(
λ x3 .
wbr
(
cv
x2
)
(
cv
x3
)
cltq
)
(
λ x3 .
cv
x1
)
)
)
(
λ x2 .
cv
x1
)
)
)
)
⟶
wceq
c1p
(
cab
(
λ x1 .
wbr
(
cv
x1
)
c1q
cltq
)
)
⟶
wceq
cpp
(
cmpt2
(
λ x1 x2 .
cnp
)
(
λ x1 x2 .
cnp
)
(
λ x1 x2 .
cab
(
λ x3 .
wrex
(
λ x4 .
wrex
(
λ x5 .
wceq
(
cv
x3
)
(
co
(
cv
x4
)
(
cv
x5
)
cplq
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cv
x1
)
)
)
)
⟶
wceq
cmp
(
cmpt2
(
λ x1 x2 .
cnp
)
(
λ x1 x2 .
cnp
)
(
λ x1 x2 .
cab
(
λ x3 .
wrex
(
λ x4 .
wrex
(
λ x5 .
wceq
(
cv
x3
)
(
co
(
cv
x4
)
(
cv
x5
)
cmq
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cv
x1
)
)
)
)
⟶
wceq
cltp
(
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
cnp
)
(
wcel
(
cv
x2
)
cnp
)
)
(
wpss
(
cv
x1
)
(
cv
x2
)
)
)
)
⟶
wceq
cer
(
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
(
cxp
cnp
cnp
)
)
(
wcel
(
cv
x2
)
(
cxp
cnp
cnp
)
)
)
(
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wex
(
λ x6 .
wa
(
wa
(
wceq
(
cv
x1
)
(
cop
(
cv
x3
)
(
cv
x4
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
cv
x5
)
(
cv
x6
)
)
)
)
(
wceq
(
co
(
cv
x3
)
(
cv
x6
)
cpp
)
(
co
(
cv
x4
)
(
cv
x5
)
cpp
)
)
)
)
)
)
)
)
)
⟶
wceq
cnr
(
cqs
(
cxp
cnp
cnp
)
cer
)
⟶
wceq
cplr
(
coprab
(
λ x1 x2 x3 .
wa
(
wa
(
wcel
(
cv
x1
)
cnr
)
(
wcel
(
cv
x2
)
cnr
)
)
(
wex
(
λ x4 .
wex
(
λ x5 .
wex
(
λ x6 .
wex
(
λ x7 .
wa
(
wa
(
wceq
(
cv
x1
)
(
cec
(
cop
(
cv
x4
)
(
cv
x5
)
)
cer
)
)
(
wceq
(
cv
x2
)
(
cec
(
cop
(
cv
x6
)
(
cv
x7
)
)
cer
)
)
)
(
wceq
(
cv
x3
)
(
cec
(
cop
(
co
(
cv
x4
)
(
cv
x6
)
cpp
)
(
co
(
cv
x5
)
(
cv
x7
)
cpp
)
)
cer
)
)
)
)
)
)
)
)
)
⟶
x0
)
⟶
x0
Theorem
df_mpq
:
wceq
cmpq
(
cmpt2
(
λ x0 x1 .
cxp
cnpi
cnpi
)
(
λ x0 x1 .
cxp
cnpi
cnpi
)
(
λ x0 x1 .
cop
(
co
(
cfv
(
cv
x0
)
c1st
)
(
cfv
(
cv
x1
)
c1st
)
cmi
)
(
co
(
cfv
(
cv
x0
)
c2nd
)
(
cfv
(
cv
x1
)
c2nd
)
cmi
)
)
)
(proof)
Theorem
df_ltpq
:
wceq
cltpq
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
(
cxp
cnpi
cnpi
)
)
(
wcel
(
cv
x1
)
(
cxp
cnpi
cnpi
)
)
)
(
wbr
(
co
(
cfv
(
cv
x0
)
c1st
)
(
cfv
(
cv
x1
)
c2nd
)
cmi
)
(
co
(
cfv
(
cv
x1
)
c1st
)
(
cfv
(
cv
x0
)
c2nd
)
cmi
)
clti
)
)
)
(proof)
Theorem
df_enq
:
wceq
ceq
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
(
cxp
cnpi
cnpi
)
)
(
wcel
(
cv
x1
)
(
cxp
cnpi
cnpi
)
)
)
(
wex
(
λ x2 .
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wa
(
wa
(
wceq
(
cv
x0
)
(
cop
(
cv
x2
)
(
cv
x3
)
)
)
(
wceq
(
cv
x1
)
(
cop
(
cv
x4
)
(
cv
x5
)
)
)
)
(
wceq
(
co
(
cv
x2
)
(
cv
x5
)
cmi
)
(
co
(
cv
x3
)
(
cv
x4
)
cmi
)
)
)
)
)
)
)
)
)
(proof)
Theorem
df_nq
:
wceq
cnq
(
crab
(
λ x0 .
wral
(
λ x1 .
wbr
(
cv
x0
)
(
cv
x1
)
ceq
⟶
wn
(
wbr
(
cfv
(
cv
x1
)
c2nd
)
(
cfv
(
cv
x0
)
c2nd
)
clti
)
)
(
λ x1 .
cxp
cnpi
cnpi
)
)
(
λ x0 .
cxp
cnpi
cnpi
)
)
(proof)
Theorem
df_erq
:
wceq
cerq
(
cin
ceq
(
cxp
(
cxp
cnpi
cnpi
)
cnq
)
)
(proof)
Theorem
df_plq
:
wceq
cplq
(
cres
(
ccom
cerq
cplpq
)
(
cxp
cnq
cnq
)
)
(proof)
Theorem
df_mq
:
wceq
cmq
(
cres
(
ccom
cerq
cmpq
)
(
cxp
cnq
cnq
)
)
(proof)
Theorem
df_1nq
:
wceq
c1q
(
cop
c1o
c1o
)
(proof)
Theorem
df_rq
:
wceq
crq
(
cima
(
ccnv
cmq
)
(
csn
c1q
)
)
(proof)
Theorem
df_ltnq
:
wceq
cltq
(
cin
cltpq
(
cxp
cnq
cnq
)
)
(proof)
Theorem
df_np
:
wceq
cnp
(
cab
(
λ x0 .
wa
(
wa
(
wpss
c0
(
cv
x0
)
)
(
wpss
(
cv
x0
)
cnq
)
)
(
wral
(
λ x1 .
wa
(
∀ x2 .
wbr
(
cv
x2
)
(
cv
x1
)
cltq
⟶
wcel
(
cv
x2
)
(
cv
x0
)
)
(
wrex
(
λ x2 .
wbr
(
cv
x1
)
(
cv
x2
)
cltq
)
(
λ x2 .
cv
x0
)
)
)
(
λ x1 .
cv
x0
)
)
)
)
(proof)
Theorem
df_1p
:
wceq
c1p
(
cab
(
λ x0 .
wbr
(
cv
x0
)
c1q
cltq
)
)
(proof)
Theorem
df_plp
:
wceq
cpp
(
cmpt2
(
λ x0 x1 .
cnp
)
(
λ x0 x1 .
cnp
)
(
λ x0 x1 .
cab
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wceq
(
cv
x2
)
(
co
(
cv
x3
)
(
cv
x4
)
cplq
)
)
(
λ x4 .
cv
x1
)
)
(
λ x3 .
cv
x0
)
)
)
)
(proof)
Theorem
df_mp
:
wceq
cmp
(
cmpt2
(
λ x0 x1 .
cnp
)
(
λ x0 x1 .
cnp
)
(
λ x0 x1 .
cab
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wceq
(
cv
x2
)
(
co
(
cv
x3
)
(
cv
x4
)
cmq
)
)
(
λ x4 .
cv
x1
)
)
(
λ x3 .
cv
x0
)
)
)
)
(proof)
Theorem
df_ltp
:
wceq
cltp
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
cnp
)
(
wcel
(
cv
x1
)
cnp
)
)
(
wpss
(
cv
x0
)
(
cv
x1
)
)
)
)
(proof)
Theorem
df_enr
:
wceq
cer
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
(
cxp
cnp
cnp
)
)
(
wcel
(
cv
x1
)
(
cxp
cnp
cnp
)
)
)
(
wex
(
λ x2 .
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wa
(
wa
(
wceq
(
cv
x0
)
(
cop
(
cv
x2
)
(
cv
x3
)
)
)
(
wceq
(
cv
x1
)
(
cop
(
cv
x4
)
(
cv
x5
)
)
)
)
(
wceq
(
co
(
cv
x2
)
(
cv
x5
)
cpp
)
(
co
(
cv
x3
)
(
cv
x4
)
cpp
)
)
)
)
)
)
)
)
)
(proof)
Theorem
df_nr
:
wceq
cnr
(
cqs
(
cxp
cnp
cnp
)
cer
)
(proof)
Theorem
df_plr
:
wceq
cplr
(
coprab
(
λ x0 x1 x2 .
wa
(
wa
(
wcel
(
cv
x0
)
cnr
)
(
wcel
(
cv
x1
)
cnr
)
)
(
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wex
(
λ x6 .
wa
(
wa
(
wceq
(
cv
x0
)
(
cec
(
cop
(
cv
x3
)
(
cv
x4
)
)
cer
)
)
(
wceq
(
cv
x1
)
(
cec
(
cop
(
cv
x5
)
(
cv
x6
)
)
cer
)
)
)
(
wceq
(
cv
x2
)
(
cec
(
cop
(
co
(
cv
x3
)
(
cv
x5
)
cpp
)
(
co
(
cv
x4
)
(
cv
x6
)
cpp
)
)
cer
)
)
)
)
)
)
)
)
)
(proof)