| λ 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 |
|