Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrFBJ..
/
ec41e..
PUS6K..
/
b322a..
vout
PrFBJ..
/
12da8..
0.09 bars
TMLQh..
/
df661..
ownership of
64a17..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMNAX..
/
9fbc3..
ownership of
dd7c1..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVgz..
/
3aab6..
ownership of
3fbcc..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMa15..
/
fd692..
ownership of
2a095..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMKJZ..
/
13427..
ownership of
a08e0..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcU9..
/
3910b..
ownership of
95564..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcQo..
/
43969..
ownership of
541ba..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPao..
/
617b7..
ownership of
244ee..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQ3n..
/
afc1a..
ownership of
1e860..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMW5n..
/
a6c68..
ownership of
8f21c..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMK7p..
/
23c46..
ownership of
24703..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMamN..
/
6723f..
ownership of
96574..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcS9..
/
e43e6..
ownership of
25c87..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPxr..
/
b9d97..
ownership of
fe3b4..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMJZ9..
/
5bced..
ownership of
f8284..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQJx..
/
e64f5..
ownership of
e47cf..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TML7r..
/
c708d..
ownership of
cbb6b..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMS54..
/
71b16..
ownership of
98115..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMTNY..
/
e755e..
ownership of
b2522..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMUT9..
/
f51db..
ownership of
ec254..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZRV..
/
58004..
ownership of
6b1df..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMThE..
/
a57e9..
ownership of
a0eac..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQqC..
/
d6c07..
ownership of
05fe1..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMJJo..
/
4b20e..
ownership of
ca3f3..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMPVy..
/
96ad8..
ownership of
e6dc4..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQT9..
/
65935..
ownership of
91429..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMGSP..
/
79e75..
ownership of
5e815..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVT5..
/
57f95..
ownership of
42d5e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMT9L..
/
f1f6a..
ownership of
72aff..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMGkG..
/
00d8d..
ownership of
6d788..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMbkS..
/
207ab..
ownership of
4df1d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMT1Y..
/
86660..
ownership of
4dfb0..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVU7..
/
529f1..
ownership of
5d7d9..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVM2..
/
765f0..
ownership of
9426e..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMLqj..
/
6ab28..
ownership of
0ab0c..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMUyK..
/
d8dc6..
ownership of
5638a..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
PUd3U..
/
75f17..
doc published by
PrCmT..
Known
df_mr__df_ltr__df_0r__df_1r__df_m1r__df_c__df_0__df_1__df_i__df_r__df_add__df_mul__df_lt__df_pnf__df_mnf__df_xr__df_ltxr__df_le
:
∀ x0 : ο .
(
wceq
cmr
(
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
(
co
(
cv
x4
)
(
cv
x6
)
cmp
)
(
co
(
cv
x5
)
(
cv
x7
)
cmp
)
cpp
)
(
co
(
co
(
cv
x4
)
(
cv
x7
)
cmp
)
(
co
(
cv
x5
)
(
cv
x6
)
cmp
)
cpp
)
)
cer
)
)
)
)
)
)
)
)
)
⟶
wceq
cltr
(
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
cnr
)
(
wcel
(
cv
x2
)
cnr
)
)
(
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wex
(
λ x6 .
wa
(
wa
(
wceq
(
cv
x1
)
(
cec
(
cop
(
cv
x3
)
(
cv
x4
)
)
cer
)
)
(
wceq
(
cv
x2
)
(
cec
(
cop
(
cv
x5
)
(
cv
x6
)
)
cer
)
)
)
(
wbr
(
co
(
cv
x3
)
(
cv
x6
)
cpp
)
(
co
(
cv
x4
)
(
cv
x5
)
cpp
)
cltp
)
)
)
)
)
)
)
)
⟶
wceq
c0r
(
cec
(
cop
c1p
c1p
)
cer
)
⟶
wceq
c1r
(
cec
(
cop
(
co
c1p
c1p
cpp
)
c1p
)
cer
)
⟶
wceq
cm1r
(
cec
(
cop
c1p
(
co
c1p
c1p
cpp
)
)
cer
)
⟶
wceq
cc
(
cxp
cnr
cnr
)
⟶
wceq
cc0
(
cop
c0r
c0r
)
⟶
wceq
c1
(
cop
c1r
c0r
)
⟶
wceq
ci
(
cop
c0r
c1r
)
⟶
wceq
cr
(
cxp
cnr
(
csn
c0r
)
)
⟶
wceq
caddc
(
coprab
(
λ x1 x2 x3 .
wa
(
wa
(
wcel
(
cv
x1
)
cc
)
(
wcel
(
cv
x2
)
cc
)
)
(
wex
(
λ x4 .
wex
(
λ x5 .
wex
(
λ x6 .
wex
(
λ x7 .
wa
(
wa
(
wceq
(
cv
x1
)
(
cop
(
cv
x4
)
(
cv
x5
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
cv
x6
)
(
cv
x7
)
)
)
)
(
wceq
(
cv
x3
)
(
cop
(
co
(
cv
x4
)
(
cv
x6
)
cplr
)
(
co
(
cv
x5
)
(
cv
x7
)
cplr
)
)
)
)
)
)
)
)
)
)
⟶
wceq
cmul
(
coprab
(
λ x1 x2 x3 .
wa
(
wa
(
wcel
(
cv
x1
)
cc
)
(
wcel
(
cv
x2
)
cc
)
)
(
wex
(
λ x4 .
wex
(
λ x5 .
wex
(
λ x6 .
wex
(
λ x7 .
wa
(
wa
(
wceq
(
cv
x1
)
(
cop
(
cv
x4
)
(
cv
x5
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
cv
x6
)
(
cv
x7
)
)
)
)
(
wceq
(
cv
x3
)
(
cop
(
co
(
co
(
cv
x4
)
(
cv
x6
)
cmr
)
(
co
cm1r
(
co
(
cv
x5
)
(
cv
x7
)
cmr
)
cmr
)
cplr
)
(
co
(
co
(
cv
x5
)
(
cv
x6
)
cmr
)
(
co
(
cv
x4
)
(
cv
x7
)
cmr
)
cplr
)
)
)
)
)
)
)
)
)
)
⟶
wceq
cltrr
(
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
cr
)
(
wcel
(
cv
x2
)
cr
)
)
(
wex
(
λ x3 .
wex
(
λ x4 .
wa
(
wa
(
wceq
(
cv
x1
)
(
cop
(
cv
x3
)
c0r
)
)
(
wceq
(
cv
x2
)
(
cop
(
cv
x4
)
c0r
)
)
)
(
wbr
(
cv
x3
)
(
cv
x4
)
cltr
)
)
)
)
)
)
⟶
wceq
cpnf
(
cpw
(
cuni
cc
)
)
⟶
wceq
cmnf
(
cpw
cpnf
)
⟶
wceq
cxr
(
cun
cr
(
cpr
cpnf
cmnf
)
)
⟶
wceq
clt
(
cun
(
copab
(
λ x1 x2 .
w3a
(
wcel
(
cv
x1
)
cr
)
(
wcel
(
cv
x2
)
cr
)
(
wbr
(
cv
x1
)
(
cv
x2
)
cltrr
)
)
)
(
cun
(
cxp
(
cun
cr
(
csn
cmnf
)
)
(
csn
cpnf
)
)
(
cxp
(
csn
cmnf
)
cr
)
)
)
⟶
wceq
cle
(
cdif
(
cxp
cxr
cxr
)
(
ccnv
clt
)
)
⟶
x0
)
⟶
x0
Theorem
df_mr
:
wceq
cmr
(
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
(
co
(
cv
x3
)
(
cv
x5
)
cmp
)
(
co
(
cv
x4
)
(
cv
x6
)
cmp
)
cpp
)
(
co
(
co
(
cv
x3
)
(
cv
x6
)
cmp
)
(
co
(
cv
x4
)
(
cv
x5
)
cmp
)
cpp
)
)
cer
)
)
)
)
)
)
)
)
)
(proof)
Theorem
df_ltr
:
wceq
cltr
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
cnr
)
(
wcel
(
cv
x1
)
cnr
)
)
(
wex
(
λ x2 .
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wa
(
wa
(
wceq
(
cv
x0
)
(
cec
(
cop
(
cv
x2
)
(
cv
x3
)
)
cer
)
)
(
wceq
(
cv
x1
)
(
cec
(
cop
(
cv
x4
)
(
cv
x5
)
)
cer
)
)
)
(
wbr
(
co
(
cv
x2
)
(
cv
x5
)
cpp
)
(
co
(
cv
x3
)
(
cv
x4
)
cpp
)
cltp
)
)
)
)
)
)
)
)
(proof)
Theorem
df_0r
:
wceq
c0r
(
cec
(
cop
c1p
c1p
)
cer
)
(proof)
Theorem
df_1r
:
wceq
c1r
(
cec
(
cop
(
co
c1p
c1p
cpp
)
c1p
)
cer
)
(proof)
Theorem
df_m1r
:
wceq
cm1r
(
cec
(
cop
c1p
(
co
c1p
c1p
cpp
)
)
cer
)
(proof)
Theorem
df_c
:
wceq
cc
(
cxp
cnr
cnr
)
(proof)
Theorem
df_0
:
wceq
cc0
(
cop
c0r
c0r
)
(proof)
Theorem
df_1
:
wceq
c1
(
cop
c1r
c0r
)
(proof)
Theorem
df_i
:
wceq
ci
(
cop
c0r
c1r
)
(proof)
Theorem
df_r
:
wceq
cr
(
cxp
cnr
(
csn
c0r
)
)
(proof)
Theorem
df_add
:
wceq
caddc
(
coprab
(
λ x0 x1 x2 .
wa
(
wa
(
wcel
(
cv
x0
)
cc
)
(
wcel
(
cv
x1
)
cc
)
)
(
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wex
(
λ x6 .
wa
(
wa
(
wceq
(
cv
x0
)
(
cop
(
cv
x3
)
(
cv
x4
)
)
)
(
wceq
(
cv
x1
)
(
cop
(
cv
x5
)
(
cv
x6
)
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
co
(
cv
x3
)
(
cv
x5
)
cplr
)
(
co
(
cv
x4
)
(
cv
x6
)
cplr
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
df_mul
:
wceq
cmul
(
coprab
(
λ x0 x1 x2 .
wa
(
wa
(
wcel
(
cv
x0
)
cc
)
(
wcel
(
cv
x1
)
cc
)
)
(
wex
(
λ x3 .
wex
(
λ x4 .
wex
(
λ x5 .
wex
(
λ x6 .
wa
(
wa
(
wceq
(
cv
x0
)
(
cop
(
cv
x3
)
(
cv
x4
)
)
)
(
wceq
(
cv
x1
)
(
cop
(
cv
x5
)
(
cv
x6
)
)
)
)
(
wceq
(
cv
x2
)
(
cop
(
co
(
co
(
cv
x3
)
(
cv
x5
)
cmr
)
(
co
cm1r
(
co
(
cv
x4
)
(
cv
x6
)
cmr
)
cmr
)
cplr
)
(
co
(
co
(
cv
x4
)
(
cv
x5
)
cmr
)
(
co
(
cv
x3
)
(
cv
x6
)
cmr
)
cplr
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
df_lt
:
wceq
cltrr
(
copab
(
λ x0 x1 .
wa
(
wa
(
wcel
(
cv
x0
)
cr
)
(
wcel
(
cv
x1
)
cr
)
)
(
wex
(
λ x2 .
wex
(
λ x3 .
wa
(
wa
(
wceq
(
cv
x0
)
(
cop
(
cv
x2
)
c0r
)
)
(
wceq
(
cv
x1
)
(
cop
(
cv
x3
)
c0r
)
)
)
(
wbr
(
cv
x2
)
(
cv
x3
)
cltr
)
)
)
)
)
)
(proof)
Theorem
df_pnf
:
wceq
cpnf
(
cpw
(
cuni
cc
)
)
(proof)
Theorem
df_mnf
:
wceq
cmnf
(
cpw
cpnf
)
(proof)
Theorem
df_xr
:
wceq
cxr
(
cun
cr
(
cpr
cpnf
cmnf
)
)
(proof)
Theorem
df_ltxr
:
wceq
clt
(
cun
(
copab
(
λ x0 x1 .
w3a
(
wcel
(
cv
x0
)
cr
)
(
wcel
(
cv
x1
)
cr
)
(
wbr
(
cv
x0
)
(
cv
x1
)
cltrr
)
)
)
(
cun
(
cxp
(
cun
cr
(
csn
cmnf
)
)
(
csn
cpnf
)
)
(
cxp
(
csn
cmnf
)
cr
)
)
)
(proof)
Theorem
df_le
:
wceq
cle
(
cdif
(
cxp
cxr
cxr
)
(
ccnv
clt
)
)
(proof)