| ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ο . ∀ x7 : ι → ι → ι → ι → ι → ι → ι . ∀ x8 . prim1 x8 (6cd44.. x0 x1 x2 x3 x4 x5 x6 x7) ⟶ ∃ x9 . and (prim1 x9 x0) (∃ x11 . and (prim1 x11 (x1 x9)) (∃ x13 . and (prim1 x13 (x2 x9 x11)) (∃ x15 . and (prim1 x15 (x3 x9 x11 x13)) (∃ x17 . and (prim1 x17 (x4 x9 x11 x13 x15)) (∃ x19 . and (prim1 x19 (x5 x9 x11 x13 x15 x17)) (and (x6 x9 x11 x13 x15 x17 x19) (x8 = x7 x9 x11 x13 x15 x17 x19))))))) |
|