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: a4ee9.. x0.

Assume H2: Church6_p x1.

Assume H3: a4ee9.. x2.

Assume H4: Church6_p x3.

Apply H1 with λ x4 : ι → ι → ι → ι → ι → ι → ι . (x4 = x2 ⟶ x1 = x3 ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_a x4 x1 x2 x3 = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_b x4 x1 x2 x3 = λ x5 x6 . x5 leaving 5 subgoals.

Apply H2 with λ x4 : ι → ι → ι → ι → ι → ι → ι . ((λ x5 x6 x7 x8 x9 x10 . x5) = x2 ⟶ x4 = x3 ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_a (λ x5 x6 x7 x8 x9 x10 . x5) x4 x2 x3 = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_b (λ x5 x6 x7 x8 x9 x10 . x5) x4 x2 x3 = λ x5 x6 . x5 leaving 6 subgoals.

Apply H3 with λ x4 : ι → ι → ι → ι → ι → ι → ι . ((λ x5 x6 x7 x8 x9 x10 . x5) = x4 ⟶ (λ x5 x6 x7 x8 x9 x10 . x5) = x3 ⟶ False) ⟶ (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_b (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x5) x4 x3 = λ x5 x6 . x5 leaving 5 subgoals.

Apply H4 with λ x4 : ι → ι → ι → ι → ι → ι → ι . (((λ x5 x6 x7 x8 x9 x10 . x5) = λ x5 x6 x7 x8 x9 x10 . x5) ⟶ (λ x5 x6 x7 x8 x9 x10 . x5) = x4 ⟶ False) ⟶ (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_b (λ 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 leaving 6 subgoals.

Assume H5: ((λ 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) ⟶ False.

Apply FalseE with (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) ⟶ TwoRamseyGraph_4_6_Church6_squared_b (λ 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.

Apply H5 leaving 2 subgoals.

Let x4 of type (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο be given.

Assume H6: x4 (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x5).

The subproof is completed by applying H6.

Let x4 of type (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο be given.

Assume H6: x4 (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x5).

The subproof is completed by applying H6.

Assume H5: ((λ 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) ⟶ False.

Assume H6: 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_b (λ 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 L0.

The subproof is completed by applying H6.

Assume H5: ((λ 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) ⟶ False.

Assume H6: 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 H7: x4 (TwoRamseyGraph_4_6_Church6_squared_b (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x7)) (λ x5 x6 . x5).

The subproof is completed by applying H7.

Assume H5: (λ x4 x5 x6 x7 x8 x9 . x4) = ... ⟶ ((λ x4 x5 x6 x7 x8 x9 . x4) = λ x4 x5 x6 x7 x8 x9 . x7) ⟶ False.

...

■

Proofgold Proof