| ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u16 ⟶ x1 x2 ∈ u16) ⟶ (∀ x2 . x2 ∈ u16 ⟶ ∀ x3 . x3 ∈ u16 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ (∀ x2 . x2 ∈ u16 ⟶ ∀ x3 . x3 ∈ u16 ⟶ x0 (x1 x2) (x1 x3) ⟶ x0 x2 x3) ⟶ (∀ x2 . x2 ∈ u16 ⟶ x1 (x1 (x1 (x1 x2))) = x2) ⟶ x1 u12 = u13 ⟶ x1 u13 = u14 ⟶ x1 u14 = u15 ⟶ x1 u15 = u12 ⟶ ∀ x2 . x2 ⊆ u16 ⟶ atleastp u6 x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x0 x3 x4)) ⟶ atleastp u2 (setminus x2 u12) ⟶ ∀ x3 : ο . (∀ x4 . x4 ⊆ u16 ⟶ atleastp u6 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u12 ∈ x4 ⟶ u13 ∈ x4 ⟶ x3) ⟶ (∀ x4 . x4 ⊆ u16 ⟶ atleastp u6 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u12 ∈ x4 ⟶ u14 ∈ x4 ⟶ x3) ⟶ x3 |
|