Beginning of Section
Eq
Variable
A :
SType
Definition.
We define
eq
to be
λx y :
A
⇒
∀Q :
A
→
A
→
prop
,
Q
x
y
→
Q
y
x
of type
A
→
A
→
prop
.
End of Section
Eq
Notation
. We use
=
as an infix operator with priority 502 and no associativity corresponding to applying term
eq
.
Beginning of Section
Ex
Variable
A :
SType
Definition.
We define
ex
to be
λQ :
A
→
prop
⇒
∀P :
prop
,
(
∀x :
A
,
Q
x
→
P
)
→
P
of type
(
A
→
prop
)
→
prop
.
End of Section
Ex
Notation
. We use
∃
x
...
y
[possibly with ascriptions] ,
B
as a binder notation corresponding to a term constructed using
ex
.
Primitive
. The name
Eps_i
is a term of type
(
set
→
prop
)
→
set
.
Primitive
. The name
Empty
is a term of type
set
.
Primitive
. The name
ordsucc
is a term of type
set
→
set
.
In Proofgold the corresponding term root is
65d883...
and object id is
1452f7...
Notation
. Natural numbers 0,1,2,... are notation for the terms formed using
Empty
as 0 and forming successors with
ordsucc
.
Primitive
. The name
nat_p
is a term of type
set
→
prop
.
In Proofgold the corresponding term root is
458be3...
and object id is
cfd8eb...
Primitive
. The name
add_nat
is a term of type
set
→
set
→
set
.
In Proofgold the corresponding term root is
afa8ae...
and object id is
29768b...
Notation
. We use
+
as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat
.
Primitive
. The name
TwoRamseyProp
is a term of type
set
→
set
→
set
→
prop
.
In Proofgold the corresponding term root is
c5d86c...
and object id is
faf73f...
Axiom.
(
TwoRamseyProp_2
) We take the following as an axiom:
∀n,
TwoRamseyProp
2
n
n
In Proofgold the corresponding term root is
0b333a...
and proposition id is
f0d6f8...
Axiom.
(
TwoRamseyProp_3_4_9
) We take the following as an axiom:
TwoRamseyProp
3
4
9
In Proofgold the corresponding term root is
d90d6a...
and proposition id is
8aad15...
Axiom.
(
nat_4
) We take the following as an axiom:
nat_p
4
In Proofgold the corresponding term root is
2c8e1a...
and proposition id is
69ffc3...
Axiom.
(
nat_8
) We take the following as an axiom:
nat_p
8
In Proofgold the corresponding term root is
18883c...
and proposition id is
f93125...
Axiom.
(
add_nat_8_4
) We take the following as an axiom:
8
+
4
=
12
In Proofgold the corresponding term root is
6cbf2c...
and proposition id is
69b67e...
Axiom.
(
TwoRamseyProp_bd
) We take the following as an axiom:
∀r s m n,
nat_p
m
→
nat_p
n
→
TwoRamseyProp
(
ordsucc
r
)
s
(
ordsucc
m
)
→
TwoRamseyProp
r
(
ordsucc
s
)
(
ordsucc
n
)
→
TwoRamseyProp
(
ordsucc
r
)
(
ordsucc
s
)
(
ordsucc
(
ordsucc
(
m
+
n
)
)
)
In Proofgold the corresponding term root is
8dc902...
and proposition id is
164da7...
Theorem.
(
TwoRamseyProp_3_5_14
)
TwoRamseyProp
3
5
14
In Proofgold the corresponding term root is
3e761f...
and proposition id is
9131ef...
Proof:
We will
prove
TwoRamseyProp
(
ordsucc
2
)
(
ordsucc
4
)
(
ordsucc
(
ordsucc
12
)
)
.
rewrite
the current goal using
add_nat_8_4
(from right to left).
We will
prove
TwoRamseyProp
(
ordsucc
2
)
(
ordsucc
4
)
(
ordsucc
(
ordsucc
(
8
+
4
)
)
)
.
Apply
TwoRamseyProp_bd
2
4
8
4
nat_8
nat_4
to the current goal.
We will
prove
TwoRamseyProp
(
ordsucc
2
)
4
(
ordsucc
8
)
.
We will
prove
TwoRamseyProp
3
4
9
.
An
exact
proof term for the current goal is
TwoRamseyProp_3_4_9
.
We will
prove
TwoRamseyProp
2
(
ordsucc
4
)
(
ordsucc
4
)
.
We will
prove
TwoRamseyProp
2
5
5
.
An
exact
proof term for the current goal is
TwoRamseyProp_2
5
.
∎