Theorem MED-7. Cancellative medial algebras satisfy the quotient condition. Let a, b, c, d, a_{0}, b_{0}, c_{0}, d_{0} be constants.

\{ \begin{matrix}cancellation \\ (xy)(zu) = (xz)(yu) \\ aa_{0} = bb_{0} \\ ca_{0} = db_{0} \\ ac_{0} = bd_{0} \end{matrix} \} ⇒ \{cc_{0} = dd_{0}\}.

Proof (found by Otter 3.0.4 on gyro at 9.76 seconds).

1 d · d_{0} = c · c_{0} → □ 3 x · y = z, x · u = z → y = u 4 x · y = z, u · y = z → x = u 5 (x · y) · (z · u) = (x · z) · (y · u) 6 b · b_{0} = a · a_{0} 8 d · b_{0} = c · a_{0} 10 b · d_{0} = a · c_{0}

12  ((x · y) · (z · u)) · (v · w) = ((x · z) · v) · ((y · u) · w)  [5 → 5]
14  ((x · y) · z) · ((u · v) · w) = ((x · u) · (y · v)) · (z · w)  [flip 12]
17  (b · x) · (b_{0} · y) = (a · a_{0}) · (x · y)  [6 → 5, flip]
21  (d · x) · (b_{0} · y) = (c · a_{0}) · (x · y)  [8 → 5, flip]
49  (a · c_{0}) · (b_{0} · x) = (a · a_{0}) · (d_{0} · x)  [10 → 17]
88  (x · y) · ((a · a_{0}) · (d_{0} · z)) = (x · (a · c_{0})) · (y · (b_{0} · z))  [49 → 5]

107 ((x · y) · (z · u)) · ((v · w) · v_{6}) = ((x · v) · (z · w)) · ((y · u) · v_{6})

[5 → 14]
370  (x · (a · c_{0})) · (y · (b_{0} · z)) = (x · (a · a_{0})) · (y · (d_{0} · z))  [5 → 88, flip]
488  (x · c_{0}) · (b_{0} · y) = (x · a_{0}) · (d_{0} · y)  [3,370,107]
506  d · d_{0} = c · c_{0}  [4,21,488]
508  □  [506,1]