Search for blocks/addresses/...
Proofgold Address
address
PUZeuXFkYVuUQAhE8MQLwu48emSAAj8KDJB
total
0
mg
-
conjpub
-
current assets
3b0cf..
/
693bc..
bday:
15602
doc published by
Pr4zB..
Param
nat_p
nat_p
:
ι
→
ο
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
ChurchNum_ii_6
:=
λ x0 :
(
ι → ι
)
→
ι → ι
.
λ x1 :
ι → ι
.
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
Definition
ChurchNum2
:=
λ x0 :
ι → ι
.
λ x1 .
x0
(
x0
x1
)
Known
f3785..
:
∀ x0 :
ι → ι
.
∀ x1 :
ι → ο
.
(
∀ x2 .
x1
x2
⟶
x1
(
x0
x2
)
)
⟶
∀ x2 .
x1
x2
⟶
x1
(
ChurchNum_ii_6
ChurchNum2
x0
x2
)
Known
nat_ordsucc
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Definition
ChurchNum_ii_5
:=
λ x0 :
(
ι → ι
)
→
ι → ι
.
λ x1 :
ι → ι
.
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
Known
9821b..
:
∀ x0 :
ι → ι
.
∀ x1 :
ι → ο
.
(
∀ x2 .
x1
x2
⟶
x1
(
x0
x2
)
)
⟶
∀ x2 .
x1
x2
⟶
x1
(
ChurchNum_ii_5
ChurchNum2
x0
x2
)
Known
nat_3
nat_3
:
nat_p
3
Theorem
5b6f8..
:
nat_p
99
(proof)
Param
add_nat
add_nat
:
ι
→
ι
→
ι
Definition
ChurchNum_ii_3
:=
λ x0 :
(
ι → ι
)
→
ι → ι
.
λ x1 :
ι → ι
.
x0
(
x0
(
x0
x1
)
)
Known
93d19..
:
∀ x0 :
ι → ι
.
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
(
∀ x3 .
x1
x3
⟶
x1
(
x0
x3
)
)
⟶
(
∀ x3 .
x1
x3
⟶
x2
(
x0
x3
)
=
x0
(
x2
x3
)
)
⟶
∀ x3 .
x1
x3
⟶
x2
(
ChurchNum_ii_5
ChurchNum2
x0
x3
)
=
ChurchNum_ii_5
ChurchNum2
x0
(
x2
x3
)
Known
add_nat_SR
add_nat_SR
:
∀ x0 x1 .
nat_p
x1
⟶
add_nat
x0
(
ordsucc
x1
)
=
ordsucc
(
add_nat
x0
x1
)
Known
nat_9
nat_9
:
nat_p
9
Known
69b84..
:
∀ x0 :
ι → ι
.
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
(
∀ x3 .
x1
x3
⟶
x1
(
x0
x3
)
)
⟶
(
∀ x3 .
x1
x3
⟶
x2
(
x0
x3
)
=
x0
(
x2
x3
)
)
⟶
∀ x3 .
x1
x3
⟶
x2
(
ChurchNum_ii_3
ChurchNum2
x0
x3
)
=
ChurchNum_ii_3
ChurchNum2
x0
(
x2
x3
)
Known
nat_1
nat_1
:
nat_p
1
Known
nat_0
nat_0
:
nat_p
0
Known
add_nat_0R
add_nat_0R
:
∀ x0 .
add_nat
x0
0
=
x0
Theorem
9280e..
:
add_nat
99
41
=
140
(proof)
Param
TwoRamseyProp
TwoRamseyProp
:
ι
→
ι
→
ι
→
ο
Param
TwoRamseyProp_atleastp
:
ι
→
ι
→
ι
→
ο
Known
97c7e..
:
∀ x0 x1 x2 x3 .
nat_p
x2
⟶
nat_p
x3
⟶
TwoRamseyProp_atleastp
(
ordsucc
x0
)
x1
x2
⟶
TwoRamseyProp_atleastp
x0
(
ordsucc
x1
)
x3
⟶
TwoRamseyProp
(
ordsucc
x0
)
(
ordsucc
x1
)
(
ordsucc
(
add_nat
x2
x3
)
)
Known
61d53..
:
nat_p
41
Param
atleastp
atleastp
:
ι
→
ι
→
ο
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
TwoRamseyProp_4_7_99
:
TwoRamseyProp
4
7
99
Known
atleastp_ref
:
∀ x0 .
atleastp
x0
x0
Known
TwoRamseyProp_3_8_41
:
TwoRamseyProp
3
8
41
Theorem
TwoRamseyProp_4_8_141
:
TwoRamseyProp
4
8
141
(proof)
Definition
ChurchNum_ii_8
:=
λ x0 :
(
ι → ι
)
→
ι → ι
.
λ x1 :
ι → ι
.
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
(
x0
x1
)
)
)
)
)
)
)
Definition
ChurchNum_ii_4
:=
λ x0 :
(
ι → ι
)
→
ι → ι
.
λ x1 :
ι → ι
.
x0
(
x0
(
x0
(
x0
x1
)
)
)
Known
b8288..
:
∀ x0 :
ι → ι
.
∀ x1 :
ι →
ι → ο
.
(
∀ x2 x3 .
x1
x3
x2
⟶
x1
x3
(
x0
x2
)
)
⟶
∀ x2 x3 .
x1
x3
x2
⟶
x1
x3
(
ChurchNum_ii_6
ChurchNum2
x0
x2
)
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
80fa6..
:
∀ x0 :
ι → ι
.
∀ x1 :
ι →
ι → ο
.
(
∀ x2 x3 .
x1
x3
x2
⟶
x1
x3
(
x0
x2
)
)
⟶
∀ x2 x3 .
x1
x3
x2
⟶
x1
x3
(
ChurchNum_ii_5
ChurchNum2
x0
x2
)
Known
8c01a..
:
∀ x0 :
ι → ι
.
∀ x1 :
ι →
ι → ο
.
(
∀ x2 x3 .
x1
x3
x2
⟶
x1
x3
(
x0
x2
)
)
⟶
∀ x2 x3 .
x1
x3
x2
⟶
x1
x3
(
ChurchNum_ii_4
ChurchNum2
x0
x2
)
Known
1b77a..
:
∀ x0 :
ι → ι
.
∀ x1 :
ι →
ι → ο
.
(
∀ x2 x3 .
x1
x3
x2
⟶
x1
x3
(
x0
x2
)
)
⟶
∀ x2 x3 .
x1
x3
x2
⟶
x1
x3
(
ChurchNum2
x0
x2
)
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Theorem
20b75..
:
141
∈
ChurchNum_ii_8
ChurchNum2
ordsucc
0
(proof)
Known
46dcf..
:
∀ x0 x1 x2 x3 .
atleastp
x2
x3
⟶
TwoRamseyProp
x0
x1
x2
⟶
TwoRamseyProp
x0
x1
x3
Param
exp_nat
exp_nat
:
ι
→
ι
→
ι
Known
atleastp_tra
atleastp_tra
:
∀ x0 x1 x2 .
atleastp
x0
x1
⟶
atleastp
x1
x2
⟶
atleastp
x0
x2
Known
bbc1b..
:
exp_nat
2
8
=
ChurchNum_ii_8
ChurchNum2
ordsucc
0
Known
nat_In_atleastp
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
atleastp
x1
x0
Known
28496..
:
nat_p
256
Param
equip
equip
:
ι
→
ι
→
ο
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
Known
293d3..
:
∀ x0 .
nat_p
x0
⟶
equip
(
prim4
x0
)
(
exp_nat
2
x0
)
Known
nat_8
nat_8
:
nat_p
8
Theorem
TwoRamseyProp_4_8_Power_8
TwoRamseyProp_4_8_Power_8
:
TwoRamseyProp
4
8
(
prim4
8
)
(proof)
previous assets