Proofgold Address

Known 1110b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x5 (x1 x7 (x1 x6 x8)))))
Theorem 20578.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x5 (x1 x8 (x1 x7 x6)))))
Theorem 9086f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x5 (x1 x8 (x1 x7 x6)))))
Theorem 0df93.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x5 (x1 x6 (x1 x8 x7)))))
Theorem 08ad0.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x5 (x1 x6 (x1 x8 x7)))))
Known 94aed.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x7 (x1 x5 x8)))))
Theorem 8287d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x8 (x1 x5 x7)))))
Theorem d6bd2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x8 (x1 x5 x7)))))
Known 45f87.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x1 x2 (x1 x3 (x1 x4 x5)) = x1 x3 (x1 x4 (x1 x2 x5))
Theorem 40852.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x8 (x1 x7 x5)))))
Theorem 7ad62.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x8 (x1 x7 x5)))))
Theorem a43a4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x7 (x1 x8 x5)))))
Theorem 3fff8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x7 (x1 x8 x5)))))
Known 98568.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x5 x7))))
Theorem acc8f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x5 (x1 x8 x7)))))
Theorem 05906.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x6 (x1 x5 (x1 x8 x7)))))
Theorem f9fad.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x7 (x1 x8 (x1 x5 x6)))))
Theorem 9931a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x7 (x1 x8 (x1 x5 x6)))))
Theorem cc73e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x7 (x1 x8 (x1 x6 x5)))))
Theorem a77e9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x7 (x1 x8 (x1 x6 x5)))))
Theorem 28262.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x7 (x1 x6 (x1 x8 x5)))))
Theorem 16a21.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x7 (x1 x6 (x1 x8 x5)))))
Known 3326a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x7 (x1 x6 (x1 x5 x8)))))
Theorem 33984.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x8 (x1 x7 (x1 x6 x5)))))
Theorem fac9c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x8 (x1 x7 (x1 x6 x5)))))
Theorem a3840.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x8 (x1 x6 (x1 x7 x5)))))
Theorem dcd10.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x2 (x1 x4 (x1 x8 (x1 x6 (x1 x7 x5)))))
Known 93eac.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 x6))) = x1 x3 (x1 x4 (x1 x5 (x1 x2 x6)))
Known 5c0b2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x3 (x1 x6 (x1 x4 (x1 x5 x9))))))
Theorem 96acd.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x4 (x1 x6 x5))))))
Theorem 175e5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x4 (x1 x6 x5))))))
Theorem eb789.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x4 (x1 x5 x6))))))
Theorem 1faa1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x4 (x1 x5 x6))))))
Known 75b00.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x2 x7))))
Theorem 41c9b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x5 (x1 x6 x4))))))
Theorem 511e4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x5 (x1 x6 x4))))))
Known 63b79.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x3 (x1 x6 (x1 x5 (x1 x4 x9))))))
Theorem 3da20.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x5 (x1 x4 x6))))))
Theorem dee74.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x5 (x1 x4 x6))))))
Theorem 67a46.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x6 (x1 x5 x4))))))
Theorem 9a962.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x6 (x1 x5 x4))))))
Theorem e006d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x6 (x1 x4 x5))))))
Theorem f8bea.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x7 (x1 x6 (x1 x4 x5))))))
Known d9404.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x3 (x1 x5 (x1 x4 (x1 x6 x9))))))
Theorem 41e6e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x4 (x1 x7 x5))))))
Theorem 1dd83.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x4 (x1 x7 x5))))))
Theorem 2b651.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x4 (x1 x5 x7))))))
Theorem b1f04.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x4 (x1 x5 x7))))))
Theorem 14d16.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x5 (x1 x7 x4))))))
Theorem bcfc7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x5 (x1 x7 x4))))))
Theorem 14831.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x5 (x1 x4 x7))))))
Theorem b5a04.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x5 (x1 x4 x7))))))
Known 1fa22.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x3 (x1 x5 (x1 x6 (x1 x4 x9))))))
Theorem 79cc4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x7 (x1 x5 x4))))))
Theorem af9d6.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x7 (x1 x5 x4))))))
Theorem 7ae01.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x7 (x1 x4 x5))))))
Theorem 7a400.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x6 (x1 x7 (x1 x4 x5))))))
Theorem 91ec3.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x4 (x1 x7 x6))))))
Theorem b7495.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x4 (x1 x7 x6))))))
Theorem 3bfb2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x4 (x1 x6 x7))))))
Theorem 03ed3.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x4 (x1 x6 x7))))))
Known 7662b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x9))))))
Theorem bf40a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x6 (x1 x7 x4))))))
Theorem 1ba0f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x6 (x1 x7 x4))))))
Theorem fc5eb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x6 (x1 x4 x7))))))
Theorem 644cc.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x6 (x1 x4 x7))))))
Known 031de.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x3 (x1 x4 (x1 x6 (x1 x5 x9))))))
Theorem e783d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x7 (x1 x6 x4))))))
Theorem a83df.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x7 (x1 x6 x4))))))
Theorem 03e81.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x7 (x1 x4 x6))))))
Theorem 9142a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x5 (x1 x7 (x1 x4 x6))))))
Theorem 2ecf5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x5 (x1 x7 x6))))))
Theorem 403cc.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x5 (x1 x7 x6))))))
Theorem 64613.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7))))))
Theorem f5483.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7))))))
Theorem 1af2e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x6 (x1 x7 x5))))))
Theorem da6b1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x6 (x1 x7 x5))))))
Theorem e8a6b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x6 (x1 x5 x7))))))
Theorem 76c1f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x6 (x1 x5 x7))))))
Theorem 15b08.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x7 (x1 x6 x5))))))
Theorem c63a2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x7 (x1 x6 x5))))))
Theorem 6474c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x7 (x1 x5 x6))))))
Theorem 76b71.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x3 (x1 x4 (x1 x7 (x1 x5 x6))))))
Known cdf31.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x4 (x1 x6 (x1 x3 (x1 x5 x9))))))
Theorem bd4d7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x3 (x1 x6 x5))))))
Theorem dccf8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x3 (x1 x6 x5))))))
Theorem 74f89.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x3 (x1 x5 x6))))))
Theorem f8063.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x3 (x1 x5 x6))))))
Known c0c54.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x2 x8)))))
Theorem ea154.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x5 (x1 x6 x3))))))
Theorem 7f6d1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x5 (x1 x6 x3))))))
Known 3daae.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x4 (x1 x6 (x1 x5 (x1 x3 x9))))))
Theorem 9779b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x5 (x1 x3 x6))))))
Theorem dd600.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x5 (x1 x3 x6))))))
Theorem 34346.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x6 (x1 x5 x3))))))
Theorem b50be.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x6 (x1 x5 x3))))))
Theorem f3c3f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x6 (x1 x3 x5))))))
Theorem 5d7f1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x7 (x1 x6 (x1 x3 x5))))))
Known 8b281.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x4 (x1 x5 (x1 x3 (x1 x6 x9))))))
Theorem 87e6a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x3 (x1 x7 x5))))))
Theorem 3524f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x3 (x1 x7 x5))))))
Theorem 4f721.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x3 (x1 x5 x7))))))
Theorem 2336b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x3 (x1 x5 x7))))))
Theorem 220cb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x5 (x1 x7 x3))))))
Theorem 59eb7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x5 (x1 x7 x3))))))
Theorem c7434.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x5 (x1 x3 x7))))))
Theorem 437cb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x5 (x1 x3 x7))))))
Theorem 3a7c5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x7 (x1 x5 x3))))))
Theorem 300e9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x7 (x1 x5 x3))))))
Known 229a1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x8 (x1 x2 (x1 x7 (x1 x4 (x1 x5 (x1 x6 (x1 x3 x9))))))
Theorem 6fc0c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x7 (x1 x3 x5))))))
Theorem fadc7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x6 (x1 x7 (x1 x3 x5))))))
Theorem e7b71.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x3 (x1 x7 x6))))))
Theorem 13455.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x3 (x1 x7 x6))))))
Theorem e5ee4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x3 (x1 x6 x7))))))
Theorem 68daf.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x3 (x1 x6 x7))))))
Theorem c4778.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x3))))))
Theorem e15bb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x3))))))
Theorem a4b5b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x6 (x1 x3 x7))))))
Theorem 26de0.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x6 (x1 x3 x7))))))
Theorem e242b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x7 (x1 x6 x3))))))
Theorem ba94b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x7 (x1 x6 x3))))))
Theorem 458cb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 x3 (x1 x2 x4)) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x7 (x1 x3 x6))))))
Theorem f56b9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ (∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4) ⟶ (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x1 x2 x3 = x1 x3 x2) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 x9 (x1 x2 (x1 x8 (x1 x4 (x1 x5 (x1 x7 (x1 x3 x6))))))