Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr6G3..
/
2ae1d..
PUYHm..
/
b0c99..
vout
Pr6G3..
/
24454..
6.25 bars
TMYZL..
/
9770b..
ownership of
d2ce5..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMdY2..
/
83ef9..
ownership of
b3305..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMZtJ..
/
79c37..
ownership of
364bd..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMXEo..
/
09c1b..
ownership of
3deb6..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMTNp..
/
497aa..
ownership of
3a427..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMcBS..
/
eeb64..
ownership of
507ac..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMSyi..
/
6fcc6..
ownership of
c412b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMbFN..
/
74dde..
ownership of
0e83b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMTXi..
/
104c2..
ownership of
e67b3..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMPjx..
/
d6ac9..
ownership of
a9d5b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMRsf..
/
0ae72..
ownership of
05a66..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMdMv..
/
5ae01..
ownership of
649bd..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMcmY..
/
022fe..
ownership of
9a412..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMSBo..
/
ee9c8..
ownership of
c9d4b..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMc1D..
/
9eec9..
ownership of
be3b8..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMMPJ..
/
9774b..
ownership of
55d7a..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMUgX..
/
976f0..
ownership of
314c4..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TML3y..
/
b6cfa..
ownership of
92cca..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMTZm..
/
cd987..
ownership of
c1cde..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMaF6..
/
16fcd..
ownership of
1bdd2..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMQmU..
/
6a2b6..
ownership of
0edf0..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMbGi..
/
adc2b..
ownership of
012b8..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMQV5..
/
1d36e..
ownership of
c2b81..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMPKv..
/
44a71..
ownership of
eda78..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMYGX..
/
679dd..
ownership of
9c421..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMPXo..
/
84a00..
ownership of
3c36e..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMcXU..
/
2e6dc..
ownership of
859f0..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMHZ4..
/
0d21a..
ownership of
93311..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMGfV..
/
95589..
ownership of
dee82..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMbpS..
/
f1806..
ownership of
8b481..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMQRJ..
/
dfb48..
ownership of
ca0ee..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMadT..
/
c2d89..
ownership of
3b396..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMSqH..
/
39894..
ownership of
769c1..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMWTY..
/
b9522..
ownership of
fbf96..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMain..
/
8260c..
ownership of
f88df..
as obj with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMXhy..
/
0db1b..
ownership of
6d86b..
as obj with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
PUfcG..
/
5f3c4..
doc published by
Pr4zB..
Param
Sing
Sing
:
ι
→
ι
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Known
SingI
SingI
:
∀ x0 .
x0
∈
Sing
x0
Theorem
not_Empty_eq_Sing
:
∀ x0 .
0
=
Sing
x0
⟶
∀ x1 : ο .
x1
(proof)
Param
UPair
UPair
:
ι
→
ι
→
ι
Known
UPairI1
UPairI1
:
∀ x0 x1 .
x0
∈
UPair
x0
x1
Theorem
not_Empty_eq_UPair
:
∀ x0 x1 .
0
=
UPair
x0
x1
⟶
∀ x2 : ο .
x2
(proof)
Theorem
nIn_not_eq_Sing
:
∀ x0 x1 .
nIn
x0
x1
⟶
x1
=
Sing
x0
⟶
∀ x2 : ο .
x2
(proof)
Theorem
nIn_not_eq_UPair_1
:
∀ x0 x1 x2 .
nIn
x0
x2
⟶
x2
=
UPair
x0
x1
⟶
∀ x3 : ο .
x3
(proof)
Known
UPairI2
UPairI2
:
∀ x0 x1 .
x1
∈
UPair
x0
x1
Theorem
nIn_not_eq_UPair_2
:
∀ x0 x1 x2 .
nIn
x1
x2
⟶
x2
=
UPair
x0
x1
⟶
∀ x3 : ο .
x3
(proof)
Param
ordsucc
ordsucc
:
ι
→
ι
Param
setminus
setminus
:
ι
→
ι
→
ι
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
PowerI
PowerI
:
∀ x0 x1 .
x1
⊆
x0
⟶
x1
∈
prim4
x0
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
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
PowerE
PowerE
:
∀ x0 x1 .
x1
∈
prim4
x0
⟶
x1
⊆
x0
Theorem
In_Power_ordsucc_cases_impred
:
∀ x0 x1 .
x1
∈
prim4
(
ordsucc
x0
)
⟶
∀ x2 : ο .
(
x1
∈
prim4
x0
⟶
x2
)
⟶
(
x0
∈
x1
⟶
setminus
x1
(
Sing
x0
)
∈
prim4
x0
⟶
x2
)
⟶
x2
(proof)
Known
Power_0_Sing_0
Power_0_Sing_0
:
prim4
0
=
Sing
0
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Theorem
In_Power_0_eq_0
:
∀ x0 .
x0
∈
prim4
0
⟶
x0
=
0
(proof)
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
In_0_1
In_0_1
:
0
∈
1
Known
setminusI
setminusI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
nIn
x2
x1
⟶
x2
∈
setminus
x0
x1
Known
cases_1
cases_1
:
∀ x0 .
x0
∈
1
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
x0
Theorem
In_Power_1_cases_impred
:
∀ x0 .
x0
∈
prim4
1
⟶
∀ x1 : ο .
(
x0
=
0
⟶
x1
)
⟶
(
x0
=
1
⟶
x1
)
⟶
x1
(proof)
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Known
cases_2
cases_2
:
∀ x0 .
x0
∈
2
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
x0
Known
setminusE1
setminusE1
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
x2
∈
x0
Theorem
In_Power_2_cases_impred
:
∀ x0 .
x0
∈
prim4
2
⟶
∀ x1 : ο .
(
x0
=
0
⟶
x1
)
⟶
(
x0
=
1
⟶
x1
)
⟶
(
x0
=
Sing
1
⟶
x1
)
⟶
(
x0
=
2
⟶
x1
)
⟶
x1
(proof)
Known
cases_3
cases_3
:
∀ x0 .
x0
∈
3
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
2
⟶
x1
x0
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
neq_1_2
neq_1_2
:
1
=
2
⟶
∀ x0 : ο .
x0
Known
UPairE
UPairE
:
∀ x0 x1 x2 .
x0
∈
UPair
x1
x2
⟶
or
(
x0
=
x1
)
(
x0
=
x2
)
Known
neq_0_1
neq_0_1
:
0
=
1
⟶
∀ x0 : ο .
x0
Known
neq_0_2
neq_0_2
:
0
=
2
⟶
∀ x0 : ο .
x0
Known
In_0_2
In_0_2
:
0
∈
2
Known
In_1_2
In_1_2
:
1
∈
2
Theorem
In_Power_3_cases_impred
:
∀ x0 .
x0
∈
prim4
3
⟶
∀ x1 : ο .
(
x0
=
0
⟶
x1
)
⟶
(
x0
=
1
⟶
x1
)
⟶
(
x0
=
Sing
1
⟶
x1
)
⟶
(
x0
=
2
⟶
x1
)
⟶
(
x0
=
Sing
2
⟶
x1
)
⟶
(
x0
=
UPair
0
2
⟶
x1
)
⟶
(
x0
=
UPair
1
2
⟶
x1
)
⟶
(
x0
=
3
⟶
x1
)
⟶
x1
(proof)
Param
bij
bij
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Definition
equip
equip
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Definition
TwoRamseyProp
TwoRamseyProp
:=
λ x0 x1 x2 .
∀ x3 :
ι →
ι → ο
.
(
∀ x4 x5 .
x3
x4
x5
⟶
x3
x5
x4
)
⟶
or
(
∀ x4 : ο .
(
∀ x5 .
and
(
x5
⊆
x2
)
(
and
(
equip
x0
x5
)
(
∀ x6 .
x6
∈
x5
⟶
∀ x7 .
x7
∈
x5
⟶
(
x6
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
x3
x6
x7
)
)
⟶
x4
)
⟶
x4
)
(
∀ x4 : ο .
(
∀ x5 .
and
(
x5
⊆
x2
)
(
and
(
equip
x1
x5
)
(
∀ x6 .
x6
∈
x5
⟶
∀ x7 .
x7
∈
x5
⟶
(
x6
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
not
(
x3
x6
x7
)
)
)
⟶
x4
)
⟶
x4
)
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
Known
bij_inj
bij_inj
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
inj
x0
x1
x2
Theorem
equip_atleastp
equip_atleastp
:
∀ x0 x1 .
equip
x0
x1
⟶
atleastp
x0
x1
(proof)
Definition
TwoRamseyProp_atleastp
:=
λ x0 x1 x2 .
∀ x3 :
ι →
ι → ο
.
(
∀ x4 x5 .
x3
x4
x5
⟶
x3
x5
x4
)
⟶
or
(
∀ x4 : ο .
(
∀ x5 .
and
(
x5
⊆
x2
)
(
and
(
atleastp
x0
x5
)
(
∀ x6 .
x6
∈
x5
⟶
∀ x7 .
x7
∈
x5
⟶
(
x6
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
x3
x6
x7
)
)
⟶
x4
)
⟶
x4
)
(
∀ x4 : ο .
(
∀ x5 .
and
(
x5
⊆
x2
)
(
and
(
atleastp
x1
x5
)
(
∀ x6 .
x6
∈
x5
⟶
∀ x7 .
x7
∈
x5
⟶
(
x6
=
x7
⟶
∀ x8 : ο .
x8
)
⟶
not
(
x3
x6
x7
)
)
)
⟶
x4
)
⟶
x4
)
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Theorem
inj_comp
inj_comp
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι → ι
.
inj
x0
x1
x3
⟶
inj
x1
x2
x4
⟶
inj
x0
x2
(
λ x5 .
x4
(
x3
x5
)
)
(proof)
Known
equip_ref
equip_ref
:
∀ x0 .
equip
x0
x0
Theorem
atleastp_ref
:
∀ x0 .
atleastp
x0
x0
(proof)
Theorem
atleastp_tra
atleastp_tra
:
∀ x0 x1 x2 .
atleastp
x0
x1
⟶
atleastp
x1
x2
⟶
atleastp
x0
x2
(proof)
Theorem
Subq_atleastp
Subq_atleastp
:
∀ x0 x1 .
x0
⊆
x1
⟶
atleastp
x0
x1
(proof)
Param
nat_p
nat_p
:
ι
→
ο
Known
nat_trans
nat_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Theorem
nat_In_atleastp
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
atleastp
x1
x0
(proof)
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Theorem
TwoRamseyProp_atleastp_atleastp
:
∀ x0 x1 x2 x3 x4 .
TwoRamseyProp
x0
x2
x4
⟶
atleastp
x1
x0
⟶
atleastp
x3
x2
⟶
TwoRamseyProp_atleastp
x1
x3
x4
(proof)