Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr314..
/
20380..
PULZn..
/
c9a24..
vout
Pr314..
/
99fc7..
44.14 bars
TMNJL..
/
922c0..
ownership of
40e63..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMLP..
/
df921..
ownership of
f844e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMJ2h..
/
b15ae..
ownership of
097ec..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYyj..
/
e8f4f..
ownership of
c802f..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHvn..
/
005c0..
ownership of
d5450..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMWvb..
/
f30b4..
ownership of
af5c9..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMdFS..
/
6024f..
ownership of
7484f..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHsc..
/
67431..
ownership of
5b2d2..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMViY..
/
5090f..
ownership of
84934..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMVPZ..
/
45fca..
ownership of
c5fc1..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZnZ..
/
0841c..
ownership of
c38f0..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMMuX..
/
2e447..
ownership of
45a71..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMaAs..
/
7d7f8..
ownership of
a616f..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMTgt..
/
fce5a..
ownership of
6f139..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMFEF..
/
078e1..
ownership of
0869d..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMJTE..
/
5ddfa..
ownership of
c7c4a..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMdvs..
/
b9917..
ownership of
440f9..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRpi..
/
a45df..
ownership of
1c4b7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMXZB..
/
a0a5e..
ownership of
f9f9c..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMR1e..
/
79500..
ownership of
fab35..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMWqR..
/
7dce1..
ownership of
07fd4..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMHB4..
/
627b8..
ownership of
072d8..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMQ4T..
/
94087..
ownership of
523de..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMQ2k..
/
2a8f0..
ownership of
8c3e9..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMc3U..
/
e3bd9..
ownership of
7b3f7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKAU..
/
3b661..
ownership of
221fd..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMH8E..
/
34bfb..
ownership of
7f221..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMWk1..
/
2d804..
ownership of
d490e..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRNE..
/
82647..
ownership of
ef681..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMPeo..
/
3a20d..
ownership of
1df4b..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZ8v..
/
aa669..
ownership of
9c07c..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKTQ..
/
54a2e..
ownership of
e1da7..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMRvc..
/
c1c89..
ownership of
0dacf..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMc1a..
/
0cd77..
ownership of
cc980..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMaVj..
/
57479..
ownership of
3f1df..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMP3v..
/
83767..
ownership of
431ff..
as prop with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMboF..
/
6f65a..
ownership of
1d79d..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMNLd..
/
2b9df..
ownership of
dd2a3..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZfH..
/
d1ef6..
ownership of
989da..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMcRv..
/
e8b06..
ownership of
c8482..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKTg..
/
d0402..
ownership of
2b257..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMbr9..
/
5952b..
ownership of
d768d..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMctT..
/
00771..
ownership of
7cd66..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMSu7..
/
37230..
ownership of
3115e..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMZcV..
/
cf15a..
ownership of
e47cc..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMYL2..
/
fe2d9..
ownership of
040f1..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMcBv..
/
fd03e..
ownership of
e5fe3..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMNYz..
/
1f128..
ownership of
2c274..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMLDG..
/
4a624..
ownership of
6b27d..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMEpg..
/
7e2db..
ownership of
a833c..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMdXf..
/
4bcdc..
ownership of
11c0b..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMbQX..
/
50f23..
ownership of
b0639..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMXqX..
/
5f64e..
ownership of
439cb..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMd9n..
/
4aa35..
ownership of
486f6..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMU2Y..
/
b1663..
ownership of
84b4d..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
TMKDx..
/
ba7a9..
ownership of
11a78..
as obj with payaddr
PrQUS..
rights free controlledby
PrQUS..
upto 0
PUVHe..
/
62545..
doc published by
PrQUS..
Param
f4b0e..
:
ι
→
ι
→
ι
→
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
84b4d..
:=
f4b0e..
0
1
0
0
Definition
439cb..
:=
f4b0e..
0
0
1
0
Definition
11c0b..
:=
f4b0e..
0
0
0
1
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
SNo
SNo
:
ι
→
ο
Definition
6b27d..
:=
λ x0 .
prim0
(
λ x1 .
and
(
SNo
x1
)
(
∃ x2 .
and
(
SNo
x2
)
(
∃ x4 .
and
(
SNo
x4
)
(
∃ x6 .
and
(
SNo
x6
)
(
x0
=
f4b0e..
x1
x2
x4
x6
)
)
)
)
)
Definition
e5fe3..
:=
λ x0 .
prim0
(
λ x1 .
and
(
SNo
x1
)
(
∃ x2 .
and
(
SNo
x2
)
(
∃ x4 .
and
(
SNo
x4
)
(
x0
=
f4b0e..
(
6b27d..
x0
)
x1
x2
x4
)
)
)
)
Definition
e47cc..
:=
λ x0 .
prim0
(
λ x1 .
and
(
SNo
x1
)
(
∃ x2 .
and
(
SNo
x2
)
(
x0
=
f4b0e..
(
6b27d..
x0
)
(
e5fe3..
x0
)
x1
x2
)
)
)
Definition
7cd66..
:=
λ x0 .
prim0
(
λ x1 .
and
(
SNo
x1
)
(
x0
=
f4b0e..
(
6b27d..
x0
)
(
e5fe3..
x0
)
(
e47cc..
x0
)
x1
)
)
Definition
8c189..
:=
λ x0 .
∃ x1 .
and
(
SNo
x1
)
(
∃ x3 .
and
(
SNo
x3
)
(
∃ x5 .
and
(
SNo
x5
)
(
∃ x7 .
and
(
SNo
x7
)
(
x0
=
f4b0e..
x1
x3
x5
x7
)
)
)
)
Known
Eps_i_ex
Eps_i_ex
:
∀ x0 :
ι → ο
.
(
∃ x1 .
x0
x1
)
⟶
x0
(
prim0
x0
)
Theorem
3f1df..
:
∀ x0 .
8c189..
x0
⟶
and
(
SNo
(
6b27d..
x0
)
)
(
∃ x1 .
and
(
SNo
x1
)
(
∃ x3 .
and
(
SNo
x3
)
(
∃ x5 .
and
(
SNo
x5
)
(
x0
=
f4b0e..
(
6b27d..
x0
)
x1
x3
x5
)
)
)
)
...
Theorem
0dacf..
:
∀ x0 .
8c189..
x0
⟶
and
(
SNo
(
e5fe3..
x0
)
)
(
∃ x1 .
and
(
SNo
x1
)
(
∃ x3 .
and
(
SNo
x3
)
(
x0
=
f4b0e..
(
6b27d..
x0
)
(
e5fe3..
x0
)
x1
x3
)
)
)
...
Theorem
9c07c..
:
∀ x0 .
8c189..
x0
⟶
and
(
SNo
(
e47cc..
x0
)
)
(
∃ x1 .
and
(
SNo
x1
)
(
x0
=
f4b0e..
(
6b27d..
x0
)
(
e5fe3..
x0
)
(
e47cc..
x0
)
x1
)
)
...
Theorem
ef681..
:
∀ x0 .
8c189..
x0
⟶
and
(
SNo
(
7cd66..
x0
)
)
(
x0
=
f4b0e..
(
6b27d..
x0
)
(
e5fe3..
x0
)
(
e47cc..
x0
)
(
7cd66..
x0
)
)
...
Theorem
7f221..
:
∀ x0 .
8c189..
x0
⟶
SNo
(
6b27d..
x0
)
...
Theorem
7b3f7..
:
∀ x0 .
8c189..
x0
⟶
SNo
(
e5fe3..
x0
)
...
Theorem
523de..
:
∀ x0 .
8c189..
x0
⟶
SNo
(
e47cc..
x0
)
...
Theorem
07fd4..
:
∀ x0 .
8c189..
x0
⟶
SNo
(
7cd66..
x0
)
...
Theorem
f9f9c..
:
∀ x0 .
8c189..
x0
⟶
x0
=
f4b0e..
(
6b27d..
x0
)
(
e5fe3..
x0
)
(
e47cc..
x0
)
(
7cd66..
x0
)
...
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Theorem
440f9..
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
8c189..
(
f4b0e..
x0
x1
x2
x3
)
...
Theorem
0869d..
:
∀ x0 .
8c189..
x0
⟶
∀ x1 :
ι → ο
.
(
∀ x2 x3 x4 x5 .
SNo
x2
⟶
SNo
x3
⟶
SNo
x4
⟶
SNo
x5
⟶
x0
=
f4b0e..
x2
x3
x4
x5
⟶
x1
(
f4b0e..
x2
x3
x4
x5
)
)
⟶
x1
x0
...
Known
SNo_0
SNo_0
:
SNo
0
Known
SNo_1
SNo_1
:
SNo
1
Theorem
a616f..
:
8c189..
84b4d..
...
Theorem
c38f0..
:
8c189..
439cb..
...
Theorem
84934..
:
8c189..
11c0b..
...
Known
84fad..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x4
⟶
SNo
x5
⟶
SNo
x6
⟶
f4b0e..
x0
x1
x2
x3
=
f4b0e..
x4
x5
x6
x7
⟶
x0
=
x4
Theorem
7484f..
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
6b27d..
(
f4b0e..
x0
x1
x2
x3
)
=
x0
...
Known
aa1e8..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
SNo
x4
⟶
SNo
x5
⟶
SNo
x6
⟶
SNo
x7
⟶
f4b0e..
x0
x1
x2
x3
=
f4b0e..
x4
x5
x6
x7
⟶
x1
=
x5
Theorem
d5450..
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
e5fe3..
(
f4b0e..
x0
x1
x2
x3
)
=
x1
...
Known
04ead..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
SNo
x4
⟶
SNo
x5
⟶
SNo
x6
⟶
SNo
x7
⟶
f4b0e..
x0
x1
x2
x3
=
f4b0e..
x4
x5
x6
x7
⟶
x2
=
x6
Theorem
097ec..
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
e47cc..
(
f4b0e..
x0
x1
x2
x3
)
=
x2
...
Known
57cf4..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
SNo
x4
⟶
SNo
x5
⟶
SNo
x6
⟶
SNo
x7
⟶
f4b0e..
x0
x1
x2
x3
=
f4b0e..
x4
x5
x6
x7
⟶
x3
=
x7
Theorem
40e63..
:
∀ x0 x1 x2 x3 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
7cd66..
(
f4b0e..
x0
x1
x2
x3
)
=
x3
...
Param
minus_SNo
minus_SNo
:
ι
→
ι
Definition
2b257..
:=
λ x0 .
f4b0e..
(
minus_SNo
(
6b27d..
x0
)
)
(
minus_SNo
(
e5fe3..
x0
)
)
(
minus_SNo
(
e47cc..
x0
)
)
(
minus_SNo
(
7cd66..
x0
)
)
Param
add_SNo
add_SNo
:
ι
→
ι
→
ι
Definition
989da..
:=
λ x0 x1 .
f4b0e..
(
add_SNo
(
6b27d..
x0
)
(
6b27d..
x1
)
)
(
add_SNo
(
e5fe3..
x0
)
(
e5fe3..
x1
)
)
(
add_SNo
(
e47cc..
x0
)
(
e47cc..
x1
)
)
(
add_SNo
(
7cd66..
x0
)
(
7cd66..
x1
)
)
Param
mul_SNo
mul_SNo
:
ι
→
ι
→
ι
Definition
1d79d..
:=
λ x0 x1 .
f4b0e..
(
add_SNo
(
mul_SNo
(
6b27d..
x0
)
(
6b27d..
x1
)
)
(
add_SNo
(
minus_SNo
(
mul_SNo
(
e5fe3..
x0
)
(
e5fe3..
x1
)
)
)
(
add_SNo
(
minus_SNo
(
mul_SNo
(
e47cc..
x0
)
(
e47cc..
x1
)
)
)
(
minus_SNo
(
mul_SNo
(
7cd66..
x0
)
(
7cd66..
x1
)
)
)
)
)
)
(
add_SNo
(
mul_SNo
(
6b27d..
x0
)
(
e5fe3..
x1
)
)
(
add_SNo
(
mul_SNo
(
e5fe3..
x0
)
(
6b27d..
x1
)
)
(
add_SNo
(
mul_SNo
(
e47cc..
x0
)
(
7cd66..
x1
)
)
(
minus_SNo
(
mul_SNo
(
7cd66..
x0
)
(
e47cc..
x1
)
)
)
)
)
)
(
add_SNo
(
mul_SNo
(
6b27d..
x0
)
(
e47cc..
x1
)
)
(
add_SNo
(
minus_SNo
(
mul_SNo
(
e5fe3..
x0
)
(
7cd66..
x1
)
)
)
(
add_SNo
(
mul_SNo
(
e47cc..
x0
)
(
6b27d..
x1
)
)
(
mul_SNo
(
7cd66..
x0
)
(
e5fe3..
x1
)
)
)
)
)
(
add_SNo
(
mul_SNo
(
6b27d..
x0
)
(
7cd66..
x1
)
)
(
add_SNo
(
mul_SNo
(
e5fe3..
x0
)
(
e47cc..
x1
)
)
(
add_SNo
(
minus_SNo
(
mul_SNo
(
e47cc..
x0
)
(
e5fe3..
x1
)
)
)
(
mul_SNo
(
7cd66..
x0
)
(
6b27d..
x1
)
)
)
)
)