| ∀ 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) |
|