| λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ι . λ x5 : ι → ι → ι → ι . λ x6 x7 : ι → ι . and (and (∀ x8 . x0 x8 ⟶ x3 (x4 (x4 (x4 x8))) (x4 (x4 x8)) (x4 x8) (x7 x8) (x5 (x4 (x4 x8)) (x4 x8) (x7 x8)) = x3 (x4 (x4 (x4 x8))) (x4 (x4 x8)) (x4 x8) (x7 x8) (x7 (x4 x8))) (∀ x8 . x0 x8 ⟶ x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x6 (x4 x8)) = x2 (x4 x8))) (∀ x8 . x0 x8 ⟶ x3 (x4 x8) (x4 (x4 x8)) (x4 x8) (x7 x8) (x5 x8 (x4 x8) (x6 x8)) = x2 (x4 x8)) |
|