Proofgold Asset

Param ChurchNum_3ary_proj_p : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο
Param ChurchNum_8ary_proj_p : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο
Param TwoRamseyGraph_4_5_24_ChurchNums_3x8 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Param ap^ap : ι → ι → ι
Definition False^False := ∀ x0 : ο . x0
Param lam^Sigma : ι → (ι → ι) → ι
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Param and^and : ο → ο → ο
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
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 nat_p^nat_p : ι → ο
Definition not^not := λ x0 : ο . x0 ⟶ False
Known 4fb58..^{Pigeonhole_not_atleastp_ordsucc} : ∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)
Known 73189.. : nat_p u24
Param mul_nat^mul_nat : ι → ι → ι
Definition u25 := ordsucc u24
Known c12f7.. : mul_nat u5 u5 = u25
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Param equip^equip : ι → ι → ο
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known a57cb.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ equip (mul_nat x0 x1) (setprod x0 x1)
Known nat_5^nat_5 : nat_p 5
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Param If_i^If_i : ο → ι → ι → ι
Known tuple_Sigma_eta^{tuple_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0)
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Known cases_5^cases_5 : ∀ x0 . x0 ∈ 5 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 x0
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known In_4_5^In_4_5 : 4 ∈ 5
Known In_3_5^In_3_5 : 3 ∈ 5
Known In_2_5^In_2_5 : 2 ∈ 5
Known In_1_5^In_1_5 : 1 ∈ 5
Known In_0_5^In_0_5 : 0 ∈ 5
Theorem cd8d1.. : ∀ 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 . x11 ∈ u5 ⟶ ∀ x12 . x12 ∈ u5 ⟶ ap (ap x10 x11) x12 ∈ 24) ⟶ (∀ x11 . x11 ∈ u5 ⟶ ∀ x12 . x12 ∈ u5 ⟶ ∀ x13 . x13 ∈ u5 ⟶ ap (ap x10 x11) x12 = ap (ap x10 x11) x13 ⟶ x12 = x13) ⟶ (∀ x11 . x11 ∈ u5 ⟶ ∀ x12 . x12 ∈ u5 ⟶ (x11 = x12 ⟶ ∀ x13 : ο . x13) ⟶ ∀ x13 . x13 ∈ u5 ⟶ ∀ x14 . x14 ∈ u5 ⟶ ap (ap x10 x11) x13 = ap (ap x10 x12) x14 ⟶ ∀ x15 : ο . x15) ⟶ False (proof)
Param ChurchNums_3x8_to_u24 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ι
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 (ι → ι)
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 (ι → ι)
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 (ι → ι)
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 (ι → ι)
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
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 neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
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 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_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 1b4dc.. : ∀ x0 x1 x2 x3 x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x5 x6 x7 x8 x9 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x5 ⟶ x1 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x5 x0 ⟶ x6 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x5 ⟶ ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_3ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x7 ⟶ ChurchNum_8ary_proj_p x8 ⟶ ChurchNum_8ary_proj_p x9 ⟶ (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
Known cases_2^cases_2 : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
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 cases_3^cases_3 : ∀ x0 . x0 ∈ 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
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 cases_4^cases_4 : ∀ x0 . x0 ∈ 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
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
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 16d18.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x1 ⟶ ChurchNums_3x8_to_u24 x0 x1 ∈ u24
Known 24233.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x0 x1)
Known dac10.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x0)
Known 7b754.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x0 x1)
Known eaaf4.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x0)
Known 2f553.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x0 x1)
Known c5de4.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x0)
Known 1aa1c.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x0 x1)
Known 4ac5f.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x0)
Theorem 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 (proof)