Search for blocks/addresses/...
Proofgold Proof
pf
Claim L0:
...
...
Let x0 of type
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
be given.
Let x1 of type
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
be given.
Let x2 of type
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
be given.
Let x3 of type
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
be given.
Assume H1:
Church6_p
x0
.
Assume H2:
Church6_lt4p
x1
.
Assume H3:
Church6_p
x2
.
Assume H4:
Church6_lt4p
x3
.
Apply H1 with
λ x4 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
(
TwoRamseyGraph_4_6_Church6_squared_a
x4
x1
x2
x3
=
λ x5 x6 .
x5
)
⟶
TwoRamseyGraph_4_6_Church6_squared_a
x4
(
permargs_i_3_2_1_0_4_5
x1
)
x2
(
permargs_i_3_2_1_0_4_5
x3
)
=
λ x5 x6 .
x5
leaving 6 subgoals.
Apply H2 with
λ x4 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
(
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
x4
x2
x3
=
λ x5 x6 .
x5
)
⟶
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
x4
)
x2
(
permargs_i_3_2_1_0_4_5
x3
)
=
λ x5 x6 .
x5
leaving 4 subgoals.
Apply H3 with
λ x4 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
(
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
x4
x3
=
λ x5 x6 .
x5
)
⟶
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
)
x4
(
permargs_i_3_2_1_0_4_5
x3
)
=
λ x5 x6 .
x5
leaving 6 subgoals.
Apply H4 with
λ x4 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
(
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
x4
=
λ x5 x6 .
x5
)
⟶
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
)
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
x4
)
=
λ x5 x6 .
x5
leaving 4 subgoals.
Assume H5:
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
=
λ x4 x5 .
x4
.
Let x4 of type
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ο
be given.
Assume H6:
x4
(
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
)
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
)
)
(
λ x5 x6 .
x5
)
.
The subproof is completed by applying H6.
Assume H5:
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x5
)
=
λ x4 x5 .
x4
.
Apply FalseE with
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
permargs_i_3_2_1_0_4_5
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
permargs_i_3_2_1_0_4_5
(
λ x4 x5 x6 x7 x8 x9 .
x5
)
)
=
λ x4 x5 .
x4
.
Apply L0.
The subproof is completed by applying H5.
Assume H5:
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x6
)
=
λ x4 x5 .
x4
.
Let x4 of type
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ο
be given.
Assume H6:
x4
(
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
)
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
(
λ x5 x6 x7 x8 x9 x10 .
x7
)
)
)
(
λ x5 x6 .
x5
)
.
The subproof is completed by applying H6.
Assume H5:
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x7
)
=
λ x4 x5 .
x4
.
Apply FalseE with
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
permargs_i_3_2_1_0_4_5
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
permargs_i_3_2_1_0_4_5
(
λ x4 x5 x6 x7 x8 x9 .
x7
)
)
=
λ x4 x5 .
x4
.
Apply L0.
The subproof is completed by applying H5.
Apply H4 with
λ x4 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
(
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
λ x5 x6 x7 x8 x9 x10 .
x6
)
x4
=
λ x5 x6 .
x5
)
⟶
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
)
(
λ x5 x6 x7 x8 x9 x10 .
x6
)
(
permargs_i_3_2_1_0_4_5
x4
)
=
λ x5 x6 .
x5
leaving 4 subgoals.
Assume H5:
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
(
λ x4 x5 x6 x7 x8 x9 .
x5
)
(
λ x4 x5 x6 x7 x8 x9 .
x4
)
=
λ x4 x5 .
x4
.
Let x4 of type
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ο
be given.
Assume H6:
x4
(
TwoRamseyGraph_4_6_Church6_squared_a
(
λ x5 x6 x7 x8 x9 x10 .
x5
)
(
permargs_i_3_2_1_0_4_5
...
)
...
...
)
...
.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■