Search for blocks/addresses/...
Proofgold Signed Transaction
vin
Pr8Ky..
/
0989b..
PUSDz..
/
dda7b..
vout
Pr8Ky..
/
c69be..
0.00 bars
TMG43..
/
b7c66..
negprop ownership controlledby
Pr4zB..
upto 0
TMYLS..
/
9f564..
negprop ownership controlledby
Pr4zB..
upto 0
TMK6i..
/
8d3d3..
ownership of
5b30a..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMNUw..
/
888d7..
ownership of
73633..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMV3L..
/
6424c..
ownership of
485cd..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
TMWsG..
/
899f7..
ownership of
1accb..
as prop with payaddr
Pr4zB..
rights free controlledby
Pr4zB..
upto 0
PUUKF..
/
481ed..
doc published by
Pr4zB..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Param
TwoRamseyProp
TwoRamseyProp
:
ι
→
ι
→
ι
→
ο
Param
ordsucc
ordsucc
:
ι
→
ι
Known
not_TwoRamseyProp_4_4_17
not_TwoRamseyProp_4_4_17
:
not
(
TwoRamseyProp
4
4
17
)
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
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Known
46dcf..
:
∀ x0 x1 x2 x3 .
atleastp
x2
x3
⟶
TwoRamseyProp
x0
x1
x2
⟶
TwoRamseyProp
x0
x1
x3
Known
atleastp_tra
atleastp_tra
:
∀ x0 x1 x2 .
atleastp
x0
x1
⟶
atleastp
x1
x2
⟶
atleastp
x0
x2
Param
equip
equip
:
ι
→
ι
→
ο
Known
equip_atleastp
equip_atleastp
:
∀ x0 x1 .
equip
x0
x1
⟶
atleastp
x0
x1
Param
exp_nat
exp_nat
:
ι
→
ι
→
ι
Known
db1de..
:
exp_nat
2
4
=
16
Param
nat_p
nat_p
:
ι
→
ο
Known
293d3..
:
∀ x0 .
nat_p
x0
⟶
equip
(
prim4
x0
)
(
exp_nat
2
x0
)
Known
nat_4
nat_4
:
nat_p
4
Known
nat_In_atleastp
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
atleastp
x1
x0
Known
nat_17
nat_17
:
nat_p
17
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Theorem
485cd..
not_TwoRamseyProp_4_4_Power_4
:
not
(
TwoRamseyProp
4
4
(
prim4
4
)
)
(proof)
Param
TwoRamseyProp_atleastp
:
ι
→
ι
→
ι
→
ο
Known
b8b19..
:
∀ x0 x1 x2 .
TwoRamseyProp_atleastp
x0
x1
x2
⟶
TwoRamseyProp
x0
x1
x2
Known
TwoRamseyProp_atleastp_atleastp
:
∀ x0 x1 x2 x3 x4 .
TwoRamseyProp
x0
x2
x4
⟶
atleastp
x1
x0
⟶
atleastp
x3
x2
⟶
TwoRamseyProp_atleastp
x1
x3
x4
Known
atleastp_ref
:
∀ x0 .
atleastp
x0
x0
Known
nat_5
nat_5
:
nat_p
5
Known
In_4_5
In_4_5
:
4
∈
5
Theorem
5b30a..
not_TwoRamseyProp_4_5_Power_4
:
not
(
TwoRamseyProp
4
5
(
prim4
4
)
)
(proof)