| ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ 8d7df.. x0 x1 x2 (bbc71.. x3 x4 x5 x6 x7 x8 x9 x10) = x6 |
|