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

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

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

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

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

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

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

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

Assume H0: ChurchNum_3ary_proj_p x0.

Assume H1: ChurchNum_3ary_proj_p x1.

Assume H2: ChurchNum_3ary_proj_p x2.

Assume H3: ChurchNum_3ary_proj_p x3.

Assume H4: ChurchNum_8ary_proj_p x4.

Assume H5: ChurchNum_8ary_proj_p x5.

Assume H6: ChurchNum_8ary_proj_p x6.

Assume H7: ChurchNum_8ary_proj_p x7.

Assume H8: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x1 x5 = λ x8 x9 . x8.

Assume H9: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x2 x6 = λ x8 x9 . x8.

Assume H10: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x3 x7 = λ x8 x9 . x8.

Assume H11: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x5 x2 x6 = λ x8 x9 . x8.

Assume H12: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x5 x3 x7 = λ x8 x9 . x8.

Assume H13: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x6 x3 x7 = λ x8 x9 . x8.

Assume H14: ChurchNums_3x8_neq x0 x4 x1 x5.

Assume H15: ChurchNums_3x8_neq x0 x4 x2 x6.

Assume H16: ChurchNums_3x8_neq x0 x4 x3 x7.

Assume H17: ChurchNums_3x8_neq x1 x5 x2 x6.

Assume H18: ChurchNums_3x8_neq x1 x5 x3 x7.

Assume H19: ChurchNums_3x8_neq x2 x6 x3 x7.

Apply unknownprop_c8b48e9264a42277b6e74dadf293c790236658d06af14f3853a9f07edfcbcc1f with x0, x4, False leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H4.

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

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

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

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

Assume H20: ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x13 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x12 ⟶ ChurchNum_8ary_proj_p x13 ⟶ ChurchNum_3ary_proj_p (x8 x13 x12).

Assume H21: ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x13 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x12 ⟶ ChurchNum_8ary_proj_p x13 ⟶ ChurchNum_3ary_proj_p (x9 x13 x12).

Assume H22: ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x13 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x13 ⟶ x8 x13 (x9 x13 x12) = x12.

Assume H23: ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x13 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x13 ⟶ x9 x13 (x8 x13 x12) = x12.

Assume H24: ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x12 ⟶ ChurchNum_8ary_proj_p (x10 x12).

Assume H25: ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x12 ⟶ ChurchNum_8ary_proj_p (x11 x12).

Assume H26: ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x10 (x11 x12) = x12.

Assume H27: ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x11 (x10 x12) = x12.

Assume H28: ∀ x12 x13 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x14 x15 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x12 ⟶ ChurchNum_3ary_proj_p x13 ⟶ ChurchNum_8ary_proj_p x14 ⟶ ChurchNum_8ary_proj_p x15 ⟶ TwoRamseyGraph_4_5_24_ChurchNums_3x8 x12 x14 x13 x15 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (x8 x14 x12) (x10 x14) (x8 x15 x13) (x10 x15).

Assume H29: x8 x4 x0 = λ x12 x13 x14 : (ι → ι) → ι → ι . x12.

Assume H30: x10 x4 = λ x12 x13 x14 x15 x16 x17 x18 x19 : (ι → ι) → ι → ι . x12.

Claim L31: ...

...

Apply unknownprop_2f9b72be21372c8a8b7b42b3a40f7fef5656e1eaf0c273f4f463663a3e6320bc with x8 x5 x1, x8 x6 x2, x8 x7 x3, x10 x5, x10 x6, x10 x7 leaving 18 subgoals.

Apply H20 with x1, x5 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H5.

Apply H20 with x2, x6 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H6.

Apply H20 with x3, x7 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H7.

Apply H24 with x5.

The subproof is completed by applying H5.

Apply H24 with x6.

The subproof is completed by applying H6.

Apply H24 with x7.

The subproof is completed by applying H7.

Apply H29 with λ x12 x13 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 x12 (λ x14 x15 x16 x17 x18 x19 x20 x21 : (ι → ι) → ι → ι . x14) (x8 x5 x1) (x10 ...) = ....

...

■

Proofgold Proof