Claim L0: ...

...

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.

Assume H1: ChurchNum_3ary_proj_p x0.

Assume H2: ChurchNum_3ary_proj_p x1.

Assume H3: ChurchNum_8ary_proj_p x2.

Assume H4: ChurchNum_8ary_proj_p x3.

Assume H5: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 = λ x4 x5 . x4.

Assume H6: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 = λ x4 x5 . x4.

Apply unknownprop_2064d925adb7ad93ca392156fe7b0a7b799e0a1ed452f931aaf6d83e86b04609 with x0, x2, (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x4 x5 . x4) ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 ⟶ ChurchNums_3x8_neq x0 x2 x1 x3 ⟶ False leaving 14 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

The subproof is completed by applying H5.

Assume H7: x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4.

Assume H8: x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4.

Assume H9: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 = λ x4 x5 . x4.

Assume H10: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 = λ x4 x5 . x4.

Assume H11: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x4 x5 . x4.

Assume H12: ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2.

Apply H12 with ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) x1 x3 ⟶ ChurchNums_3x8_neq x0 x2 x1 x3 ⟶ False.

Apply unknownprop_489a19599530946830ae79502aec6ef7b2f064765691a3ca83405abd2ab867f4 with λ x4 x5 x6 : (ι → ι) → ι → ι . x4, x0, λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4, x2 leaving 2 subgoals.

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

The subproof is completed by applying H7 with λ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 x6 x5.

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

The subproof is completed by applying H8 with λ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 x6 x5.

Assume H7: x0 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4.

Assume H8: x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5.

Apply H7 with λ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x5 x2 = ... ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x3 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x5 x2 x1 x3 = λ x6 x7 . x6) ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x5 x2 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x5 x2 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x3 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x3 ⟶ ChurchNums_3x8_neq x5 x2 x1 x3 ⟶ False.

...

■

Proofgold Proof