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.

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

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

Assume H0: ChurchNum_3ary_proj_p x0.

Assume H1: ChurchNum_8ary_proj_p x5.

Assume H2: x1 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x5 x0.

Assume H3: x6 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x5.

Assume H4: ChurchNum_3ary_proj_p x2.

Assume H5: ChurchNum_3ary_proj_p x3.

Assume H6: ChurchNum_3ary_proj_p x4.

Assume H7: ChurchNum_8ary_proj_p x7.

Assume H8: ChurchNum_8ary_proj_p x8.

Assume H9: ChurchNum_8ary_proj_p x9.

Assume H10: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x2 x7 = λ x10 x11 . x11.

Assume H11: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x3 x8 = λ x10 x11 . x11.

Assume H12: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x4 x9 = λ x10 x11 . x11.

Assume H13: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x2 x7 = λ x10 x11 . x11.

Assume H14: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x3 x8 = λ x10 x11 . x11.

Assume H15: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x4 x9 = λ x10 x11 . x11.

Assume H16: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x3 x8 = λ x10 x11 . x11.

Assume H17: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x4 x9 = λ x10 x11 . x11.

Assume H18: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x3 x8 x4 x9 = λ x10 x11 . x11.

Apply unknownprop_9cee29baa93f11e013d65cf0e4ad7df4638b3ee96d47be7bf7654b5b77cac08d with x0, x5, False leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

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

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

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

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

Assume H19: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x15 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x14 ⟶ ChurchNum_8ary_proj_p x15 ⟶ ChurchNum_3ary_proj_p (x10 x15 x14).

Assume H20: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x15 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x14 ⟶ ChurchNum_8ary_proj_p x15 ⟶ ChurchNum_3ary_proj_p (x11 x15 x14).

Assume H21: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x15 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x15 ⟶ x10 x15 (x11 x15 x14) = x14.

Assume H22: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x15 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x15 ⟶ x11 x15 (x10 x15 x14) = x14.

Assume H23: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x14 ⟶ ChurchNum_8ary_proj_p (x12 x14).

Assume H24: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x14 ⟶ ChurchNum_8ary_proj_p (x13 x14).

Assume H25: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x12 (x13 x14) = x14.

Assume H26: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x13 (x12 x14) = x14.

Assume H27: ∀ x14 x15 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x16 x17 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x14 ⟶ ChurchNum_3ary_proj_p x15 ⟶ ChurchNum_8ary_proj_p x16 ⟶ ChurchNum_8ary_proj_p x17 ⟶ TwoRamseyGraph_4_5_24_ChurchNums_3x8 x14 x16 x15 x17 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (x10 x16 x14) (x12 x16) (x10 x17 x15) (x12 x17).

Assume H28: x10 x5 x0 = λ x14 x15 x16 : (ι → ι) → ι → ι . x14.

Assume H29: x12 x5 = λ x14 x15 x16 x17 x18 x19 x20 x21 : (ι → ι) → ι → ι . x14.

Assume H30: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x12 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x14) = ChurchNums_8_perm_3_4_5_6_7_0_1_2 (x12 x14).

Assume H31: ∀ x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x15 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x15 ⟶ x10 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x15) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x15 x14) = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (x12 x15) (x10 x15 x14).

Claim L32: ...

...

Claim L33: ...

...

Claim L34: ...

...

Claim L35: ...

...

Apply unknownprop_a5077f97daf85af0c0d4479eb111f3aab1bedc27313b4ddb24ec4a247a2c6f6c with x10 x7 x2, x10 x8 x3, x10 x9 x4, ..., ..., ... leaving 15 subgoals.

...

■

Proofgold Proof