Proofgold Asset

Param 4402e.. : ι → (ι → ι → ο) → ο
Param cf2df.. : ι → (ι → ι → ο) → ο
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param setminus^setminus : ι → ι → ι
Param Sing^Sing : ι → ι
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition 2f869.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ not (x0 x2 x3) ⟶ not (x0 x1 x4) ⟶ not (x0 x2 x4) ⟶ x0 x3 x4 ⟶ x5) ⟶ x5
Definition 87c36.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ x0 x2 x5 ⟶ not (x0 x3 x5) ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition 6648a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (87c36.. x0 x1 x2 x3 x4 x5 ⟶ (x1 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ not (x0 x1 x6) ⟶ x0 x2 x6 ⟶ x0 x3 x6 ⟶ not (x0 x4 x6) ⟶ not (x0 x5 x6) ⟶ x7) ⟶ x7
Definition 836ee.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (6648a.. x0 x1 x2 x3 x4 x5 x6 ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ x0 x1 x7 ⟶ not (x0 x2 x7) ⟶ not (x0 x3 x7) ⟶ not (x0 x4 x7) ⟶ x0 x5 x7 ⟶ x0 x6 x7 ⟶ x8) ⟶ x8
Definition 725c8.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (836ee.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ x0 x1 x8 ⟶ not (x0 x2 x8) ⟶ not (x0 x3 x8) ⟶ not (x0 x4 x8) ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition 79ee1.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (725c8.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ x0 x2 x9 ⟶ not (x0 x3 x9) ⟶ x0 x4 x9 ⟶ not (x0 x5 x9) ⟶ not (x0 x6 x9) ⟶ not (x0 x7 x9) ⟶ not (x0 x8 x9) ⟶ x10) ⟶ x10
Definition 8b6ad.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ not (x0 x2 x3) ⟶ not (x0 x1 x4) ⟶ not (x0 x2 x4) ⟶ not (x0 x3 x4) ⟶ x5) ⟶ x5
Definition 62523.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (8b6ad.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ not (x0 x2 x5) ⟶ not (x0 x3 x5) ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition fba9e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (62523.. x0 x1 x2 x3 x4 x5 ⟶ (x1 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ not (x0 x1 x6) ⟶ x0 x2 x6 ⟶ x0 x3 x6 ⟶ not (x0 x4 x6) ⟶ not (x0 x5 x6) ⟶ x7) ⟶ x7
Definition 99de9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (fba9e.. x0 x1 x3 x4 x2 x6 x5 ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ x0 x1 x7 ⟶ not (x0 x2 x7) ⟶ x0 x3 x7 ⟶ x0 x4 x7 ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8
Definition 771b4.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (99de9.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ x0 x1 x8 ⟶ not (x0 x2 x8) ⟶ not (x0 x3 x8) ⟶ x0 x4 x8 ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition aa64f.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (771b4.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ not (x0 x1 x9) ⟶ not (x0 x2 x9) ⟶ x0 x3 x9 ⟶ not (x0 x4 x9) ⟶ not (x0 x5 x9) ⟶ x0 x6 x9 ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition e26ca.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (aa64f.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ not (x0 x8 x10) ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition c5756.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (8b6ad.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ not (x0 x2 x5) ⟶ x0 x3 x5 ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition 2de86.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (c5756.. x0 x1 x2 x3 x4 x5 ⟶ (x1 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ not (x0 x1 x6) ⟶ x0 x2 x6 ⟶ not (x0 x3 x6) ⟶ x0 x4 x6 ⟶ not (x0 x5 x6) ⟶ x7) ⟶ x7
Definition 36d58.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (2de86.. x0 x1 x2 x3 x4 x5 x6 ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ x0 x1 x7 ⟶ not (x0 x2 x7) ⟶ x0 x3 x7 ⟶ x0 x4 x7 ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8
Definition af16d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (36d58.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ not (x0 x1 x8) ⟶ not (x0 x2 x8) ⟶ not (x0 x3 x8) ⟶ x0 x4 x8 ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition a3794.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (af16d.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ not (x0 x2 x9) ⟶ x0 x3 x9 ⟶ not (x0 x4 x9) ⟶ not (x0 x5 x9) ⟶ x0 x6 x9 ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 4e84e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a3794.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ not (x0 x8 x10) ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 723e0.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (771b4.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ not (x0 x1 x9) ⟶ not (x0 x2 x9) ⟶ x0 x3 x9 ⟶ not (x0 x4 x9) ⟶ not (x0 x5 x9) ⟶ not (x0 x6 x9) ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition abccc.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (723e0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ x0 x6 x10 ⟶ not (x0 x7 x10) ⟶ not (x0 x8 x10) ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 796c4.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (2de86.. x0 x1 x2 x3 x4 x5 x6 ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ x0 x1 x7 ⟶ not (x0 x2 x7) ⟶ x0 x3 x7 ⟶ not (x0 x4 x7) ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8
Definition d7cce.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (796c4.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ not (x0 x1 x8) ⟶ not (x0 x2 x8) ⟶ not (x0 x3 x8) ⟶ x0 x4 x8 ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition 58722.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (d7cce.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ x0 x2 x9 ⟶ not (x0 x3 x9) ⟶ not (x0 x4 x9) ⟶ x0 x5 x9 ⟶ not (x0 x6 x9) ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 1a8a9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (58722.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 9ab74.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (58722.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 3819d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (2de86.. x0 x1 x2 x3 x4 x5 x6 ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ x0 x1 x7 ⟶ x0 x2 x7 ⟶ x0 x3 x7 ⟶ not (x0 x4 x7) ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8
Definition 1b79b.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (3819d.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ not (x0 x1 x8) ⟶ not (x0 x2 x8) ⟶ x0 x3 x8 ⟶ not (x0 x4 x8) ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition 8c9ed.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (1b79b.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ not (x0 x2 x9) ⟶ not (x0 x3 x9) ⟶ not (x0 x4 x9) ⟶ x0 x5 x9 ⟶ not (x0 x6 x9) ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 53b49.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (8c9ed.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition f8709.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (c5756.. x0 x1 x2 x3 x4 x5 ⟶ (x1 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ not (x0 x1 x6) ⟶ x0 x2 x6 ⟶ x0 x3 x6 ⟶ x0 x4 x6 ⟶ not (x0 x5 x6) ⟶ x7) ⟶ x7
Definition 16c0f.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (f8709.. x0 x1 x2 x3 x4 x5 x6 ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ x0 x1 x7 ⟶ x0 x2 x7 ⟶ not (x0 x3 x7) ⟶ x0 x4 x7 ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8
Definition cc0ce.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (16c0f.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ not (x0 x1 x8) ⟶ x0 x2 x8 ⟶ not (x0 x3 x8) ⟶ not (x0 x4 x8) ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition 70a3c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (cc0ce.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ not (x0 x2 x9) ⟶ not (x0 x3 x9) ⟶ not (x0 x4 x9) ⟶ not (x0 x5 x9) ⟶ x0 x6 x9 ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition f982a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (70a3c.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ x0 x3 x10 ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition aa035.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (99de9.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ not (x0 x1 x8) ⟶ not (x0 x2 x8) ⟶ not (x0 x3 x8) ⟶ x0 x4 x8 ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition 22b3a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (aa035.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ not (x0 x2 x9) ⟶ not (x0 x3 x9) ⟶ not (x0 x4 x9) ⟶ x0 x5 x9 ⟶ x0 x6 x9 ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 9f4c9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (22b3a.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 7e5de.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (af16d.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ not (x0 x2 x9) ⟶ not (x0 x3 x9) ⟶ not (x0 x4 x9) ⟶ x0 x5 x9 ⟶ x0 x6 x9 ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 218e4.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (7e5de.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition d2827.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (36d58.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ not (x0 x1 x8) ⟶ not (x0 x2 x8) ⟶ x0 x3 x8 ⟶ not (x0 x4 x8) ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition 915dd.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (d2827.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ not (x0 x2 x9) ⟶ not (x0 x3 x9) ⟶ not (x0 x4 x9) ⟶ x0 x5 x9 ⟶ x0 x6 x9 ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 6d791.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (915dd.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 8acce.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (d7cce.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ not (x0 x2 x9) ⟶ x0 x3 x9 ⟶ not (x0 x4 x9) ⟶ not (x0 x5 x9) ⟶ x0 x6 x9 ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 77953.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (8acce.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 37e04.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (1b79b.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ x0 x1 x9 ⟶ not (x0 x2 x9) ⟶ not (x0 x3 x9) ⟶ not (x0 x4 x9) ⟶ x0 x5 x9 ⟶ x0 x6 x9 ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 97406.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (37e04.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 55171.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (7e5de.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 24120.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (d7cce.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ not (x0 x1 x9) ⟶ x0 x2 x9 ⟶ not (x0 x3 x9) ⟶ not (x0 x4 x9) ⟶ x0 x5 x9 ⟶ not (x0 x6 x9) ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 77203.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (24120.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ x0 x6 x10 ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 21422.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (2de86.. x0 x1 x2 x3 x4 x5 x6 ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ x0 x1 x7 ⟶ not (x0 x2 x7) ⟶ x0 x3 x7 ⟶ not (x0 x4 x7) ⟶ not (x0 x5 x7) ⟶ x0 x6 x7 ⟶ x8) ⟶ x8
Definition f0d5b.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (21422.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ not (x0 x1 x8) ⟶ not (x0 x2 x8) ⟶ not (x0 x3 x8) ⟶ x0 x4 x8 ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition 72e0a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (f0d5b.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ not (x0 x1 x9) ⟶ x0 x2 x9 ⟶ not (x0 x3 x9) ⟶ not (x0 x4 x9) ⟶ not (x0 x5 x9) ⟶ not (x0 x6 x9) ⟶ x0 x7 x9 ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 93e63.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (72e0a.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 182cc.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (f8709.. x0 x1 x2 x3 x4 x5 x6 ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ x0 x1 x7 ⟶ x0 x2 x7 ⟶ not (x0 x3 x7) ⟶ not (x0 x4 x7) ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8
Definition 84d5a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (182cc.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ not (x0 x1 x8) ⟶ x0 x2 x8 ⟶ not (x0 x3 x8) ⟶ not (x0 x4 x8) ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition 2e1d5.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (84d5a.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ not (x0 x1 x9) ⟶ not (x0 x2 x9) ⟶ x0 x3 x9 ⟶ x0 x4 x9 ⟶ not (x0 x5 x9) ⟶ not (x0 x6 x9) ⟶ x0 x7 x9 ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition d833d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (2e1d5.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ x0 x6 x10 ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 0314a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (3819d.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ x0 x1 x8 ⟶ not (x0 x2 x8) ⟶ not (x0 x3 x8) ⟶ x0 x4 x8 ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition a2064.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (0314a.. x0 x1 x2 x3 x4 x5 x6 x7 x8 ⟶ (x1 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x2 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x3 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x4 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x9 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x9 ⟶ ∀ x11 : ο . x11) ⟶ not (x0 x1 x9) ⟶ not (x0 x2 x9) ⟶ x0 x3 x9 ⟶ not (x0 x4 x9) ⟶ not (x0 x5 x9) ⟶ not (x0 x6 x9) ⟶ not (x0 x7 x9) ⟶ x0 x8 x9 ⟶ x10) ⟶ x10
Definition 99903.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a2064.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ x0 x6 x10 ⟶ not (x0 x7 x10) ⟶ not (x0 x8 x10) ⟶ x0 x9 x10 ⟶ x11) ⟶ x11
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known e0f29.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ cf2df.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 79ee1.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ ∀ x13 : ο . (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ x2 x5 x3 ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ x2 x6 x3 ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ x2 x5 x3 ⟶ x2 x6 x3 ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ x2 x7 x3 ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ x2 x5 x3 ⟶ not (x2 x6 x3) ⟶ x2 x7 x3 ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ x2 x8 x3 ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ x2 x6 x3 ⟶ not (x2 x7 x3) ⟶ x2 x8 x3 ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ x2 x9 x3 ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ x2 x7 x3 ⟶ not (x2 x8 x3) ⟶ x2 x9 x3 ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ x2 x8 x3 ⟶ x2 x9 x3 ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ x2 x5 x3 ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ x2 x6 x3 ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ x2 x5 x3 ⟶ x2 x6 x3 ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ x2 x7 x3 ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ x2 x5 x3 ⟶ not (x2 x6 x3) ⟶ x2 x7 x3 ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ x2 x11 x3 ⟶ not (x2 x12 x3) ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ not (x2 x11 x3) ⟶ x2 x12 x3 ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ x2 x6 x3 ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ not (x2 x11 x3) ⟶ x2 x12 x3 ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ x2 x12 x3 ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ x2 x6 x3 ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ x2 x12 x3 ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ x2 x8 x3 ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ x2 x12 x3 ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ x2 x6 x3 ⟶ not (x2 x7 x3) ⟶ x2 x8 x3 ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ x2 x12 x3 ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ x2 x9 x3 ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ x2 x12 x3 ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ x2 x8 x3 ⟶ x2 x9 x3 ⟶ not (x2 x10 x3) ⟶ x2 x11 x3 ⟶ x2 x12 x3 ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ not (x2 x6 x3) ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ x2 x11 x3 ⟶ x2 x12 x3 ⟶ x13) ⟶ (not (x2 x4 x3) ⟶ not (x2 x5 x3) ⟶ x2 x6 x3 ⟶ not (x2 x7 x3) ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ x2 x10 x3 ⟶ x2 x11 x3 ⟶ x2 x12 x3 ⟶ x13) ⟶ x13
Known neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Theorem 5bfbe.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ cf2df.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ 79ee1.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ ∀ x13 : ο . (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ e26ca.. x2 x14 x3 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 4e84e.. x2 x14 x15 x16 x17 x18 x19 x20 x3 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ abccc.. x2 x14 x3 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 1a8a9.. x2 x3 x14 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 9ab74.. x2 x3 x14 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 53b49.. x2 x14 x3 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ f982a.. x2 x14 x15 x16 x3 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 9f4c9.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 218e4.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 6d791.. x2 x14 x15 x16 x17 x3 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 77953.. x2 x3 x14 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 97406.. x2 x14 x15 x16 x17 x3 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 55171.. x2 x14 x15 x16 x17 x3 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 77203.. x2 x3 x14 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 93e63.. x2 x14 x15 x3 x16 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ d833d.. x2 x14 x15 x16 x3 x17 x18 x19 x20 x21 x22 ⟶ x13) ⟶ (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ∀ x19 . x19 ∈ x0 ⟶ ∀ x20 . x20 ∈ x0 ⟶ ∀ x21 . x21 ∈ x0 ⟶ ∀ x22 . x22 ∈ x0 ⟶ 99903.. x2 x14 x15 x16 x17 x18 x3 x19 x20 x21 x22 ⟶ x13) ⟶ x13 (proof)