| ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ο . ∀ x8 : ι → ι → ι → ι → ι → ι → ι → ι . ∀ x9 . prim1 x9 (e5d4c.. x0 x1 x2 x3 x4 x5 x6 x7 x8) ⟶ ∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 (x1 x11)) (∀ x14 : ο . (∀ x15 . and (prim1 x15 (x2 x11 x13)) (∀ x16 : ο . (∀ x17 . and (prim1 x17 (x3 x11 x13 x15)) (∀ x18 : ο . (∀ x19 . and (prim1 x19 (x4 x11 x13 x15 x17)) (∀ x20 : ο . (∀ x21 . and (prim1 x21 (x5 x11 x13 x15 x17 x19)) (∀ x22 : ο . (∀ x23 . and (prim1 x23 (x6 x11 x13 x15 x17 x19 x21)) (and (x7 x11 x13 x15 x17 x19 x21 x23) (x9 = x8 x11 x13 x15 x17 x19 x21 x23)) ⟶ x22) ⟶ x22) ⟶ x20) ⟶ x20) ⟶ x18) ⟶ x18) ⟶ x16) ⟶ x16) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10 |
|