| ∀ 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 ⟶ 02f3e.. x2 x4 x5 x6 x7 x8 x9 x10 ⟶ ∀ x11 : ο . (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 7676b.. x2 x12 x13 x14 x15 x16 x17 x18 x3 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ d98cb.. x2 x12 x13 x14 x15 x16 x3 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 0282b.. x2 x12 x13 x3 x14 x15 x16 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 00e1f.. x2 x3 x12 x13 x14 x15 x16 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ a5c5d.. x2 x12 x13 x14 x15 x16 x17 x18 x3 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ a6215.. x2 x12 x3 x13 x14 x15 x16 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ c8b10.. x2 x12 x13 x14 x15 x16 x17 x18 x3 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 5072f.. x2 x12 x13 x14 x15 x16 x3 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 662fb.. x2 x12 x13 x3 x14 x15 x16 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 599ac.. x2 x12 x13 x3 x14 x15 x16 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 33dd8.. x2 x12 x13 x14 x3 x15 x16 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ ec99f.. x2 x3 x12 x13 x14 x15 x16 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 6ea2b.. x2 x12 x13 x14 x15 x16 x17 x3 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 67161.. x2 x12 x13 x14 x15 x16 x17 x3 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 6caef.. x2 x12 x13 x14 x15 x16 x3 x17 x18 ⟶ x11) ⟶ x11 |
|