Let x0 of type ι be given.

Assume H0: x0 ⊆ u24.

Assume H1: atleastp u5 x0.

Assume H2: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_4_5_24 x1 x2).

Apply unknownprop_611d05f3c0e0aff033700ccf72b7ceaf4160dd0bd5dde16fbd4a43684d4061b2 with x0, False leaving 2 subgoals.

The subproof is completed by applying H1.

Let x1 of type ι be given.

Assume H3: x1 ∈ x0.

Let x2 of type ι be given.

Assume H4: x2 ∈ x0.

Let x3 of type ι be given.

Assume H5: x3 ∈ x0.

Let x4 of type ι be given.

Assume H6: x4 ∈ x0.

Let x5 of type ι be given.

Assume H7: x5 ∈ x0.

Assume H8: x1 = x2 ⟶ ∀ x6 : ο . x6.

Assume H9: x1 = x3 ⟶ ∀ x6 : ο . x6.

Assume H10: x1 = x4 ⟶ ∀ x6 : ο . x6.

Assume H11: x1 = x5 ⟶ ∀ x6 : ο . x6.

Assume H12: x2 = x3 ⟶ ∀ x6 : ο . x6.

Assume H13: x2 = x4 ⟶ ∀ x6 : ο . x6.

Assume H14: x2 = x5 ⟶ ∀ x6 : ο . x6.

Assume H15: x3 = x4 ⟶ ∀ x6 : ο . x6.

Assume H16: x3 = x5 ⟶ ∀ x6 : ο . x6.

Assume H17: x4 = x5 ⟶ ∀ x6 : ο . x6.

Claim L18: ...

...

Claim L19: ...

...

Claim L20: ...

...

Claim L21: ...

...

Claim L22: ...

...

Claim L23: ...

...

Claim L24: ...

...

Claim L25: ...

...

Claim L26: ...

...

Claim L27: ...

...

Apply unknownprop_71f021c030b388b031b0cb54393cd4b453c65667caa2e250dac00458eefad39c with x1, False leaving 2 subgoals.

Apply H0 with x1.

The subproof is completed by applying H3.

Let x6 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Let x7 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Assume H28: ChurchNum_3ary_proj_p x6.

Assume H29: ChurchNum_8ary_proj_p x7.

Assume H30: x1 = x6 (λ x8 : ι → ι . λ x9 . x9) (λ x8 : ι → ι . λ x9 . x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 x9)))))))) (λ x8 : ι → ι . λ x9 . x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 (x8 x9)))))))))))))))) ordsucc (x7 (λ x8 : ι → ι . λ x9 . x9) (λ x8 : ι → ι . x8) (λ x8 : ι → ι . λ x9 . x8 (x8 x9)) (λ x8 : ι → ι . λ x9 . x8 (x8 (x8 x9))) (λ x8 : ι → ι . λ x9 . x8 (x8 (x8 (x8 x9)))) (λ x8 : ι → ι . λ x9 . x8 (x8 (x8 (x8 (x8 x9))))) (λ x8 : ι → ι . λ x9 . x8 (x8 (x8 (x8 (x8 (x8 x9)))))) (λ x8 : ι → ι . λ x9 . x8 (x8 (x8 (x8 (x8 (x8 (x8 x9))))))) ordsucc 0).

Apply unknownprop_71f021c030b388b031b0cb54393cd4b453c65667caa2e250dac00458eefad39c with x2, False leaving 2 subgoals.

Apply H0 with x2.

The subproof is completed by applying H4.

Let x8 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Let x9 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Assume H31: ChurchNum_3ary_proj_p x8.

Assume H32: ChurchNum_8ary_proj_p x9.

Assume H33: x2 = x8 (λ x10 : ι → ι . λ x11 . x11) (λ x10 : ι → ι . λ x11 . x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 x11)))))))) (λ x10 : ι → ι . λ x11 . x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 (x10 x11)))))))))))))))) ordsucc (x9 (λ x10 : ι → ι . λ x11 . x11) (λ x10 : ι → ι . x10) (λ x10 : ι → ι . λ x11 . x10 (x10 x11)) (λ x10 : ι → ι . λ x11 . x10 ...) ... ... ... ... ... 0).

...

■

Proofgold Proof