Theorem MFL-1. Moufang-1 ⇒ Moufang-2 in loops.

\{ \begin{matrix}loop \\ (x · (y · z)) · x = (x · y) · (z · x) \end{matrix} \} ⇒ \{((x · y) · z) · y = x · (y · (z · y))\}.

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

3,2 1 · x = x 5,4 x · 1 = x 6 x · (x\y) = y 8 x\(x · y) = y 10 (x/y) · y = x 13,12 (x · y)/y = x 14 x · R(x) = 1 18 (x · (y · z)) · x = (x · y) · (z · x) 20 ((A · B) · C) · B ≠ A · (B · (C · B))

30,29  x\1 = R(x)  [14 → 8]
32,31  x\x = 1  [4 → 8]
51  (x · (y/z)) · (z · x) = (x · y) · x  [10 → 18, flip]
53  (x · y) · x = (x · z) · ((z\y) · x)  [6 → 18]
55,54  (x · y) · x = x · (y · x)  [2 → 18 :5]
56  (x · y) · ((y\z) · x) = x · (z · x)  [flip 53 :55]
58  (x · (y/z)) · (z · x) = x · (y · x)  [51 :55]
60  x · ((y · z) · x) = (x · y) · (z · x)  [18 :55]
64  x · (R(x) · x) = x  [14 → 54 :3, flip]
68  x · ((x\y) · x) = y · x  [6 → 54, flip]
70  (x · (y · x))/x = x · y  [54 → 12]
78  R(x) · x = 1  [64 → 8 :32, flip]
85,84  R(R(x)) = x  [78 → 8 :30]
104  x\(y · x) = (x\y) · x  [68 → 8]
106  (x\y) · R(x) = R(x) · (y · R(x))  [78 → 56 :3]
119,118 (x · y)/x = x · (y/x)  [10 → 70]
149,148 R(x) · (y/x) = R(x) · (y · R(x))  [14 → 58 :5]
150  (x · (y/(z/x))) · z = x · (y · x)  [10 → 58]
188  x\((x · y) · (z · x)) = (y · z) · x  [60 → 8]
236  (x\(y/x)) · x = x\y  [10 → 104, flip]
255  x · ((x\y)/x) = y/x  [6 → 118, flip]
286  x\(y/x) = (x\y)/x  [236 → 12, flip]
493,492 x\y = R(x) · y  [106 → 12 :119,13, flip]
551,550 (R(x) · y)/x = R(x) · (y · R(x))  [286 :493,149,493, flip]
559,558 x/y = y · (R(y) · (x · R(y)))  [255 :493,551, flip]
566 R(x) · ((x · y) · (z · x)) = (y · z) · x [188 :493]
585,584 R(x) · (x · y) = y  [8 :493]
587,586 x · (R(x) · y) = y  [6 :493]
630  (x · (y · R(z · R(x)))) · z = x · (y · x)  [150 :559,587,559,587]
634  (x · R(y)) · y = x  [10 :559,587]

658  (x · y) · R(y) = x  [84 → 634]^{672  x · R(y · x) = R(y)  [584 → 658]}^{687,686 R(x · y) = R(y) · R(x)  [658 → 672, flip]}^{692  (x · (y · (x · R(z)))) · z = x · (y · x)  [630 :687,85]}^{946  (x · (y · x)) · z = x · (y · (x · z))  [692 → 634 :85]}^{954  ((x · y) · z) · y = x · (y · (z · y))  [946 → 566 :585, flip]}^{956  □  [954,20]}

2