| ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . Loop x0 x1 x2 x3 x4 ⟶ ∀ x5 : ο . (binop_on x0 x1 ⟶ binop_on x0 x2 ⟶ binop_on x0 x3 ⟶ (∀ x6 . In x6 x0 ⟶ and (x1 x4 x6 = x6) (x1 x6 x4 = x6)) ⟶ (∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x0 ⟶ and (and (and (x2 x6 (x1 x6 x7) = x7) (x1 x6 (x2 x6 x7) = x7)) (x3 (x1 x6 x7) x7 = x6)) (x1 (x3 x6 x7) x7 = x6)) ⟶ x5) ⟶ x5 |
|