Proofgold Address

Definition ChurchNum_3ary_proj_p := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ο . x1 (λ x2 x3 x4 : (ι → ι) → ι → ι . x2) ⟶ x1 (λ x2 x3 x4 : (ι → ι) → ι → ι . x3) ⟶ x1 (λ x2 x3 x4 : (ι → ι) → ι → ι . x4) ⟶ x1 x0
Definition ChurchNum_8ary_proj_p := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ x1 x0
Definition TwoRamseyGraph_4_5_24_ChurchNums_3x8 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x4 . x0 (x1 (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)))) (x1 (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)))) (x1 (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)))) (λ x5 . x4)
Definition ChurchNums_8x3_to_3_lt4_id_ge4_rot2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)
Definition ChurchNums_8_perm_4_5_6_7_0_1_2_3 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x0 x5 x6 x7 x8 x1 x2 x3 x4
Theorem 1bd40.. : ∀ 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 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x3 x1) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x3) (proof)