Proofgold Asset

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))
Known fe827.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x6 (x1 x2 x9))))))
Theorem b7762.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x8 (x1 x4 (x1 x2 x6)))))) (proof)
Theorem 19c32.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x8 (x1 x4 (x1 x2 x6)))))) (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))))
Known 74985.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x4 (x1 x7 (x1 x5 (x1 x2 x9))))))
Theorem 31ccf.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x8 (x1 x6 (x1 x2 x4)))))) (proof)
Theorem b4f33.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x8 (x1 x6 (x1 x2 x4)))))) (proof)
Known fc9b9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x4 (x1 x5 (x1 x2 (x1 x7 x9))))))
Theorem 896d7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x2 (x1 x8 x4)))))) (proof)
Theorem c498d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x2 (x1 x8 x4)))))) (proof)
Known 2b1f0.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x2 (x1 x4 x9))))))
Theorem 14ca2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x2 (x1 x4 x8)))))) (proof)
Theorem 57e5b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x2 (x1 x4 x8)))))) (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))))))
Known c2157.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x6 (x1 x4 (x1 x5 (x1 x3 (x1 x7 x9))))))
Theorem 9262c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x4 (x1 x8 x2)))))) (proof)
Theorem e6ae9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x4 (x1 x8 x2)))))) (proof)
Known f4a20.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x4 (x1 x2 x9))))))
Theorem d8971.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x4 (x1 x2 x8)))))) (proof)
Theorem 78c41.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x4 (x1 x2 x8)))))) (proof)
Known 508bf.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x4 (x1 x5 (x1 x7 (x1 x2 x9))))))
Theorem b3357.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x8 (x1 x2 x4)))))) (proof)
Theorem 7be9b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x6 (x1 x8 (x1 x2 x4)))))) (proof)
Known 029ab.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x5 (x1 x4 (x1 x2 (x1 x7 x9))))))
Theorem 71155.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x2 (x1 x8 x6)))))) (proof)
Theorem b5ec0.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x2 (x1 x8 x6)))))) (proof)
Known acb8a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x2 (x1 x6 x9))))))
Theorem 6cfa9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x2 (x1 x6 x8)))))) (proof)
Theorem 10a45.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x2 (x1 x6 x8)))))) (proof)
Known d2982.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x6 (x1 x4 (x1 x3 (x1 x5 (x1 x7 x9))))))
Theorem 2268d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x6 (x1 x8 x2)))))) (proof)
Theorem 0de60.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x6 (x1 x8 x2)))))) (proof)
Theorem ac29a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x6 (x1 x2 x8)))))) (proof)
Theorem 2529b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x6 (x1 x2 x8)))))) (proof)
Known 3ba89.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x6 (x1 x4 (x1 x3 (x1 x7 (x1 x5 x9))))))
Theorem 55980.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x8 (x1 x6 x2)))))) (proof)
Theorem 36ffb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x8 (x1 x6 x2)))))) (proof)
Known dba18.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x5 (x1 x4 (x1 x7 (x1 x2 x9))))))
Theorem 169ff.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x8 (x1 x2 x6)))))) (proof)
Theorem 3cb86.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x4 (x1 x8 (x1 x2 x6)))))) (proof)
Known 4d026.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x5 (x1 x2 (x1 x4 (x1 x7 x9))))))
Theorem 6af3d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x4 (x1 x8 x6)))))) (proof)
Theorem c356b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x4 (x1 x8 x6)))))) (proof)
Known a3026.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x4 (x1 x6 x9))))))
Theorem cedf4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x4 (x1 x6 x8)))))) (proof)
Theorem b0cc4.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x4 (x1 x6 x8)))))) (proof)
Known 2c790.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x4 (x1 x2 (x1 x5 (x1 x7 x9))))))
Theorem 6e78b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x6 (x1 x8 x4)))))) (proof)
Theorem e7254.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x6 (x1 x8 x4)))))) (proof)
Known 38735.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x6 (x1 x4 x9))))))
Theorem e2db7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x6 (x1 x4 x8)))))) (proof)
Theorem 66b75.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x6 (x1 x4 x8)))))) (proof)
Known 7c391.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x4 (x1 x2 (x1 x7 (x1 x5 x9))))))
Theorem bdc0b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x8 (x1 x6 x4)))))) (proof)
Theorem 6c4f9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x8 (x1 x6 x4)))))) (proof)
Known dd123.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x5 (x1 x2 (x1 x7 (x1 x4 x9))))))
Theorem cf584.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x8 (x1 x4 x6)))))) (proof)
Theorem d4151.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x5 (x1 x2 (x1 x8 (x1 x4 x6)))))) (proof)
Known f10eb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x5 (x1 x7 (x1 x2 (x1 x4 x9))))))
Theorem 7a355.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x2 (x1 x5 x4)))))) (proof)
Theorem 3263c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x2 (x1 x5 x4)))))) (proof)
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)))
Theorem 0a718.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x2 (x1 x4 x5)))))) (proof)
Theorem 6910c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x2 (x1 x4 x5)))))) (proof)
Known 50a74.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x6 (x1 x5 (x1 x7 (x1 x3 (x1 x4 x9))))))
Theorem 9fc7e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x4 (x1 x5 x2)))))) (proof)
Theorem 9c34d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x4 (x1 x5 x2)))))) (proof)
Theorem 02e4e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x4 (x1 x2 x5)))))) (proof)
Theorem d8af9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x4 (x1 x2 x5)))))) (proof)
Theorem 43fc8.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x5 (x1 x2 x4)))))) (proof)
Theorem bec8d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x8 (x1 x5 (x1 x2 x4)))))) (proof)
Theorem b3399.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x2 (x1 x8 x4)))))) (proof)
Theorem d8889.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x2 (x1 x8 x4)))))) (proof)
Known b93bd.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x2 (x1 x4 x9))))))
Theorem 9ee91.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x2 (x1 x4 x8)))))) (proof)
Theorem 47b8d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x2 (x1 x4 x8)))))) (proof)
Known 98346.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x6 (x1 x5 (x1 x4 (x1 x3 (x1 x7 x9))))))
Theorem 6ad7b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x4 (x1 x8 x2)))))) (proof)
Theorem 9c1fd.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x4 (x1 x8 x2)))))) (proof)
Known 6d6c6.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x4 (x1 x2 x9))))))
Theorem d4dcb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x4 (x1 x2 x8)))))) (proof)
Theorem 0c985.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x4 (x1 x2 x8)))))) (proof)
Theorem 3d5c9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x8 (x1 x2 x4)))))) (proof)
Theorem a5736.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x5 (x1 x8 (x1 x2 x4)))))) (proof)
Theorem 496a7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x2 (x1 x8 x5)))))) (proof)
Theorem 56a64.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x2 (x1 x8 x5)))))) (proof)
Known 0e3e7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x2 (x1 x5 x9))))))
Theorem e05fd.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x2 (x1 x5 x8)))))) (proof)
Theorem 2cebc.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x2 (x1 x5 x8)))))) (proof)
Known b2829.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x6 (x1 x5 (x1 x3 (x1 x4 (x1 x7 x9))))))
Theorem b7b2d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x5 (x1 x8 x2)))))) (proof)
Theorem 9e196.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x5 (x1 x8 x2)))))) (proof)
Known 968a9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x5 (x1 x2 x9))))))
Theorem 177d6.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x5 (x1 x2 x8)))))) (proof)
Theorem b5059.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x5 (x1 x2 x8)))))) (proof)
Known 3fb8b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x6 (x1 x5 (x1 x3 (x1 x7 (x1 x4 x9))))))
Theorem 4d28a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x8 (x1 x5 x2)))))) (proof)
Theorem 76622.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x8 (x1 x5 x2)))))) (proof)
Theorem 4e853.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x8 (x1 x2 x5)))))) (proof)
Theorem 74eb6.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x4 (x1 x8 (x1 x2 x5)))))) (proof)
Theorem 8e754.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x4 (x1 x8 x5)))))) (proof)
Theorem 7854a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x4 (x1 x8 x5)))))) (proof)
Known 6a7b6.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x4 (x1 x5 x9))))))
Theorem 72353.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x4 (x1 x5 x8)))))) (proof)
Theorem c6d48.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x4 (x1 x5 x8)))))) (proof)
Theorem d102f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x5 (x1 x8 x4)))))) (proof)
Theorem 00feb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x5 (x1 x8 x4)))))) (proof)
Known 3abe9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x5 (x1 x4 x9))))))
Theorem 070b3.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x5 (x1 x4 x8)))))) (proof)
Theorem aa2e9.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x5 (x1 x4 x8)))))) (proof)
Theorem 7312d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x8 (x1 x5 x4)))))) (proof)
Theorem 8937b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x8 (x1 x5 x4)))))) (proof)
Theorem 1a85d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x8 (x1 x4 x5)))))) (proof)
Theorem c6aa0.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x6 (x1 x2 (x1 x8 (x1 x4 x5)))))) (proof)
Known e5840.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x7 (x1 x5 (x1 x2 (x1 x4 x9))))))
Theorem 2bf5c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x2 (x1 x5 x4)))))) (proof)
Theorem e58b1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x2 (x1 x5 x4)))))) (proof)
Theorem fcd2b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x2 (x1 x4 x5)))))) (proof)
Theorem 22d61.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x2 (x1 x4 x5)))))) (proof)
Known a98e6.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x6 (x1 x7 (x1 x5 (x1 x3 (x1 x4 x9))))))
Theorem 5dee1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x4 (x1 x5 x2)))))) (proof)
Theorem 33903.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x4 (x1 x5 x2)))))) (proof)
Theorem 34d85.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x4 (x1 x2 x5)))))) (proof)
Theorem f607c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x4 (x1 x2 x5)))))) (proof)
Theorem 086d7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x5 (x1 x2 x4)))))) (proof)
Theorem 57034.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x6 (x1 x5 (x1 x2 x4)))))) (proof)
Known 3f695.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x7 (x1 x4 (x1 x2 (x1 x5 x9))))))
Theorem 40b31.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x5 (x1 x2 (x1 x6 x4)))))) (proof)
Theorem f4fdb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x5 (x1 x2 (x1 x6 x4)))))) (proof)
Theorem deecd.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x5 (x1 x2 (x1 x4 x6)))))) (proof)
Theorem ce8bb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x5 (x1 x2 (x1 x4 x6)))))) (proof)
Theorem fd006.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x5 (x1 x4 (x1 x2 x6)))))) (proof)
Theorem 9db5b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x5 (x1 x4 (x1 x2 x6)))))) (proof)
Known b0b0a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x6 (x1 x7 (x1 x4 (x1 x5 (x1 x2 x9))))))
Theorem 18ca6.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x5 (x1 x6 (x1 x2 x4)))))) (proof)
Theorem ae272.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x5 (x1 x6 (x1 x2 x4)))))) (proof)
Theorem 1d59a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x4 (x1 x2 (x1 x6 x5)))))) (proof)
Theorem 9f84a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x4 (x1 x2 (x1 x6 x5)))))) (proof)
Theorem bea3b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x4 (x1 x2 (x1 x5 x6)))))) (proof)
Theorem 28b97.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x4 (x1 x2 (x1 x5 x6)))))) (proof)
Known 0b957.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x6 (x1 x7 (x1 x3 (x1 x4 (x1 x5 x9))))))
Theorem 78272.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x4 (x1 x5 (x1 x6 x2)))))) (proof)
Theorem b5a2a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 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 x3 (x1 x7 (x1 x8 (x1 x4 (x1 x5 (x1 x6 x2)))))) (proof)