Proofgold Address

Theorem 547c4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x2 (x1 x3 (x1 x4 x5)) x6 = x1 (x2 x3 x6) (x1 (x2 x4 x6) (x2 x5 x6)) (proof)
Known e11b7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x2 (x1 x3 x4))
Theorem 81c99.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) x7 = x1 (x2 x3 x7) (x1 (x2 x4 x7) (x1 (x2 x5 x7) (x2 x6 x7))) (proof)
Known 25618.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 x5)))
Theorem bc000.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) x8 = x1 (x2 x3 x8) (x1 (x2 x4 x8) (x1 (x2 x5 x8) (x1 (x2 x6 x8) (x2 x7 x8)))) (proof)
Known b9f0e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 x6))))
Theorem a4026.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) x9 = x1 (x2 x3 x9) (x1 (x2 x4 x9) (x1 (x2 x5 x9) (x1 (x2 x6 x9) (x1 (x2 x7 x9) (x2 x8 x9))))) (proof)
Known 2a50e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))))
Theorem 6ee59.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) x10 = x1 (x2 x3 x10) (x1 (x2 x4 x10) (x1 (x2 x5 x10) (x1 (x2 x6 x10) (x1 (x2 x7 x10) (x1 (x2 x8 x10) (x2 x9 x10)))))) (proof)
Known 948ae.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))))
Theorem 2fffd.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) x11 = x1 (x2 x3 x11) (x1 (x2 x4 x11) (x1 (x2 x5 x11) (x1 (x2 x6 x11) (x1 (x2 x7 x11) (x1 (x2 x8 x11) (x1 (x2 x9 x11) (x2 x10 x11))))))) (proof)
Known 18faf.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))))
Theorem de9e9.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))) x12 = x1 (x2 x3 x12) (x1 (x2 x4 x12) (x1 (x2 x5 x12) (x1 (x2 x6 x12) (x1 (x2 x7 x12) (x1 (x2 x8 x12) (x1 (x2 x9 x12) (x1 (x2 x10 x12) (x2 x11 x12)))))))) (proof)
Known 880a1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))))
Theorem 6c866.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))))) x13 = x1 (x2 x3 x13) (x1 (x2 x4 x13) (x1 (x2 x5 x13) (x1 (x2 x6 x13) (x1 (x2 x7 x13) (x1 (x2 x8 x13) (x1 (x2 x9 x13) (x1 (x2 x10 x13) (x1 (x2 x11 x13) (x2 x12 x13))))))))) (proof)
Known 737fb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))))
Theorem 1fe00.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))))))) x14 = x1 (x2 x3 x14) (x1 (x2 x4 x14) (x1 (x2 x5 x14) (x1 (x2 x6 x14) (x1 (x2 x7 x14) (x1 (x2 x8 x14) (x1 (x2 x9 x14) (x1 (x2 x10 x14) (x1 (x2 x11 x14) (x1 (x2 x12 x14) (x2 x13 x14)))))))))) (proof)
Known f7821.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))))))
Theorem 2555f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))) x15 = x1 (x2 x3 x15) (x1 (x2 x4 x15) (x1 (x2 x5 x15) (x1 (x2 x6 x15) (x1 (x2 x7 x15) (x1 (x2 x8 x15) (x1 (x2 x9 x15) (x1 (x2 x10 x15) (x1 (x2 x11 x15) (x1 (x2 x12 x15) (x1 (x2 x13 x15) (x2 x14 x15))))))))))) (proof)
Known 2c5ad.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))))))))
Theorem 3841c.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))) x16 = x1 (x2 x3 x16) (x1 (x2 x4 x16) (x1 (x2 x5 x16) (x1 (x2 x6 x16) (x1 (x2 x7 x16) (x1 (x2 x8 x16) (x1 (x2 x9 x16) (x1 (x2 x10 x16) (x1 (x2 x11 x16) (x1 (x2 x12 x16) (x1 (x2 x13 x16) (x1 (x2 x14 x16) (x2 x15 x16)))))))))))) (proof)
Known ea7b1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))))
Theorem 8454f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))))))))) x17 = x1 (x2 x3 x17) (x1 (x2 x4 x17) (x1 (x2 x5 x17) (x1 (x2 x6 x17) (x1 (x2 x7 x17) (x1 (x2 x8 x17) (x1 (x2 x9 x17) (x1 (x2 x10 x17) (x1 (x2 x11 x17) (x1 (x2 x12 x17) (x1 (x2 x13 x17) (x1 (x2 x14 x17) (x1 (x2 x15 x17) (x2 x16 x17))))))))))))) (proof)
Known 6cd80.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))))
Theorem 1d55a.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17)))))))))))))) x18 = x1 (x2 x3 x18) (x1 (x2 x4 x18) (x1 (x2 x5 x18) (x1 (x2 x6 x18) (x1 (x2 x7 x18) (x1 (x2 x8 x18) (x1 (x2 x9 x18) (x1 (x2 x10 x18) (x1 (x2 x11 x18) (x1 (x2 x12 x18) (x1 (x2 x13 x18) (x1 (x2 x14 x18) (x1 (x2 x15 x18) (x1 (x2 x16 x18) (x2 x17 x18)))))))))))))) (proof)
Known 855a7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))))))))))
Theorem d1d81.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x0 x19 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18))))))))))))))) x19 = x1 (x2 x3 x19) (x1 (x2 x4 x19) (x1 (x2 x5 x19) (x1 (x2 x6 x19) (x1 (x2 x7 x19) (x1 (x2 x8 x19) (x1 (x2 x9 x19) (x1 (x2 x10 x19) (x1 (x2 x11 x19) (x1 (x2 x12 x19) (x1 (x2 x13 x19) (x1 (x2 x14 x19) (x1 (x2 x15 x19) (x1 (x2 x16 x19) (x1 (x2 x17 x19) (x2 x18 x19))))))))))))))) (proof)
Theorem cebfe.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x2 x6 (x1 x3 (x1 x4 x5)) = x1 (x2 x6 x3) (x1 (x2 x6 x4) (x2 x6 x5)) (proof)
Theorem bbdc7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x2 x7 (x1 x3 (x1 x4 (x1 x5 x6))) = x1 (x2 x7 x3) (x1 (x2 x7 x4) (x1 (x2 x7 x5) (x2 x7 x6))) (proof)
Theorem 6831b.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 x8 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 (x2 x8 x3) (x1 (x2 x8 x4) (x1 (x2 x8 x5) (x1 (x2 x8 x6) (x2 x8 x7)))) (proof)
Theorem 67024.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 x9 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 (x2 x9 x3) (x1 (x2 x9 x4) (x1 (x2 x9 x5) (x1 (x2 x9 x6) (x1 (x2 x9 x7) (x2 x9 x8))))) (proof)
Theorem fc0c5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 x10 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 (x2 x10 x3) (x1 (x2 x10 x4) (x1 (x2 x10 x5) (x1 (x2 x10 x6) (x1 (x2 x10 x7) (x1 (x2 x10 x8) (x2 x10 x9)))))) (proof)
Theorem 128a5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 x11 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) = x1 (x2 x11 x3) (x1 (x2 x11 x4) (x1 (x2 x11 x5) (x1 (x2 x11 x6) (x1 (x2 x11 x7) (x1 (x2 x11 x8) (x1 (x2 x11 x9) (x2 x11 x10))))))) (proof)
Theorem 3eed7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 x12 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))) = x1 (x2 x12 x3) (x1 (x2 x12 x4) (x1 (x2 x12 x5) (x1 (x2 x12 x6) (x1 (x2 x12 x7) (x1 (x2 x12 x8) (x1 (x2 x12 x9) (x1 (x2 x12 x10) (x2 x12 x11)))))))) (proof)
Theorem 83656.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 x13 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))))) = x1 (x2 x13 x3) (x1 (x2 x13 x4) (x1 (x2 x13 x5) (x1 (x2 x13 x6) (x1 (x2 x13 x7) (x1 (x2 x13 x8) (x1 (x2 x13 x9) (x1 (x2 x13 x10) (x1 (x2 x13 x11) (x2 x13 x12))))))))) (proof)
Theorem e214f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 x14 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))))))) = x1 (x2 x14 x3) (x1 (x2 x14 x4) (x1 (x2 x14 x5) (x1 (x2 x14 x6) (x1 (x2 x14 x7) (x1 (x2 x14 x8) (x1 (x2 x14 x9) (x1 (x2 x14 x10) (x1 (x2 x14 x11) (x1 (x2 x14 x12) (x2 x14 x13)))))))))) (proof)
Theorem 3d6c4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 x15 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))) = x1 (x2 x15 x3) (x1 (x2 x15 x4) (x1 (x2 x15 x5) (x1 (x2 x15 x6) (x1 (x2 x15 x7) (x1 (x2 x15 x8) (x1 (x2 x15 x9) (x1 (x2 x15 x10) (x1 (x2 x15 x11) (x1 (x2 x15 x12) (x1 (x2 x15 x13) (x2 x15 x14))))))))))) (proof)
Theorem 22e9e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 x16 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))) = x1 (x2 x16 x3) (x1 (x2 x16 x4) (x1 (x2 x16 x5) (x1 (x2 x16 x6) (x1 (x2 x16 x7) (x1 (x2 x16 x8) (x1 (x2 x16 x9) (x1 (x2 x16 x10) (x1 (x2 x16 x11) (x1 (x2 x16 x12) (x1 (x2 x16 x13) (x1 (x2 x16 x14) (x2 x16 x15)))))))))))) (proof)
Theorem 068aa.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x2 x17 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))))))))) = x1 (x2 x17 x3) (x1 (x2 x17 x4) (x1 (x2 x17 x5) (x1 (x2 x17 x6) (x1 (x2 x17 x7) (x1 (x2 x17 x8) (x1 (x2 x17 x9) (x1 (x2 x17 x10) (x1 (x2 x17 x11) (x1 (x2 x17 x12) (x1 (x2 x17 x13) (x1 (x2 x17 x14) (x1 (x2 x17 x15) (x2 x17 x16))))))))))))) (proof)
Theorem 20ea2.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x2 x18 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17)))))))))))))) = x1 (x2 x18 x3) (x1 (x2 x18 x4) (x1 (x2 x18 x5) (x1 (x2 x18 x6) (x1 (x2 x18 x7) (x1 (x2 x18 x8) (x1 (x2 x18 x9) (x1 (x2 x18 x10) (x1 (x2 x18 x11) (x1 (x2 x18 x12) (x1 (x2 x18 x13) (x1 (x2 x18 x14) (x1 (x2 x18 x15) (x1 (x2 x18 x16) (x2 x18 x17)))))))))))))) (proof)
Theorem 44d11.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x0 x19 ⟶ x2 x19 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18))))))))))))))) = x1 (x2 x19 x3) (x1 (x2 x19 x4) (x1 (x2 x19 x5) (x1 (x2 x19 x6) (x1 (x2 x19 x7) (x1 (x2 x19 x8) (x1 (x2 x19 x9) (x1 (x2 x19 x10) (x1 (x2 x19 x11) (x1 (x2 x19 x12) (x1 (x2 x19 x13) (x1 (x2 x19 x14) (x1 (x2 x19 x15) (x1 (x2 x19 x16) (x1 (x2 x19 x17) (x2 x19 x18))))))))))))))) (proof)
Theorem c50dc.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x2 (x1 x3 x4) (x1 x5 x6) = x1 (x1 (x2 x3 x5) (x2 x3 x6)) (x1 (x2 x4 x5) (x2 x4 x6)) (proof)
Theorem f7342.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 x7)) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x2 x3 x7))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x2 x4 x7))) (proof)
Theorem 385a8.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 x8))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x2 x3 x8)))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x2 x4 x8)))) (proof)
Theorem 99370.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x2 x3 x9))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x2 x4 x9))))) (proof)
Theorem 7e8a0.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10)))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10)))))) (proof)
Theorem 2987b.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11))))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11))))))) (proof)
Theorem 65828.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12)))))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12)))))))) (proof)
Theorem 7f9d6.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 x7) = x1 (x1 (x2 x3 x6) (x2 x3 x7)) (x1 (x1 (x2 x4 x6) (x2 x4 x7)) (x1 (x2 x5 x6) (x2 x5 x7))) (proof)
Theorem ef027.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 x8)) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x2 x3 x8))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x2 x4 x8))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x2 x5 x8)))) (proof)
Theorem 06c4f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 x9))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x2 x3 x9)))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x2 x4 x9)))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x2 x5 x9))))) (proof)
Theorem ef15c.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10)))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x2 x5 x10)))))) (proof)
Theorem 24435.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11))))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11)))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11)))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11))))))) (proof)
Theorem 6b961.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12)))))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12))))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12))))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12)))))))) (proof)
Theorem 3ba1a.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13))))))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13)))))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13)))))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))))))))) (proof)
Theorem bdad1.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 x8) = x1 (x1 (x2 x3 x7) (x2 x3 x8)) (x1 (x1 (x2 x4 x7) (x2 x4 x8)) (x1 (x1 (x2 x5 x7) (x2 x5 x8)) (x1 (x2 x6 x7) (x2 x6 x8)))) (proof)
Theorem 037b6.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 x9)) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x2 x3 x9))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x2 x4 x9))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x2 x5 x9))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x2 x6 x9))))) (proof)
Theorem 70471.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 x10))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10)))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10)))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x2 x5 x10)))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x2 x6 x10)))))) (proof)
Theorem 34a9f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x2 x6 x11))))))) (proof)
Theorem c5a67.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12)))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12)))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12)))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12)))))))) (proof)
Theorem a4275.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13))))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13))))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13))))))))) (proof)
Theorem acdf7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14)))))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14)))))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14)))))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14)))))))))) (proof)
Theorem 1634a.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 x9) = x1 (x1 (x2 x3 x8) (x2 x3 x9)) (x1 (x1 (x2 x4 x8) (x2 x4 x9)) (x1 (x1 (x2 x5 x8) (x2 x5 x9)) (x1 (x1 (x2 x6 x8) (x2 x6 x9)) (x1 (x2 x7 x8) (x2 x7 x9))))) (proof)
Theorem 9d4e1.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 x10)) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x2 x5 x10))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x2 x6 x10))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x2 x7 x10)))))) (proof)
Theorem 96e70.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 x11))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11)))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11)))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11)))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x2 x6 x11)))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x2 x7 x11))))))) (proof)
Theorem 8b8a9.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12)))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x2 x7 x12)))))))) (proof)
Theorem a33b6.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13))))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13)))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13)))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13)))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13)))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13))))))))) (proof)
Theorem 6c6f7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14)))))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14))))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14))))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14))))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14))))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14)))))))))) (proof)
Theorem a8c31.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15))))))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15)))))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15)))))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15)))))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15)))))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15))))))))))) (proof)
Theorem c240f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 x10) = x1 (x1 (x2 x3 x9) (x2 x3 x10)) (x1 (x1 (x2 x4 x9) (x2 x4 x10)) (x1 (x1 (x2 x5 x9) (x2 x5 x10)) (x1 (x1 (x2 x6 x9) (x2 x6 x10)) (x1 (x1 (x2 x7 x9) (x2 x7 x10)) (x1 (x2 x8 x9) (x2 x8 x10)))))) (proof)
Theorem ab0f3.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 x11)) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x2 x6 x11))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x2 x7 x11))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x2 x8 x11))))))) (proof)
Theorem 1b2e4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 x12))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12)))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12)))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12)))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12)))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x2 x7 x12)))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x2 x8 x12)))))))) (proof)
Theorem afa83.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x2 x8 x13))))))))) (proof)
Theorem 30e88.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14)))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14)))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14)))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14)))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14)))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x2 x8 x14)))))))))) (proof)
Theorem d7b62.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15))))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15))))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15))))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15))))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15))))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x2 x8 x15))))))))))) (proof)
Theorem 7be79.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x2 x3 x16)))))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x2 x4 x16)))))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x2 x5 x16)))))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x2 x6 x16)))))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x2 x7 x16)))))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x2 x8 x16)))))))))))) (proof)
Theorem e6d5e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 x11) = x1 (x1 (x2 x3 x10) (x2 x3 x11)) (x1 (x1 (x2 x4 x10) (x2 x4 x11)) (x1 (x1 (x2 x5 x10) (x2 x5 x11)) (x1 (x1 (x2 x6 x10) (x2 x6 x11)) (x1 (x1 (x2 x7 x10) (x2 x7 x11)) (x1 (x1 (x2 x8 x10) (x2 x8 x11)) (x1 (x2 x9 x10) (x2 x9 x11))))))) (proof)
Theorem 503ac.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 x12)) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x2 x7 x12))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x2 x8 x12))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x2 x9 x12)))))))) (proof)
Theorem f7ed5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 x13))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13)))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13)))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13)))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13)))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13)))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x2 x8 x13)))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x2 x9 x13))))))))) (proof)
Theorem 641ca.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14)))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x2 x8 x14))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x2 x9 x14)))))))))) (proof)
Theorem 7a734.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15))))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15)))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15)))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15)))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15)))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15)))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x2 x8 x15)))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x2 x9 x15))))))))))) (proof)
Theorem 45365.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16)))))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x2 x3 x16))))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x2 x4 x16))))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x2 x5 x16))))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x2 x6 x16))))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x2 x7 x16))))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x2 x8 x16))))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x2 x9 x16)))))))))))) (proof)
Theorem de0dc.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17))))))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x2 x3 x17)))))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x2 x4 x17)))))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x2 x5 x17)))))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x2 x6 x17)))))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x1 (x2 x7 x16) (x2 x7 x17)))))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x1 (x2 x8 x16) (x2 x8 x17)))))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x1 (x2 x9 x16) (x2 x9 x17))))))))))))) (proof)
Theorem 74594.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 x12) = x1 (x1 (x2 x3 x11) (x2 x3 x12)) (x1 (x1 (x2 x4 x11) (x2 x4 x12)) (x1 (x1 (x2 x5 x11) (x2 x5 x12)) (x1 (x1 (x2 x6 x11) (x2 x6 x12)) (x1 (x1 (x2 x7 x11) (x2 x7 x12)) (x1 (x1 (x2 x8 x11) (x2 x8 x12)) (x1 (x1 (x2 x9 x11) (x2 x9 x12)) (x1 (x2 x10 x11) (x2 x10 x12)))))))) (proof)
Theorem 31403.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 x13)) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x2 x8 x13))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x2 x9 x13))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x2 x10 x13))))))))) (proof)
Theorem 24a12.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 x14))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14)))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14)))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14)))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14)))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14)))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x2 x8 x14)))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x2 x9 x14)))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x2 x10 x14)))))))))) (proof)
Theorem ff328.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x2 x8 x15))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x2 x9 x15))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x2 x10 x15))))))))))) (proof)
Theorem 075c5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x2 x3 x16)))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x2 x4 x16)))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x2 x5 x16)))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x2 x6 x16)))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x2 x7 x16)))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x2 x8 x16)))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x2 x9 x16)))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x1 (x2 x10 x15) (x2 x10 x16)))))))))))) (proof)
Theorem 5a91e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17)))))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x2 x3 x17))))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x2 x4 x17))))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x2 x5 x17))))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x2 x6 x17))))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x1 (x2 x7 x16) (x2 x7 x17))))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x1 (x2 x8 x16) (x2 x8 x17))))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x1 (x2 x9 x16) (x2 x9 x17))))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x1 (x2 x10 x15) (x1 (x2 x10 x16) (x2 x10 x17))))))))))))) (proof)
Theorem 43f21.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18))))))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x1 (x2 x3 x17) (x2 x3 x18)))))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x1 (x2 x4 x17) (x2 x4 x18)))))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x1 (x2 x5 x17) (x2 x5 x18)))))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x1 (x2 x6 x17) (x2 x6 x18)))))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x1 (x2 x7 x16) (x1 (x2 x7 x17) (x2 x7 x18)))))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x1 (x2 x8 x16) (x1 (x2 x8 x17) (x2 x8 x18)))))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x1 (x2 x9 x16) (x1 (x2 x9 x17) (x2 x9 x18)))))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x1 (x2 x10 x15) (x1 (x2 x10 x16) (x1 (x2 x10 x17) (x2 x10 x18)))))))))))))) (proof)