| ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ u12 ⟶ x1 x2 ∈ u12) ⟶ (∀ x2 . x2 ∈ u12 ⟶ ∀ x3 . x3 ∈ u12 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ (∀ x2 . x2 ∈ u12 ⟶ ∀ x3 . x3 ∈ u12 ⟶ x0 (x1 x2) (x1 x3) ⟶ x0 x2 x3) ⟶ x1 u9 = u8 ⟶ x1 u10 = u11 ⟶ x1 u11 = u9 ⟶ x0 u8 u11 ⟶ ∀ x2 . x2 ⊆ u12 ⟶ atleastp u5 x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x0 x3 x4)) ⟶ atleastp u2 (setminus x2 u8) ⟶ ∀ x3 : ο . (∀ x4 . x4 ⊆ u12 ⟶ atleastp u5 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u8 ∈ x4 ⟶ u9 ∈ x4 ⟶ x3) ⟶ (∀ x4 . x4 ⊆ u12 ⟶ atleastp u5 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u8 ∈ x4 ⟶ u10 ∈ x4 ⟶ x3) ⟶ (∀ x4 . x4 ⊆ u12 ⟶ atleastp u5 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u9 ∈ x4 ⟶ u10 ∈ x4 ⟶ x3) ⟶ x3 |
|