Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrCit..
/
fb4f4..
PUZ64..
/
9704d..
vout
PrCit..
/
bad4c..
3.82 bars
TMYdo..
/
78b7c..
ownership of
5f4d4..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMdK5..
/
86e52..
ownership of
a1719..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMWkE..
/
f376d..
ownership of
9379b..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMNiU..
/
5f1d9..
ownership of
8e3d5..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMEk8..
/
4e006..
ownership of
fa851..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMbbq..
/
a88f3..
ownership of
7d6f7..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMKuU..
/
3384c..
ownership of
aafc6..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMEs9..
/
8b9b0..
ownership of
6479a..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMLJE..
/
a6b39..
ownership of
7410a..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMGSJ..
/
9a2a4..
ownership of
185e9..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMFbS..
/
f05dd..
ownership of
2bb23..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMRZr..
/
52f85..
ownership of
5058d..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMNKk..
/
a5c4e..
ownership of
c0b4c..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMZ3X..
/
1411a..
ownership of
591f6..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMXNo..
/
ef157..
ownership of
7132f..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMXaB..
/
043fa..
ownership of
a2d5a..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMWEN..
/
af21b..
ownership of
7045e..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMVpB..
/
42e93..
ownership of
6afa0..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMJta..
/
053b5..
ownership of
cc49b..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMa4u..
/
1c35e..
ownership of
4dde1..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMM5w..
/
a9e58..
ownership of
540e6..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMLZE..
/
8bf41..
ownership of
742be..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMaWt..
/
a323c..
ownership of
9018e..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMb5e..
/
88330..
ownership of
ffe0a..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMWGy..
/
7b5d5..
ownership of
a7839..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMRnv..
/
72d21..
ownership of
c2738..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMLz8..
/
61985..
ownership of
617e2..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMUM6..
/
49f60..
ownership of
1afe5..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMY38..
/
76bbe..
ownership of
c34a2..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMRTT..
/
49606..
ownership of
3c85a..
as prop with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMcix..
/
6fe5b..
ownership of
55574..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
TMZgb..
/
0ee50..
ownership of
d73fb..
as obj with payaddr
Pr4zB..
rightscost 0.00 controlledby
Pr4zB..
upto 0
PUVbn..
/
18444..
doc published by
Pr4zB..
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u1
:=
1
Definition
u2
:=
ordsucc
u1
Definition
u3
:=
ordsucc
u2
Definition
u4
:=
ordsucc
u3
Definition
u5
:=
ordsucc
u4
Definition
u6
:=
ordsucc
u5
Definition
u7
:=
ordsucc
u6
Definition
u8
:=
ordsucc
u7
Definition
u9
:=
ordsucc
u8
Definition
u10
:=
ordsucc
u9
Definition
u11
:=
ordsucc
u10
Definition
u12
:=
ordsucc
u11
Definition
u13
:=
ordsucc
u12
Definition
u14
:=
ordsucc
u13
Definition
u15
:=
ordsucc
u14
Definition
u16
:=
ordsucc
u15
Definition
u17
:=
ordsucc
u16
Definition
u18
:=
ordsucc
u17
Definition
u19
:=
ordsucc
u18
Definition
u20
:=
ordsucc
u19
Definition
u21
:=
ordsucc
u20
Definition
u22
:=
ordsucc
u21
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
179f3..
:
0
∈
u21
Theorem
c34a2..
:
0
∈
u22
(proof)
Known
07fdb..
:
u1
∈
u21
Theorem
617e2..
:
u1
∈
u22
(proof)
Known
c25ea..
:
u2
∈
u21
Theorem
a7839..
:
u2
∈
u22
(proof)
Known
0750b..
:
u3
∈
u21
Theorem
9018e..
:
u3
∈
u22
(proof)
Known
701a9..
:
u4
∈
u21
Theorem
540e6..
:
u4
∈
u22
(proof)
Param
ap
ap
:
ι
→
ι
→
ι
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Known
48efb..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 .
x3
∈
x1
⟶
ap
(
lam
x1
(
λ x5 .
If_i
(
x5
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x5
)
)
)
x3
=
x0
Theorem
cc49b..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 .
ap
(
lam
22
(
λ x23 .
If_i
(
x23
=
0
)
x0
(
If_i
(
x23
=
1
)
x1
(
If_i
(
x23
=
2
)
x2
(
If_i
(
x23
=
3
)
x3
(
If_i
(
x23
=
4
)
x4
(
If_i
(
x23
=
5
)
x5
(
If_i
(
x23
=
6
)
x6
(
If_i
(
x23
=
7
)
x7
(
If_i
(
x23
=
8
)
x8
(
If_i
(
x23
=
9
)
x9
(
If_i
(
x23
=
10
)
x10
(
If_i
(
x23
=
11
)
x11
(
If_i
(
x23
=
12
)
x12
(
If_i
(
x23
=
13
)
x13
(
If_i
(
x23
=
14
)
x14
(
If_i
(
x23
=
15
)
x15
(
If_i
(
x23
=
16
)
x16
(
If_i
(
x23
=
17
)
x17
(
If_i
(
x23
=
18
)
x18
(
If_i
(
x23
=
19
)
x19
(
If_i
(
x23
=
20
)
x20
x21
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
0
=
x0
(proof)
Known
d21a1..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 x4 .
(
x4
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
ap
(
lam
x1
(
λ x6 .
If_i
(
x6
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x6
)
)
)
x4
=
ap
(
lam
x1
(
x2
(
ordsucc
x3
)
)
)
x4
Known
neq_1_0
neq_1_0
:
u1
=
0
⟶
∀ x0 : ο .
x0
Theorem
7045e..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 .
ap
(
lam
22
(
λ x23 .
If_i
(
x23
=
0
)
x0
(
If_i
(
x23
=
1
)
x1
(
If_i
(
x23
=
2
)
x2
(
If_i
(
x23
=
3
)
x3
(
If_i
(
x23
=
4
)
x4
(
If_i
(
x23
=
5
)
x5
(
If_i
(
x23
=
6
)
x6
(
If_i
(
x23
=
7
)
x7
(
If_i
(
x23
=
8
)
x8
(
If_i
(
x23
=
9
)
x9
(
If_i
(
x23
=
10
)
x10
(
If_i
(
x23
=
11
)
x11
(
If_i
(
x23
=
12
)
x12
(
If_i
(
x23
=
13
)
x13
(
If_i
(
x23
=
14
)
x14
(
If_i
(
x23
=
15
)
x15
(
If_i
(
x23
=
16
)
x16
(
If_i
(
x23
=
17
)
x17
(
If_i
(
x23
=
18
)
x18
(
If_i
(
x23
=
19
)
x19
(
If_i
(
x23
=
20
)
x20
x21
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
u1
=
x1
(proof)
Known
neq_2_0
neq_2_0
:
u2
=
0
⟶
∀ x0 : ο .
x0
Known
neq_2_1
neq_2_1
:
u2
=
u1
⟶
∀ x0 : ο .
x0
Theorem
7132f..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 .
ap
(
lam
22
(
λ x23 .
If_i
(
x23
=
0
)
x0
(
If_i
(
x23
=
1
)
x1
(
If_i
(
x23
=
2
)
x2
(
If_i
(
x23
=
3
)
x3
(
If_i
(
x23
=
4
)
x4
(
If_i
(
x23
=
5
)
x5
(
If_i
(
x23
=
6
)
x6
(
If_i
(
x23
=
7
)
x7
(
If_i
(
x23
=
8
)
x8
(
If_i
(
x23
=
9
)
x9
(
If_i
(
x23
=
10
)
x10
(
If_i
(
x23
=
11
)
x11
(
If_i
(
x23
=
12
)
x12
(
If_i
(
x23
=
13
)
x13
(
If_i
(
x23
=
14
)
x14
(
If_i
(
x23
=
15
)
x15
(
If_i
(
x23
=
16
)
x16
(
If_i
(
x23
=
17
)
x17
(
If_i
(
x23
=
18
)
x18
(
If_i
(
x23
=
19
)
x19
(
If_i
(
x23
=
20
)
x20
x21
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
u2
=
x2
(proof)
Known
neq_3_0
neq_3_0
:
u3
=
0
⟶
∀ x0 : ο .
x0
Known
neq_3_1
neq_3_1
:
u3
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_3_2
neq_3_2
:
u3
=
u2
⟶
∀ x0 : ο .
x0
Theorem
c0b4c..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 .
ap
(
lam
22
(
λ x23 .
If_i
(
x23
=
0
)
x0
(
If_i
(
x23
=
1
)
x1
(
If_i
(
x23
=
2
)
x2
(
If_i
(
x23
=
3
)
x3
(
If_i
(
x23
=
4
)
x4
(
If_i
(
x23
=
5
)
x5
(
If_i
(
x23
=
6
)
x6
(
If_i
(
x23
=
7
)
x7
(
If_i
(
x23
=
8
)
x8
(
If_i
(
x23
=
9
)
x9
(
If_i
(
x23
=
10
)
x10
(
If_i
(
x23
=
11
)
x11
(
If_i
(
x23
=
12
)
x12
(
If_i
(
x23
=
13
)
x13
(
If_i
(
x23
=
14
)
x14
(
If_i
(
x23
=
15
)
x15
(
If_i
(
x23
=
16
)
x16
(
If_i
(
x23
=
17
)
x17
(
If_i
(
x23
=
18
)
x18
(
If_i
(
x23
=
19
)
x19
(
If_i
(
x23
=
20
)
x20
x21
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
u3
=
x3
(proof)
Known
neq_4_0
neq_4_0
:
u4
=
0
⟶
∀ x0 : ο .
x0
Known
neq_4_1
neq_4_1
:
u4
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_4_2
neq_4_2
:
u4
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_4_3
neq_4_3
:
u4
=
u3
⟶
∀ x0 : ο .
x0
Theorem
2bb23..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 .
ap
(
lam
22
(
λ x23 .
If_i
(
x23
=
0
)
x0
(
If_i
(
x23
=
1
)
x1
(
If_i
(
x23
=
2
)
x2
(
If_i
(
x23
=
3
)
x3
(
If_i
(
x23
=
4
)
x4
(
If_i
(
x23
=
5
)
x5
(
If_i
(
x23
=
6
)
x6
(
If_i
(
x23
=
7
)
x7
(
If_i
(
x23
=
8
)
x8
(
If_i
(
x23
=
9
)
x9
(
If_i
(
x23
=
10
)
x10
(
If_i
(
x23
=
11
)
x11
(
If_i
(
x23
=
12
)
x12
(
If_i
(
x23
=
13
)
x13
(
If_i
(
x23
=
14
)
x14
(
If_i
(
x23
=
15
)
x15
(
If_i
(
x23
=
16
)
x16
(
If_i
(
x23
=
17
)
x17
(
If_i
(
x23
=
18
)
x18
(
If_i
(
x23
=
19
)
x19
(
If_i
(
x23
=
20
)
x20
x21
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
u4
=
x4
(proof)
Definition
55574..
:=
λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 .
ap
(
lam
22
(
λ x23 .
If_i
(
x23
=
0
)
x1
(
If_i
(
x23
=
1
)
x2
(
If_i
(
x23
=
2
)
x3
(
If_i
(
x23
=
3
)
x4
(
If_i
(
x23
=
4
)
x5
(
If_i
(
x23
=
5
)
x6
(
If_i
(
x23
=
6
)
x7
(
If_i
(
x23
=
7
)
x8
(
If_i
(
x23
=
8
)
x9
(
If_i
(
x23
=
9
)
x10
(
If_i
(
x23
=
10
)
x11
(
If_i
(
x23
=
11
)
x12
(
If_i
(
x23
=
12
)
x13
(
If_i
(
x23
=
13
)
x14
(
If_i
(
x23
=
14
)
x15
(
If_i
(
x23
=
15
)
x16
(
If_i
(
x23
=
16
)
x17
(
If_i
(
x23
=
17
)
x18
(
If_i
(
x23
=
18
)
x19
(
If_i
(
x23
=
19
)
x20
(
If_i
(
x23
=
20
)
x21
x22
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
x0
Theorem
7410a..
:
55574..
0
=
λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 .
x1
(proof)
Theorem
aafc6..
:
55574..
u1
=
λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 .
x2
(proof)
Theorem
fa851..
:
55574..
u2
=
λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 .
x3
(proof)
Theorem
9379b..
:
55574..
u3
=
λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 .
x4
(proof)
Theorem
5f4d4..
:
55574..
u4
=
λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 .
x5
(proof)