Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
TwoRamseyProp_atleastp
u3
u7
u22
.
Apply H0 with
0aea9..
,
False
leaving 3 subgoals.
The subproof is completed by applying unknownprop_96a32fd9f43e79f68a24c790eba723eba988ce44f9334847292dbeee309df6bd.
Assume H1:
∃ x0 .
and
(
x0
⊆
u22
)
(
and
(
atleastp
u3
x0
)
(
∀ x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
0aea9..
x1
x2
)
)
.
Apply H1 with
False
.
Let x0 of type
ι
be given.
Assume H2:
(
λ x1 .
and
(
x1
⊆
u22
)
(
and
(
atleastp
u3
x1
)
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
0aea9..
x2
x3
)
)
)
x0
.
Apply H2 with
False
.
Assume H3:
x0
⊆
u22
.
Assume H4:
and
(
atleastp
u3
x0
)
(
∀ x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
0aea9..
x1
x2
)
.
Apply H4 with
False
.
Apply unknownprop_2cdba3befbb3ac0bb5de4e7433413d0b60523ef3946ee0ea55a09f6f806951ff with
x0
.
The subproof is completed by applying H3.
Assume H1:
∃ x0 .
and
(
x0
⊆
u22
)
(
and
(
atleastp
u7
x0
)
(
∀ x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
not
(
0aea9..
x1
x2
)
)
)
.
Apply H1 with
False
.
Let x0 of type
ι
be given.
Assume H2:
(
λ x1 .
and
(
x1
⊆
u22
)
(
and
(
atleastp
u7
x1
)
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
not
(
0aea9..
x2
x3
)
)
)
)
x0
.
Apply H2 with
False
.
Assume H3:
x0
⊆
u22
.
Assume H4:
and
(
atleastp
u7
x0
)
(
∀ x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
not
(
0aea9..
x1
x2
)
)
.
Apply H4 with
False
.
Apply unknownprop_6cfdd63c2d9d446313a3c5a82b07386e9adc9fd066c1990ea617fed0c875963c with
x0
.
The subproof is completed by applying H3.
■