Proofgold Address

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 b6723.. : ∀ 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 x5 (x1 x7 (x1 x6 (x1 x2 (x1 x3 (x1 x4 x9))))))
Theorem 5b5d9.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x3 (x1 x4 x5)))))) (proof)
Theorem ee80d.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x3 (x1 x4 x5)))))) (proof)
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 3acd4.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x4 (x1 x5 x3)))))) (proof)
Theorem 6a77b.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x4 (x1 x5 x3)))))) (proof)
Known 3c860.. : ∀ 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 x5 (x1 x7 (x1 x6 (x1 x2 (x1 x4 (x1 x3 x9))))))
Theorem 4b8c8.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x4 (x1 x3 x5)))))) (proof)
Theorem 11671.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x4 (x1 x3 x5)))))) (proof)
Theorem 213e0.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x5 (x1 x4 x3)))))) (proof)
Theorem 548f2.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x5 (x1 x4 x3)))))) (proof)
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 a7cf9.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x5 (x1 x3 x4)))))) (proof)
Theorem e1f0b.. : ∀ 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 x6 (x1 x8 (x1 x7 (x1 x2 (x1 x5 (x1 x3 x4)))))) (proof)
Known 46c89.. : ∀ 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 x5 (x1 x6 (x1 x2 (x1 x7 (x1 x3 (x1 x4 x9))))))
Theorem fc915.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x3 (x1 x5 x4)))))) (proof)
Theorem 6d6bb.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x3 (x1 x5 x4)))))) (proof)
Theorem 346d5.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x3 (x1 x4 x5)))))) (proof)
Theorem fac48.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x3 (x1 x4 x5)))))) (proof)
Theorem 2b685.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x4 (x1 x5 x3)))))) (proof)
Theorem b26d9.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x4 (x1 x5 x3)))))) (proof)
Known 63e29.. : ∀ 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 x5 (x1 x6 (x1 x2 (x1 x7 (x1 x4 (x1 x3 x9))))))
Theorem f3238.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x4 (x1 x3 x5)))))) (proof)
Theorem 70036.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x4 (x1 x3 x5)))))) (proof)
Theorem e9d55.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x5 (x1 x4 x3)))))) (proof)
Theorem 8ec4b.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x5 (x1 x4 x3)))))) (proof)
Theorem b5515.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x5 (x1 x3 x4)))))) (proof)
Theorem 54c78.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x8 (x1 x5 (x1 x3 x4)))))) (proof)
Known ace0d.. : ∀ 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 x5 (x1 x6 (x1 x2 (x1 x4 (x1 x3 (x1 x7 x9))))))
Theorem b203e.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x3 (x1 x8 x4)))))) (proof)
Theorem 41321.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x3 (x1 x8 x4)))))) (proof)
Known 6b685.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x3 (x1 x4 x9))))))
Theorem c2620.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x3 (x1 x4 x8)))))) (proof)
Theorem 48997.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x3 (x1 x4 x8)))))) (proof)
Theorem b4643.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x4 (x1 x8 x3)))))) (proof)
Theorem af7ce.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x4 (x1 x8 x3)))))) (proof)
Known b2a74.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x4 (x1 x3 x9))))))
Theorem fcef6.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x4 (x1 x3 x8)))))) (proof)
Theorem 83850.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x4 (x1 x3 x8)))))) (proof)
Known 53f7d.. : ∀ 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 x5 (x1 x6 (x1 x2 (x1 x4 (x1 x7 (x1 x3 x9))))))
Theorem 86f71.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x8 (x1 x4 x3)))))) (proof)
Theorem ada1c.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x8 (x1 x4 x3)))))) (proof)
Theorem 764f3.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x8 (x1 x3 x4)))))) (proof)
Theorem c6d27.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x5 (x1 x8 (x1 x3 x4)))))) (proof)
Theorem 55cb4.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x3 (x1 x8 x5)))))) (proof)
Theorem 0071d.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x3 (x1 x8 x5)))))) (proof)
Known d5e60.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x3 (x1 x5 x9))))))
Theorem 4912e.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x3 (x1 x5 x8)))))) (proof)
Theorem 9bdcc.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x3 (x1 x5 x8)))))) (proof)
Known bf243.. : ∀ 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 x5 (x1 x6 (x1 x2 (x1 x3 (x1 x4 (x1 x7 x9))))))
Theorem 4351d.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x5 (x1 x8 x3)))))) (proof)
Theorem 3c73b.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x5 (x1 x8 x3)))))) (proof)
Known b3efe.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x5 (x1 x3 x9))))))
Theorem 23945.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x5 (x1 x3 x8)))))) (proof)
Theorem 990e9.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x5 (x1 x3 x8)))))) (proof)
Known eced7.. : ∀ 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 x5 (x1 x6 (x1 x2 (x1 x3 (x1 x7 (x1 x4 x9))))))
Theorem 6d1d8.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x8 (x1 x5 x3)))))) (proof)
Theorem 1a02b.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x8 (x1 x5 x3)))))) (proof)
Theorem 81aa0.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x8 (x1 x3 x5)))))) (proof)
Theorem 55803.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x4 (x1 x8 (x1 x3 x5)))))) (proof)
Theorem 5677c.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x4 (x1 x8 x5)))))) (proof)
Theorem cf3a2.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x4 (x1 x8 x5)))))) (proof)
Known 54952.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x4 (x1 x5 x9))))))
Theorem 159c8.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x4 (x1 x5 x8)))))) (proof)
Theorem f3deb.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x4 (x1 x5 x8)))))) (proof)
Theorem 666e1.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x5 (x1 x8 x4)))))) (proof)
Theorem 51016.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x5 (x1 x8 x4)))))) (proof)
Known 3bc94.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x5 (x1 x4 x9))))))
Theorem 2468b.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x5 (x1 x4 x8)))))) (proof)
Theorem 31801.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x5 (x1 x4 x8)))))) (proof)
Theorem cf435.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x8 (x1 x5 x4)))))) (proof)
Theorem 5e10f.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x8 (x1 x5 x4)))))) (proof)
Theorem 86a60.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x8 (x1 x4 x5)))))) (proof)
Theorem fc484.. : ∀ 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 x6 (x1 x7 (x1 x2 (x1 x3 (x1 x8 (x1 x4 x5)))))) (proof)
Known c3547.. : ∀ 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 x5 (x1 x6 (x1 x3 (x1 x7 (x1 x2 (x1 x4 x9))))))
Theorem 99249.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x8 (x1 x2 (x1 x5 x4)))))) (proof)
Theorem 0fb56.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x8 (x1 x2 (x1 x5 x4)))))) (proof)
Theorem 25bb8.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x8 (x1 x2 (x1 x4 x5)))))) (proof)
Theorem 30ac9.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x8 (x1 x2 (x1 x4 x5)))))) (proof)
Known ed4e6.. : ∀ 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 x5 (x1 x7 (x1 x3 (x1 x4 (x1 x6 (x1 x2 x9))))))
Theorem f180b.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x8 (x1 x4 (x1 x2 x5)))))) (proof)
Theorem 3389f.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x8 (x1 x4 (x1 x2 x5)))))) (proof)
Theorem 01b93.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x8 (x1 x5 (x1 x2 x4)))))) (proof)
Theorem 56816.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x8 (x1 x5 (x1 x2 x4)))))) (proof)
Known b61bd.. : ∀ 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 x5 (x1 x6 (x1 x3 (x1 x4 (x1 x2 (x1 x7 x9))))))
Theorem 9ca8f.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x2 (x1 x8 x4)))))) (proof)
Theorem db888.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x2 (x1 x8 x4)))))) (proof)
Known 2bea3.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x2 (x1 x4 x9))))))
Theorem 1f4a1.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x2 (x1 x4 x8)))))) (proof)
Theorem 4d5bb.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x2 (x1 x4 x8)))))) (proof)
Known 07a54.. : ∀ 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 x5 (x1 x7 (x1 x6 (x1 x3 (x1 x4 (x1 x2 x9))))))
Theorem 77bbf.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x4 (x1 x2 x8)))))) (proof)
Theorem f60dc.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x4 (x1 x2 x8)))))) (proof)
Known 3b540.. : ∀ 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 x5 (x1 x6 (x1 x3 (x1 x4 (x1 x7 (x1 x2 x9))))))
Theorem cd0c8.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x8 (x1 x2 x4)))))) (proof)
Theorem 72688.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x5 (x1 x8 (x1 x2 x4)))))) (proof)
Theorem 89f89.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x2 (x1 x8 x5)))))) (proof)
Theorem 4f72c.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x2 (x1 x8 x5)))))) (proof)
Known 5a423.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x2 (x1 x5 x9))))))
Theorem f8376.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x2 (x1 x5 x8)))))) (proof)
Theorem 231b5.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x2 (x1 x5 x8)))))) (proof)
Known 7beaf.. : ∀ 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 x5 (x1 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x2 x9))))))
Theorem ddb93.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x5 (x1 x2 x8)))))) (proof)
Theorem ca3de.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x5 (x1 x2 x8)))))) (proof)
Theorem 98552.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x8 (x1 x2 x5)))))) (proof)
Theorem c2ddf.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x8 (x1 x2 x5)))))) (proof)
Known 91da2.. : ∀ 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 x5 (x1 x6 (x1 x3 (x1 x2 (x1 x4 (x1 x7 x9))))))
Theorem cb233.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x4 (x1 x8 x5)))))) (proof)
Theorem 95058.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x4 (x1 x8 x5)))))) (proof)
Known ac09f.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x4 (x1 x5 x9))))))
Theorem eef79.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x4 (x1 x5 x8)))))) (proof)
Theorem a8a68.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x4 (x1 x5 x8)))))) (proof)
Theorem 526d2.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x5 (x1 x8 x4)))))) (proof)
Theorem 79322.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x5 (x1 x8 x4)))))) (proof)
Known 83f27.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x5 (x1 x4 x9))))))
Theorem b25e6.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x5 (x1 x4 x8)))))) (proof)
Theorem 5edce.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x5 (x1 x4 x8)))))) (proof)
Known f8e93.. : ∀ 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 x5 (x1 x6 (x1 x3 (x1 x2 (x1 x7 (x1 x4 x9))))))
Theorem ac771.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x8 (x1 x5 x4)))))) (proof)
Theorem f88ae.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x8 (x1 x5 x4)))))) (proof)
Theorem 52ece.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x8 (x1 x4 x5)))))) (proof)
Theorem f42a1.. : ∀ 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 x6 (x1 x7 (x1 x3 (x1 x2 (x1 x8 (x1 x4 x5)))))) (proof)
Theorem bc8e6.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x2 (x1 x5 x3)))))) (proof)
Theorem 03ad0.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x2 (x1 x5 x3)))))) (proof)
Known 3ab16.. : ∀ 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 x5 (x1 x6 (x1 x4 (x1 x7 (x1 x2 (x1 x3 x9))))))
Theorem ccb85.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x2 (x1 x3 x5)))))) (proof)
Theorem a13c3.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x2 (x1 x3 x5)))))) (proof)
Known cbdc2.. : ∀ 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 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x2 x9))))))
Theorem b6c6e.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x3 (x1 x5 x2)))))) (proof)
Theorem 1cbee.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x3 (x1 x5 x2)))))) (proof)
Known 876bb.. : ∀ 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 x5 (x1 x6 (x1 x4 (x1 x7 (x1 x3 (x1 x2 x9))))))
Theorem 63071.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x3 (x1 x2 x5)))))) (proof)
Theorem 3e515.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x3 (x1 x2 x5)))))) (proof)
Theorem 982e3.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x5 (x1 x3 x2)))))) (proof)
Theorem f0a5d.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x5 (x1 x3 x2)))))) (proof)
Theorem b8d34.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x5 (x1 x2 x3)))))) (proof)
Theorem e2828.. : ∀ 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 x6 (x1 x7 (x1 x4 (x1 x8 (x1 x5 (x1 x2 x3)))))) (proof)