| ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ο . ∀ x6 : ι → ι → ι → ι → ι → ι . ∀ x7 . prim1 x7 (2aab0.. x0 x1 x2 x3 x4 x5 x6) ⟶ ∀ x8 : ο . (∀ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 (x1 x9)) (∀ x12 : ο . (∀ x13 . and (prim1 x13 (x2 x9 x11)) (∀ x14 : ο . (∀ x15 . and (prim1 x15 (x3 x9 x11 x13)) (∀ x16 : ο . (∀ x17 . and (prim1 x17 (x4 x9 x11 x13 x15)) (and (x5 x9 x11 x13 x15 x17) (x7 = x6 x9 x11 x13 x15 x17)) ⟶ x16) ⟶ x16) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8 |
|