Proofgold Signed Transaction

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
Param ordsucc^ordsucc : ι → ι
Definition ChurchNums_3x8_to_u24 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x0 (x1 (λ x2 : ι → ι . λ x3 . x3) (λ x2 : ι → ι . x2) (λ x2 : ι → ι . λ x3 . x2 (x2 x3)) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 x3))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 x3)))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 x3))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 x3)))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 (x2 x3)))))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x1 (λ x4 : ι → ι . λ x5 . x5) (λ x4 : ι → ι . x4) (λ x4 : ι → ι . λ x5 . x4 (x4 x5)) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 x5))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 x5)))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 x5))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 x5)))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 x5))))))) x2 x3))))))))) (λ x2 : ι → ι . λ x3 . x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x2 (x1 (λ x4 : ι → ι . λ x5 . x5) (λ x4 : ι → ι . x4) (λ x4 : ι → ι . λ x5 . x4 (x4 x5)) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 x5))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 x5)))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 x5))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 x5)))))) (λ x4 : ι → ι . λ x5 . x4 (x4 (x4 (x4 (x4 (x4 (x4 x5))))))) x2 x3))))))))))))))))) ordsucc 0
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
Known a2126.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (x0 = λ x5 x6 x7 : (ι → ι) → ι → ι . x1 x6 x7 x5) ⟶ 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 ⟶ ∀ x4 : ο . x4
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 False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Known neq_4_3^neq_4_3 : u4 = u3 ⟶ ∀ x0 : ο . x0
Definition u5 := ordsucc u4
Known neq_5_4^neq_5_4 : u5 = u4 ⟶ ∀ x0 : ο . x0
Definition u6 := ordsucc u5
Known neq_6_4^neq_6_4 : u6 = u4 ⟶ ∀ x0 : ο . x0
Definition u7 := ordsucc u6
Known neq_7_4^neq_7_4 : u7 = u4 ⟶ ∀ x0 : ο . x0
Known neq_6_5^neq_6_5 : u6 = u5 ⟶ ∀ x0 : ο . x0
Known neq_7_5^neq_7_5 : u7 = u5 ⟶ ∀ x0 : ο . x0
Known neq_7_6^neq_7_6 : u7 = u6 ⟶ ∀ x0 : ο . x0
Known neq_7_0^neq_7_0 : u7 = 0 ⟶ ∀ x0 : ο . x0
Definition u8 := ordsucc u7
Known neq_8_1^neq_8_1 : u8 = u1 ⟶ ∀ x0 : ο . x0
Known neq_8_7^neq_8_7 : u8 = u7 ⟶ ∀ x0 : ο . x0
Definition u9 := ordsucc u8
Known neq_9_0^neq_9_0 : u9 = 0 ⟶ ∀ x0 : ο . x0
Known neq_9_2^neq_9_2 : u9 = u2 ⟶ ∀ x0 : ο . x0
Definition u10 := ordsucc u9
Known 0e10e.. : u10 = 0 ⟶ ∀ x0 : ο . x0
Known d183f.. : u10 = u1 ⟶ ∀ x0 : ο . x0
Known 68152.. : u10 = u3 ⟶ ∀ x0 : ο . x0
Definition u11 := ordsucc u10
Known 19f75.. : u11 = 0 ⟶ ∀ x0 : ο . x0
Known 618f7.. : u11 = u1 ⟶ ∀ x0 : ο . x0
Known 2c42c.. : u11 = u2 ⟶ ∀ x0 : ο . x0
Known 6a6f1.. : u11 = u4 ⟶ ∀ x0 : ο . x0
Known 33d16.. : u10 = u4 ⟶ ∀ x0 : ο . x0
Definition u12 := ordsucc u11
Known 7aa79.. : u12 = u4 ⟶ ∀ x0 : ο . x0
Definition u13 := ordsucc u12
Known 4d850.. : u13 = u4 ⟶ ∀ x0 : ο . x0
Definition u14 := ordsucc u13
Known ffd62.. : u14 = u4 ⟶ ∀ x0 : ο . x0
Known neq_8_5^neq_8_5 : u8 = u5 ⟶ ∀ x0 : ο . x0
Known 1b659.. : u11 = u5 ⟶ ∀ x0 : ο . x0
Known 07eba.. : u12 = u5 ⟶ ∀ x0 : ο . x0
Known 29333.. : u13 = u5 ⟶ ∀ x0 : ο . x0
Known d6c57.. : u14 = u5 ⟶ ∀ x0 : ο . x0
Definition u15 := ordsucc u14
Known 24fad.. : u15 = u5 ⟶ ∀ x0 : ο . x0
Known neq_8_6^neq_8_6 : u8 = u6 ⟶ ∀ x0 : ο . x0
Known neq_9_6^neq_9_6 : u9 = u6 ⟶ ∀ x0 : ο . x0
Known 0bd83.. : u12 = u6 ⟶ ∀ x0 : ο . x0
Known 02f5c.. : u13 = u6 ⟶ ∀ x0 : ο . x0
Known 62d80.. : u14 = u6 ⟶ ∀ x0 : ο . x0
Known f5ac7.. : u15 = u6 ⟶ ∀ x0 : ο . x0
Known neq_9_7^neq_9_7 : u9 = u7 ⟶ ∀ x0 : ο . x0
Known 7d7a8.. : u10 = u7 ⟶ ∀ x0 : ο . x0
Known d9b35.. : u13 = u7 ⟶ ∀ x0 : ο . x0
Known 01bf6.. : u14 = u7 ⟶ ∀ x0 : ο . x0
Known 008b1.. : u15 = u7 ⟶ ∀ x0 : ο . x0
Known neq_9_8^neq_9_8 : u9 = u8 ⟶ ∀ x0 : ο . x0
Known 96175.. : u10 = u8 ⟶ ∀ x0 : ο . x0
Known b3a20.. : u11 = u8 ⟶ ∀ x0 : ο . x0
Known 4f6ad.. : u14 = u8 ⟶ ∀ x0 : ο . x0
Known c0d75.. : u15 = u8 ⟶ ∀ x0 : ο . x0
Known 4fc31.. : u10 = u9 ⟶ ∀ x0 : ο . x0
Known 4f03f.. : u11 = u9 ⟶ ∀ x0 : ο . x0
Known 22885.. : u12 = u9 ⟶ ∀ x0 : ο . x0
Known 3a7bc.. : u15 = u9 ⟶ ∀ x0 : ο . x0
Known ebfb7.. : u11 = u10 ⟶ ∀ x0 : ο . x0
Known 6c583.. : u12 = u10 ⟶ ∀ x0 : ο . x0
Known 78358.. : u13 = u10 ⟶ ∀ x0 : ο . x0
Known ab306.. : u12 = u11 ⟶ ∀ x0 : ο . x0
Known bf497.. : u13 = u11 ⟶ ∀ x0 : ο . x0
Known 4e1aa.. : u14 = u11 ⟶ ∀ x0 : ο . x0
Known cef55.. : ChurchNum_3ary_proj_p (λ x0 x1 x2 : (ι → ι) → ι → ι . x0)
Known a5963.. : ChurchNum_3ary_proj_p (λ x0 x1 x2 : (ι → ι) → ι → ι . x2)
Known 18961.. : ChurchNum_3ary_proj_p (λ x0 x1 x2 : (ι → ι) → ι → ι . x1)
Known ad02f.. : u13 = u12 ⟶ ∀ x0 : ο . x0
Known ef4da.. : u14 = u12 ⟶ ∀ x0 : ο . x0
Known 72647.. : u15 = u12 ⟶ ∀ x0 : ο . x0
Known e1947.. : u14 = u13 ⟶ ∀ x0 : ο . x0
Known 4d8d4.. : u15 = u13 ⟶ ∀ x0 : ο . x0
Known b8e82.. : u15 = u14 ⟶ ∀ x0 : ο . x0
Definition u16 := ordsucc u15
Known 78b49.. : u16 = u9 ⟶ ∀ x0 : ο . x0
Known 41073.. : u16 = u15 ⟶ ∀ x0 : ο . x0
Definition u17 := ordsucc u16
Known dc9e6.. : u17 = u8 ⟶ ∀ x0 : ο . x0
Known 2e5d5.. : u17 = u10 ⟶ ∀ x0 : ο . x0
Definition u18 := ordsucc u17
Known d47e8.. : u18 = u8 ⟶ ∀ x0 : ο . x0
Known d3922.. : u18 = u9 ⟶ ∀ x0 : ο . x0
Known 8da43.. : u18 = u11 ⟶ ∀ x0 : ο . x0
Definition u19 := ordsucc u18
Known 9b462.. : u19 = u8 ⟶ ∀ x0 : ο . x0
Known 4545d.. : u19 = u9 ⟶ ∀ x0 : ο . x0
Known 7d160.. : u19 = u10 ⟶ ∀ x0 : ο . x0
Known a5243.. : u19 = u12 ⟶ ∀ x0 : ο . x0
Known c1bd9.. : u18 = u12 ⟶ ∀ x0 : ο . x0
Definition u20 := ordsucc u19
Known 01bb6.. : u20 = u12 ⟶ ∀ x0 : ο . x0
Definition u21 := ordsucc u20
Known 6371d.. : u21 = u12 ⟶ ∀ x0 : ο . x0
Definition u22 := ordsucc u21
Known db21d.. : u22 = u12 ⟶ ∀ x0 : ο . x0
Known 4326e.. : u16 = u13 ⟶ ∀ x0 : ο . x0
Known 8c598.. : u19 = u13 ⟶ ∀ x0 : ο . x0
Known 551bd.. : u20 = u13 ⟶ ∀ x0 : ο . x0
Known 87a9a.. : u21 = u13 ⟶ ∀ x0 : ο . x0
Known 6a662.. : u22 = u13 ⟶ ∀ x0 : ο . x0
Definition u23 := ordsucc u22
Known 4e72c.. : u23 = u13 ⟶ ∀ x0 : ο . x0
Known 71c5e.. : u16 = u14 ⟶ ∀ x0 : ο . x0
Known 82608.. : u17 = u14 ⟶ ∀ x0 : ο . x0
Known 28d21.. : u20 = u14 ⟶ ∀ x0 : ο . x0
Known 25d09.. : u21 = u14 ⟶ ∀ x0 : ο . x0
Known bd746.. : u22 = u14 ⟶ ∀ x0 : ο . x0
Known ef472.. : u23 = u14 ⟶ ∀ x0 : ο . x0
Known ac12b.. : u17 = u15 ⟶ ∀ x0 : ο . x0
Known dfba1.. : u18 = u15 ⟶ ∀ x0 : ο . x0
Known 17bc6.. : u21 = u15 ⟶ ∀ x0 : ο . x0
Known ac3f7.. : u22 = u15 ⟶ ∀ x0 : ο . x0
Known eff68.. : u23 = u15 ⟶ ∀ x0 : ο . x0
Known 7fbc8.. : u17 = u16 ⟶ ∀ x0 : ο . x0
Known 0eaf4.. : u18 = u16 ⟶ ∀ x0 : ο . x0
Known 0384c.. : u19 = u16 ⟶ ∀ x0 : ο . x0
Known e7d80.. : u22 = u16 ⟶ ∀ x0 : ο . x0
Known c26ad.. : u23 = u16 ⟶ ∀ x0 : ο . x0
Known 82c6a.. : u18 = u17 ⟶ ∀ x0 : ο . x0
Known 3c054.. : u19 = u17 ⟶ ∀ x0 : ο . x0
Known 9ce5b.. : u20 = u17 ⟶ ∀ x0 : ο . x0
Known e9a91.. : u23 = u17 ⟶ ∀ x0 : ο . x0
Known 97eb4.. : u19 = u18 ⟶ ∀ x0 : ο . x0
Known 75fad.. : u20 = u18 ⟶ ∀ x0 : ο . x0
Known 80a82.. : u21 = u18 ⟶ ∀ x0 : ο . x0
Known 2615b.. : u20 = u19 ⟶ ∀ x0 : ο . x0
Known 44711.. : u21 = u19 ⟶ ∀ x0 : ο . x0
Known b0147.. : u22 = u19 ⟶ ∀ x0 : ο . x0
Known c9329.. : u20 = u2 ⟶ ∀ x0 : ο . x0
Known 0af1b.. : u20 = u3 ⟶ ∀ x0 : ο . x0
Known f2a22.. : u20 = u4 ⟶ ∀ x0 : ο . x0
Known 98620.. : u20 = u5 ⟶ ∀ x0 : ο . x0
Known fd91d.. : u20 = u6 ⟶ ∀ x0 : ο . x0
Known 1158c.. : u21 = 0 ⟶ ∀ x0 : ο . x0
Known 272ed.. : u21 = u3 ⟶ ∀ x0 : ο . x0
Known ac7ac.. : u21 = u4 ⟶ ∀ x0 : ο . x0
Known 18fbb.. : u21 = u5 ⟶ ∀ x0 : ο . x0
Known 2ec13.. : u21 = u6 ⟶ ∀ x0 : ο . x0
Known 471c9.. : u21 = u7 ⟶ ∀ x0 : ο . x0
Known e8714.. : u22 = 0 ⟶ ∀ x0 : ο . x0
Known 9e7b1.. : u22 = u1 ⟶ ∀ x0 : ο . x0
Known 7f2f2.. : u22 = u4 ⟶ ∀ x0 : ο . x0
Known 9a712.. : u22 = u5 ⟶ ∀ x0 : ο . x0
Known f4b67.. : u22 = u6 ⟶ ∀ x0 : ο . x0
Known 362ec.. : u22 = u7 ⟶ ∀ x0 : ο . x0
Known c432c.. : u23 = 0 ⟶ ∀ x0 : ο . x0
Known 13d86.. : u23 = u1 ⟶ ∀ x0 : ο . x0
Known 60a3a.. : u23 = u2 ⟶ ∀ x0 : ο . x0
Known b1d7f.. : u23 = u5 ⟶ ∀ x0 : ο . x0
Known 51d86.. : u23 = u6 ⟶ ∀ x0 : ο . x0
Known 49af3.. : u23 = u7 ⟶ ∀ x0 : ο . x0
Known neq_1_0^neq_1_0 : u1 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_0^neq_2_0 : u2 = 0 ⟶ ∀ x0 : ο . x0
Known neq_3_0^neq_3_0 : u3 = 0 ⟶ ∀ x0 : ο . x0
Known neq_6_0^neq_6_0 : u6 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_1^neq_2_1 : u2 = u1 ⟶ ∀ x0 : ο . x0
Known neq_3_1^neq_3_1 : u3 = u1 ⟶ ∀ x0 : ο . x0
Known neq_4_1^neq_4_1 : u4 = u1 ⟶ ∀ x0 : ο . x0
Known neq_7_1^neq_7_1 : u7 = u1 ⟶ ∀ x0 : ο . x0
Known neq_3_2^neq_3_2 : u3 = u2 ⟶ ∀ x0 : ο . x0
Known neq_4_2^neq_4_2 : u4 = u2 ⟶ ∀ x0 : ο . x0
Known neq_5_2^neq_5_2 : u5 = u2 ⟶ ∀ x0 : ο . x0
Known neq_5_3^neq_5_3 : u5 = u3 ⟶ ∀ x0 : ο . x0
Known neq_6_3^neq_6_3 : u6 = u3 ⟶ ∀ x0 : ο . x0
Known 32e25.. : u21 = u20 ⟶ ∀ x0 : ο . x0
Known c8ac0.. : u22 = u20 ⟶ ∀ x0 : ο . x0
Known 94779.. : u23 = u20 ⟶ ∀ x0 : ο . x0
Known 41315.. : u22 = u21 ⟶ ∀ x0 : ο . x0
Known 1a616.. : u23 = u21 ⟶ ∀ x0 : ο . x0
Known 3105f.. : u23 = u22 ⟶ ∀ x0 : ο . x0
Known fcaf7.. : u17 = 0 ⟶ ∀ x0 : ο . x0
Known ab690.. : u16 = u1 ⟶ ∀ x0 : ο . x0
Known 9ccac.. : u18 = u1 ⟶ ∀ x0 : ο . x0
Known 296ac.. : u16 = u2 ⟶ ∀ x0 : ο . x0
Known 2c536.. : u17 = u2 ⟶ ∀ x0 : ο . x0
Known 81672.. : u19 = u2 ⟶ ∀ x0 : ο . x0
Known ca5c3.. : u16 = u3 ⟶ ∀ x0 : ο . x0
Known 6c299.. : u17 = u3 ⟶ ∀ x0 : ο . x0
Known 1f012.. : u18 = u3 ⟶ ∀ x0 : ο . x0
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Theorem 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 (proof)