Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrJvx..
/
c22ff..
PUdHp..
/
97a8b..
vout
PrJvx..
/
edd93..
0.09 bars
TMHbo..
/
b85ca..
ownership of
fde79..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMSgo..
/
aabaf..
ownership of
18fc3..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVmi..
/
486cc..
ownership of
bf4f6..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMKxM..
/
e1aa6..
ownership of
4cad1..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMLaj..
/
696dc..
ownership of
0c2df..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcPS..
/
70c11..
ownership of
761cb..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMXiz..
/
2ab97..
ownership of
d2c15..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMHvo..
/
ab743..
ownership of
49ed5..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMXXC..
/
a1de1..
ownership of
c8619..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcKe..
/
09d2f..
ownership of
5289b..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMLA2..
/
9ab7a..
ownership of
5076b..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMX2c..
/
b2b68..
ownership of
62029..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMGAU..
/
14ad7..
ownership of
96bdb..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMQKZ..
/
14720..
ownership of
eef7d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMa2y..
/
fcf93..
ownership of
f64c7..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMdAL..
/
86237..
ownership of
e6aa0..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMSYc..
/
056ae..
ownership of
ce7a2..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVnS..
/
0f2ff..
ownership of
074ec..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMTfq..
/
0f5fa..
ownership of
26759..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMcDn..
/
2ac20..
ownership of
985a3..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMMWM..
/
71e09..
ownership of
b328d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMdXq..
/
11b95..
ownership of
666bc..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMKdk..
/
dbf00..
ownership of
9d503..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMJwz..
/
da266..
ownership of
5593d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMSWW..
/
a41bb..
ownership of
3816d..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMLQX..
/
7f7fd..
ownership of
42039..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMKUU..
/
4a602..
ownership of
b5df6..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMHNV..
/
1a042..
ownership of
b40d2..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMTa2..
/
37ace..
ownership of
d9532..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMZ4U..
/
8d861..
ownership of
b13b0..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMaXV..
/
eca17..
ownership of
416c1..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMRqZ..
/
7ca6b..
ownership of
4bd28..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMVqb..
/
734a4..
ownership of
f298b..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMHVz..
/
eca6b..
ownership of
c1dea..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMNWt..
/
cab5d..
ownership of
6d6be..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
TMYHS..
/
8ca5c..
ownership of
fd7e3..
as prop with payaddr
PrCmT..
rights free controlledby
PrCmT..
upto 0
PUSmC..
/
ae121..
doc published by
PrCmT..
Known
df_sub__df_neg__df_div__df_nn__df_2__df_3__df_4__df_5__df_6__df_7__df_8__df_9__df_10OLD__df_n0__df_xnn0__df_z__df_dec__df_uz
:
∀ x0 : ο .
(
wceq
cmin
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
crio
(
λ x3 .
wceq
(
co
(
cv
x2
)
(
cv
x3
)
caddc
)
(
cv
x1
)
)
(
λ x3 .
cc
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cneg
x1
)
(
co
cc0
x1
cmin
)
)
⟶
wceq
cdiv
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cdif
cc
(
csn
cc0
)
)
(
λ x1 x2 .
crio
(
λ x3 .
wceq
(
co
(
cv
x2
)
(
cv
x3
)
cmul
)
(
cv
x1
)
)
(
λ x3 .
cc
)
)
)
⟶
wceq
cn
(
cima
(
crdg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
co
(
cv
x1
)
c1
caddc
)
)
c1
)
com
)
⟶
wceq
c2
(
co
c1
c1
caddc
)
⟶
wceq
c3
(
co
c2
c1
caddc
)
⟶
wceq
c4
(
co
c3
c1
caddc
)
⟶
wceq
c5
(
co
c4
c1
caddc
)
⟶
wceq
c6
(
co
c5
c1
caddc
)
⟶
wceq
c7
(
co
c6
c1
caddc
)
⟶
wceq
c8
(
co
c7
c1
caddc
)
⟶
wceq
c9
(
co
c8
c1
caddc
)
⟶
wceq
c10
(
co
c9
c1
caddc
)
⟶
wceq
cn0
(
cun
cn
(
csn
cc0
)
)
⟶
wceq
cxnn0
(
cun
cn0
(
csn
cpnf
)
)
⟶
wceq
cz
(
crab
(
λ x1 .
w3o
(
wceq
(
cv
x1
)
cc0
)
(
wcel
(
cv
x1
)
cn
)
(
wcel
(
cneg
(
cv
x1
)
)
cn
)
)
(
λ x1 .
cr
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cdc
x1
x2
)
(
co
(
co
(
co
c9
c1
caddc
)
x1
cmul
)
x2
caddc
)
)
⟶
wceq
cuz
(
cmpt
(
λ x1 .
cz
)
(
λ x1 .
crab
(
λ x2 .
wbr
(
cv
x1
)
(
cv
x2
)
cle
)
(
λ x2 .
cz
)
)
)
⟶
x0
)
⟶
x0
Theorem
df_sub
:
wceq
cmin
(
cmpt2
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
crio
(
λ x2 .
wceq
(
co
(
cv
x1
)
(
cv
x2
)
caddc
)
(
cv
x0
)
)
(
λ x2 .
cc
)
)
)
(proof)
Theorem
df_neg
:
∀ x0 :
ι → ο
.
wceq
(
cneg
x0
)
(
co
cc0
x0
cmin
)
(proof)
Theorem
df_div
:
wceq
cdiv
(
cmpt2
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cdif
cc
(
csn
cc0
)
)
(
λ x0 x1 .
crio
(
λ x2 .
wceq
(
co
(
cv
x1
)
(
cv
x2
)
cmul
)
(
cv
x0
)
)
(
λ x2 .
cc
)
)
)
(proof)
Theorem
df_nn
:
wceq
cn
(
cima
(
crdg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
co
(
cv
x0
)
c1
caddc
)
)
c1
)
com
)
(proof)
Theorem
df_2
:
wceq
c2
(
co
c1
c1
caddc
)
(proof)
Theorem
df_3
:
wceq
c3
(
co
c2
c1
caddc
)
(proof)
Theorem
df_4
:
wceq
c4
(
co
c3
c1
caddc
)
(proof)
Theorem
df_5
:
wceq
c5
(
co
c4
c1
caddc
)
(proof)
Theorem
df_6
:
wceq
c6
(
co
c5
c1
caddc
)
(proof)
Theorem
df_7
:
wceq
c7
(
co
c6
c1
caddc
)
(proof)
Theorem
df_8
:
wceq
c8
(
co
c7
c1
caddc
)
(proof)
Theorem
df_9
:
wceq
c9
(
co
c8
c1
caddc
)
(proof)
Theorem
df_10OLD
:
wceq
c10
(
co
c9
c1
caddc
)
(proof)
Theorem
df_n0
:
wceq
cn0
(
cun
cn
(
csn
cc0
)
)
(proof)
Theorem
df_xnn0
:
wceq
cxnn0
(
cun
cn0
(
csn
cpnf
)
)
(proof)
Theorem
df_z
:
wceq
cz
(
crab
(
λ x0 .
w3o
(
wceq
(
cv
x0
)
cc0
)
(
wcel
(
cv
x0
)
cn
)
(
wcel
(
cneg
(
cv
x0
)
)
cn
)
)
(
λ x0 .
cr
)
)
(proof)
Theorem
df_dec
:
∀ x0 x1 :
ι → ο
.
wceq
(
cdc
x0
x1
)
(
co
(
co
(
co
c9
c1
caddc
)
x0
cmul
)
x1
caddc
)
(proof)
Theorem
df_uz
:
wceq
cuz
(
cmpt
(
λ x0 .
cz
)
(
λ x0 .
crab
(
λ x1 .
wbr
(
cv
x0
)
(
cv
x1
)
cle
)
(
λ x1 .
cz
)
)
)
(proof)