Proofgold Address

Param ChurchNum_3ary_proj_p : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο
Param ChurchNum_8ary_proj_p : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο
Param TwoRamseyGraph_4_5_24_ChurchNums_3x8 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ι → ι → ι
Param ChurchNums_3x8_to_u24 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ι
Definition False^False := ∀ x0 : ο . x0
Known 01925.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 x0 x2 = ChurchNums_3x8_to_u24 x1 x3 ⟶ False
Param ChurchNums_8x3_to_3_lt7_id_ge7_rot2 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)
Param ChurchNums_8_perm_1_2_3_4_5_6_7_0 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)
Known d7bcc.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) = ChurchNums_3x8_to_u24 x1 x3 ⟶ False
Known b428c.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 x1) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3) ⟶ False
Param ChurchNums_8x3_to_3_lt6_id_ge6_rot2 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)
Param ChurchNums_8_perm_2_3_4_5_6_7_0_1 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)
Known 7787a.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) = ChurchNums_3x8_to_u24 x1 x3 ⟶ False
Known f0975.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 x1) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3) ⟶ False
Known 28750.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x3 x1) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x3) ⟶ False
Param ChurchNums_8x3_to_3_lt5_id_ge5_rot2 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)
Param ChurchNums_8_perm_3_4_5_6_7_0_1_2 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)
Known b9a6b.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 x1) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3) ⟶ False
Known e5001.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x3 x1) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x3) ⟶ False
Known 09666.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x3 x1) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x3) ⟶ False
Param ChurchNums_8x3_to_3_lt4_id_ge4_rot2 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)
Param ChurchNums_8_perm_4_5_6_7_0_1_2_3 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)
Known 74048.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) = ChurchNums_3x8_to_u24 x1 x3 ⟶ False
Known f9a56.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x3 x1) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x3) ⟶ False
Known 9b117.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x3 x1) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x3) ⟶ False
Known 9fd37.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x3 x1) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x3) ⟶ False
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 85ac5.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 x1 x3 ⟶ and (x1 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (x3 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2)
Known bae77.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 x1) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3) ⟶ and (x1 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (x3 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2)
Param ap^ap : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Known 99cbf.. : ∀ x0 x1 x2 x3 x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x5 x6 x7 x8 x9 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_3ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x5 ⟶ ChurchNum_8ary_proj_p x6 ⟶ ChurchNum_8ary_proj_p x7 ⟶ ChurchNum_8ary_proj_p x8 ⟶ ChurchNum_8ary_proj_p x9 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x1 x6 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x2 x7 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x2 x7 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x3 x8 x4 x9 = λ x11 x12 . x12) ⟶ ∀ x10 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ι . (∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) 0 = ChurchNums_3x8_to_u24 x11 x12) ⟶ (∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) u1 = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x12 x11) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x12)) ⟶ (∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) u2 = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x12 x11) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x12)) ⟶ (∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) u3 = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x12 x11) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x12)) ⟶ (∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) u4 = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x12 x11) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x12)) ⟶ (∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x11 ⟶ ChurchNum_8ary_proj_p x12 ⟶ ∀ x13 . x13 ∈ u5 ⟶ ∀ x14 . x14 ∈ u5 ⟶ ap (x10 x11 x12) x13 = ap (x10 x11 x12) x14 ⟶ x13 = x14) ⟶ (∀ x11 x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x13 x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x11 ⟶ ChurchNum_8ary_proj_p x13 ⟶ ChurchNum_3ary_proj_p x12 ⟶ ChurchNum_8ary_proj_p x14 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x11 x13 x12 x14 = λ x16 x17 . x17) ⟶ ∀ x15 . x15 ∈ u5 ⟶ ∀ x16 . x16 ∈ u5 ⟶ ap (x10 x11 x13) x15 = ap (x10 x12 x14) x16 ⟶ ∀ x17 : ο . (x12 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x13 x11 ⟶ x14 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x13 ⟶ x17) ⟶ (x11 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x14 x12 ⟶ x13 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x14 ⟶ x17) ⟶ x17) ⟶ False
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Param ordinal^ordinal : ι → ο
Known ordinal_trichotomy_or_impred^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (x0 ∈ x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (x1 ∈ x0 ⟶ x2) ⟶ x2
Param nat_p^nat_p : ι → ο
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known nat_p_trans^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Known nat_5^nat_5 : nat_p 5
Known f60cd.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x3 x0 x2
Known cases_5^cases_5 : ∀ x0 . x0 ∈ 5 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 x0
Known tuple_5_0_eq^tuple_5_0_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 0 = x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known tuple_5_1_eq^tuple_5_1_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 1 = x1
Known tuple_5_2_eq^tuple_5_2_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 2 = x2
Known tuple_5_3_eq^tuple_5_3_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 3 = x3
Known tuple_5_4_eq^tuple_5_4_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 4 = x4
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known cases_1^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Known cases_2^cases_2 : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Known cases_3^cases_3 : ∀ x0 . x0 ∈ 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
Known cases_4^cases_4 : ∀ x0 . x0 ∈ 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Known 8f0b2.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x1 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x1) = ChurchNums_3x8_to_u24 x0 x1 ⟶ ∀ x2 : ο . x2
Known 7bf94.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x1 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x1) = ChurchNums_3x8_to_u24 x0 x1 ⟶ ∀ x2 : ο . x2
Known 471b2.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x1 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x1 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x1) ⟶ ∀ x2 : ο . x2
Known a9b55.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) = ChurchNums_3x8_to_u24 x0 x1 ⟶ ∀ x2 : ο . x2
Known 08b75.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x1 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x1) ⟶ ∀ x2 : ο . x2
Known 373fc.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x1 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x1) ⟶ ∀ x2 : ο . x2
Known d6534.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 x0 x1 ⟶ ∀ x2 : ο . x2
Known 83ebc.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x1 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x1) ⟶ ∀ x2 : ο . x2
Known 290ad.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x1 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x1) ⟶ ∀ x2 : ο . x2
Known 987aa.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) ⟶ ∀ x2 : ο . x2
Theorem 165ef.. : ∀ x0 x1 x2 x3 x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x5 x6 x7 x8 x9 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_3ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x5 ⟶ ChurchNum_8ary_proj_p x6 ⟶ ChurchNum_8ary_proj_p x7 ⟶ ChurchNum_8ary_proj_p x8 ⟶ ChurchNum_8ary_proj_p x9 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x1 x6 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x2 x7 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x2 x7 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x3 x8 x4 x9 = λ x11 x12 . x12) ⟶ False (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
Param atleastp^atleastp : ι → ι → ο
Definition TwoRamseyGraph_4_5_24 := λ x0 x1 . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_8ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x5 ⟶ x0 = x2 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))))))))))) ordsucc (x4 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . x7) (λ x7 : ι → ι . λ x8 . x7 (x7 x8)) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 x8))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 x8)))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 x8))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 x8)))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 x8))))))) ordsucc 0) ⟶ x1 = x3 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))))))))))) ordsucc (x5 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . x7) (λ x7 : ι → ι . λ x8 . x7 (x7 x8)) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 x8))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 x8)))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 x8))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 x8)))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 x8))))))) ordsucc 0) ⟶ TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x4 x3 x5 = λ x7 x8 . x7
Known 3ed86.. : ∀ x0 . atleastp u5 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x5 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x1) ⟶ x1
Known 4f390.. : ∀ x0 . x0 ∈ u24 ⟶ ∀ x1 : ο . (∀ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ x0 = x2 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))))))))))) ordsucc (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x5 (x5 x6)) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 x6))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 x6)))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 x6))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 x6)))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 x6))))))) ordsucc 0) ⟶ x1) ⟶ x1
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known 7f11d.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ or (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x5) (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = λ x5 x6 . x6)
Known bebde.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ x0 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))))))))))) ordsucc (x2 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x5 (x5 x6)) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 x6))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 x6)))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 x6))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 x6)))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 x6))))))) ordsucc 0) = x1 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 (x5 x6)))))))))))))))) ordsucc (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x5 (x5 x6)) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 x6))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 x6)))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 x6))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 x6)))))) (λ x5 : ι → ι . λ x6 . x5 (x5 (x5 (x5 (x5 (x5 (x5 x6))))))) ordsucc 0) ⟶ and (x0 = x1) (x2 = x3)
Theorem 6af4c.. : ∀ x0 . x0 ⊆ u24 ⟶ atleastp u5 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_4_5_24 x1 x2)) (proof)
Definition TwoRamseyProp_atleastp := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5 ⟶ x3 x5 x4) ⟶ or (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x0 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x3 x6 x7)) ⟶ x4) ⟶ x4) (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x1 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ not (x3 x6 x7))) ⟶ x4) ⟶ x4)
Known 9303b.. : ∀ x0 x1 . TwoRamseyGraph_4_5_24 x0 x1 ⟶ TwoRamseyGraph_4_5_24 x1 x0
Known 51a60.. : ∀ x0 . x0 ⊆ u24 ⟶ atleastp u4 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_4_5_24 x1 x2)
Theorem not_TwoRamseyProp_atleast_4_5_24 : not (TwoRamseyProp_atleastp 4 5 24) (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Known TwoRamseyProp_atleastp_atleastp : ∀ x0 x1 x2 x3 x4 . TwoRamseyProp x0 x2 x4 ⟶ atleastp x1 x0 ⟶ atleastp x3 x2 ⟶ TwoRamseyProp_atleastp x1 x3 x4
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Theorem not_TwoRamseyProp_4_5_24^{not_TwoRamseyProp_4_5_24} : not (TwoRamseyProp 4 5 24) (proof)