Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrFK8..
/
61682..
PUXb5..
/
76985..
vout
PrFK8..
/
d5273..
0.00 bars
TMPjN..
/
47b0d..
ownership of
5de9e..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMRqv..
/
799db..
ownership of
bdf8f..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZE3..
/
c353c..
ownership of
89205..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMUGR..
/
e0db8..
ownership of
7f444..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMcQX..
/
4ca86..
ownership of
bb318..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMVJ7..
/
f69db..
ownership of
df367..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMdBY..
/
2fd73..
ownership of
4b32b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMd4m..
/
251c9..
ownership of
c0c4d..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMWPq..
/
ea8fc..
ownership of
26d05..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMbEX..
/
5155b..
ownership of
a2e75..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMcAU..
/
bb054..
ownership of
4fb58..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZSb..
/
44276..
ownership of
8a6bd..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMRAk..
/
16aba..
ownership of
385ef..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMJZ7..
/
26f7e..
ownership of
94b23..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMNKo..
/
6a1ab..
ownership of
dfb49..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMGMd..
/
27f0f..
ownership of
1f3f3..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMY3Z..
/
20d1d..
ownership of
f03aa..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMKxN..
/
c238b..
ownership of
95c6c..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
PUNUU..
/
b4204..
doc published by
Pr4zB..
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Definition
inj
inj
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
Definition
atleastp
atleastp
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
inj
x0
x1
x3
⟶
x2
)
⟶
x2
Param
ordsucc
ordsucc
:
ι
→
ι
Known
In_0_3
In_0_3
:
0
∈
3
Known
In_1_3
In_1_3
:
1
∈
3
Known
In_2_3
In_2_3
:
2
∈
3
Known
neq_0_1
neq_0_1
:
0
=
1
⟶
∀ x0 : ο .
x0
Known
neq_0_2
neq_0_2
:
0
=
2
⟶
∀ x0 : ο .
x0
Known
neq_1_2
neq_1_2
:
1
=
2
⟶
∀ x0 : ο .
x0
Theorem
f03aa..
:
∀ x0 .
atleastp
3
x0
⟶
∀ x1 : ο .
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
(
x2
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x2
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
x1
)
⟶
x1
(proof)
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
setminus
setminus
:
ι
→
ι
→
ι
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Known
PowerI
PowerI
:
∀ x0 x1 .
x1
⊆
x0
⟶
x1
∈
prim4
x0
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
setminusE
setminusE
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
and
(
x2
∈
x0
)
(
nIn
x2
x1
)
Known
ordsuccE
ordsuccE
:
∀ x0 x1 .
x1
∈
ordsucc
x0
⟶
or
(
x1
∈
x0
)
(
x1
=
x0
)
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Known
setminusE2
setminusE2
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
nIn
x2
x1
Known
setminusI
setminusI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
nIn
x2
x1
⟶
x2
∈
setminus
x0
x1
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
PowerE
PowerE
:
∀ x0 x1 .
x1
∈
prim4
x0
⟶
x1
⊆
x0
Theorem
dfb49..
:
∀ x0 x1 .
x1
⊆
prim4
(
ordsucc
x0
)
⟶
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
ordsucc
x0
)
(
x5
∈
x2
=
x5
∈
x3
)
⟶
x4
)
⟶
x4
)
⟶
atleastp
x1
(
prim4
x0
)
(proof)
Param
binunion
binunion
:
ι
→
ι
→
ι
Param
setsum
setsum
:
ι
→
ι
→
ι
Param
Inj0
Inj0
:
ι
→
ι
Param
Inj1
Inj1
:
ι
→
ι
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
Inj0_setsum
Inj0_setsum
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
Inj0
x2
∈
setsum
x0
x1
Known
Inj1_setsum
Inj1_setsum
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
Inj1
x2
∈
setsum
x0
x1
Known
Inj0_inj
Inj0_inj
:
∀ x0 x1 .
Inj0
x0
=
Inj0
x1
⟶
x0
=
x1
Known
Inj0_Inj1_neq
Inj0_Inj1_neq
:
∀ x0 x1 .
Inj0
x0
=
Inj1
x1
⟶
∀ x2 : ο .
x2
Known
Inj1_inj
Inj1_inj
:
∀ x0 x1 .
Inj1
x0
=
Inj1
x1
⟶
x0
=
x1
Theorem
385ef..
:
∀ x0 x1 x2 x3 .
atleastp
x0
x2
⟶
atleastp
x1
x3
⟶
(
∀ x4 .
x4
∈
x0
⟶
nIn
x4
x1
)
⟶
atleastp
(
binunion
x0
x1
)
(
setsum
x2
x3
)
(proof)
Param
nat_p
nat_p
:
ι
→
ο
Known
PigeonHole_nat
PigeonHole_nat
:
∀ x0 .
nat_p
x0
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
ordsucc
x0
⟶
x1
x2
∈
x0
)
⟶
not
(
∀ x2 .
x2
∈
ordsucc
x0
⟶
∀ x3 .
x3
∈
ordsucc
x0
⟶
x1
x2
=
x1
x3
⟶
x2
=
x3
)
Theorem
4fb58..
Pigeonhole_not_atleastp_ordsucc
:
∀ x0 .
nat_p
x0
⟶
not
(
atleastp
(
ordsucc
x0
)
x0
)
(proof)
Param
bij
bij
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Definition
equip
equip
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Param
ap
ap
:
ι
→
ι
→
ι
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
Sing
Sing
:
ι
→
ι
Known
bijI
bijI
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
⟶
bij
x0
x1
x2
Known
cases_4
cases_4
:
∀ x0 .
x0
∈
4
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
2
⟶
x1
3
⟶
x1
x0
Known
tuple_4_0_eq
tuple_4_0_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
0
=
x0
Known
Empty_In_Power
Empty_In_Power
:
∀ x0 .
0
∈
prim4
x0
Known
tuple_4_1_eq
tuple_4_1_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
1
=
x1
Known
Subq_1_2
Subq_1_2
:
1
⊆
2
Known
tuple_4_2_eq
tuple_4_2_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
2
=
x2
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Known
In_1_2
In_1_2
:
1
∈
2
Known
tuple_4_3_eq
tuple_4_3_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
3
=
x3
Known
Self_In_Power
Self_In_Power
:
∀ x0 .
x0
∈
prim4
x0
Known
not_Empty_eq_Sing
:
∀ x0 .
0
=
Sing
x0
⟶
∀ x1 : ο .
x1
Known
neq_1_0
neq_1_0
:
1
=
0
⟶
∀ x0 : ο .
x0
Known
nIn_not_eq_Sing
:
∀ x0 x1 .
nIn
x0
x1
⟶
x1
=
Sing
x0
⟶
∀ x2 : ο .
x2
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
In_0_2
In_0_2
:
0
∈
2
Known
neq_2_0
neq_2_0
:
2
=
0
⟶
∀ x0 : ο .
x0
Known
neq_2_1
neq_2_1
:
2
=
1
⟶
∀ x0 : ο .
x0
Known
In_Power_2_cases_impred
:
∀ x0 .
x0
∈
prim4
2
⟶
∀ x1 : ο .
(
x0
=
0
⟶
x1
)
⟶
(
x0
=
1
⟶
x1
)
⟶
(
x0
=
Sing
1
⟶
x1
)
⟶
(
x0
=
2
⟶
x1
)
⟶
x1
Known
In_0_4
In_0_4
:
0
∈
4
Known
In_1_4
In_1_4
:
1
∈
4
Known
In_2_4
In_2_4
:
2
∈
4
Known
In_3_4
In_3_4
:
3
∈
4
Theorem
26d05..
:
equip
4
(
prim4
2
)
(proof)
Known
bijE
bijE
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
∀ x3 : ο .
(
(
∀ x4 .
x4
∈
x0
⟶
x2
x4
∈
x1
)
⟶
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x2
x4
=
x2
x5
⟶
x4
=
x5
)
⟶
(
∀ x4 .
x4
∈
x1
⟶
∀ x5 : ο .
(
∀ x6 .
and
(
x6
∈
x0
)
(
x2
x6
=
x4
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
Known
Inj1I2
Inj1I2
:
∀ x0 x1 .
x1
∈
x0
⟶
Inj1
x1
∈
Inj1
x0
Known
Inj1I1
Inj1I1
:
∀ x0 .
0
∈
Inj1
x0
Known
Inj1NE1
Inj1NE1
:
∀ x0 .
Inj1
x0
=
0
⟶
∀ x1 : ο .
x1
Known
Inj1E
Inj1E
:
∀ x0 x1 .
x1
∈
Inj1
x0
⟶
or
(
x1
=
0
)
(
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x0
)
(
x1
=
Inj1
x3
)
⟶
x2
)
⟶
x2
)
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Theorem
4b32b..
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
(
ordsucc
x0
)
(
Inj1
x1
)
(proof)
Known
Inj1_setsum_1L
Inj1_setsum_1L
:
∀ x0 .
setsum
1
x0
=
Inj1
x0
Theorem
bb318..
:
equip
5
(
setsum
1
(
prim4
2
)
)
(proof)
Known
nat_5
nat_5
:
nat_p
5
Known
atleastp_tra
atleastp_tra
:
∀ x0 x1 x2 .
atleastp
x0
x1
⟶
atleastp
x1
x2
⟶
atleastp
x0
x2
Known
equip_atleastp
equip_atleastp
:
∀ x0 x1 .
equip
x0
x1
⟶
atleastp
x0
x1
Known
equip_sym
equip_sym
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
x1
x0
Theorem
89205..
:
∀ x0 x1 .
(
∀ x2 .
x2
∈
x0
⟶
nIn
x2
x1
)
⟶
atleastp
6
(
binunion
x0
x1
)
⟶
atleastp
x0
1
⟶
atleastp
x1
(
prim4
2
)
⟶
False
(proof)
Known
cases_3
cases_3
:
∀ x0 .
x0
∈
3
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
2
⟶
x1
x0
Theorem
5de9e..
:
∀ x0 .
x0
⊆
3
⟶
∀ x1 .
x1
⊆
3
⟶
0
∈
x0
=
0
∈
x1
⟶
1
∈
x0
=
1
∈
x1
⟶
2
∈
x0
=
2
∈
x1
⟶
x0
=
x1
(proof)