Theorem MFL-4. Simple basis with Moufang-2 (part 1).

\{ \begin{matrix}1 · x = x \\ x′ · x = 1 \\ Moufang-2 \end{matrix} \} ⇒ \{ \begin{matrix}x · 1 = x \\ x · x′ = 1 \\ ∀x∀y∃z (x · z = y) \\ ∀x∀y∃z (z · x = y) \end{matrix} \} .

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

1 x = x 3,2 1 · x = x 5,4 x′ · x = 1 7,6 ((x · y) · z) · y = x · (y · (z · y)) 8 A · 1 = A, B · B′ = 1, C · x = D, y · E = F → □

9  x′ · (x · (y · x)) = y · x  [4 → 6 :3, flip]
12,11  (x · y) · x = x · (y · x)  [2 → 6 :3]
13  (x · (y · (z · y))) · z = (x · y) · (z · (y · z))  [6 → 6]
17  x′ · (x · x′) = x′  [4 → 11 :3, flip]
19  (x · (y · x)) · y = x · (y · (x · y))  [11 → 6]
33  x′ · (x · (x · (y · x))) = x · (y · x)  [11 → 9 :12]
37  x′ · (x · (y · (x · (z · x)))) = y · (x · (z · x))  [6 → 9 :7]
42,41  x′ · (x · x) = x  [2 → 9 :3]
44,43  x · x′ = 1  [17 → 9 :5, flip]
47  A · 1 = A, C · x = D, y · E = F → □  [8 :44 :1]
50  x · (y · ((x · y)′ · y)) = y  [43 → 6 :3, flip]
53,52  x · 1 = x  [43 → 11 :3,5, flip]
54  x · (x′ · (y · x′)) = y · x′  [43 → 6 :3, flip]
56  C · x = D, y · E = F → □  [47 :53 :1]
58,57  (x · y) · y = x · (y · y)  [2 → 13 :53,53,3, flip]
68,67  x′ · ((x · x) · x′) = 1  [41 → 11 :44, flip]
73  x · (x′ · x′) = x′  [43 → 57 :3, flip]
95  x · ((x′ · x′) · x) = 1  [73 → 11 :5, flip]
98,97  x′′ = (x · x) · x′  [67 → 9 :53]
99  (x · y′) · (y · (y · y)) = x · (y · y)  [67 → 13 :53,42,12, flip]
112,111 (x · x) · (x′ · x′) = 1  [97 → 4 :58]
113  (x′ · x′) · x = x′  [95 → 9 :53, flip]
149  x · ((y · ((x · y)′ · y)) · x) = y · x  [50 → 11, flip]
168,167 (x · x) · x′ = x  [113 → 54 :98,68,53,98,98,7,58,112,53, flip]
176,175 x′′ = x  [97 :168]
183 x · ((x · x)′ · x) = 1 [50 → 33 :5, flip]
192,191 (x · x)′ · x = x′  [183 → 9 :53, flip]
206,205 x′ · (x · y) = y  [191 → 37 :44,53,192,44,53]
208,207 x · (x′ · y) = y  [167 → 37 :176,5,53,168,5,53]
220,219 x · ((y · x)′ · x) = y′ · x  [50 → 205, flip]
235 x · ((x′ · y) · x) = y · x [149 :220]
316,315 (x · y) · x′ = x · (y · x′)  [235 → 207 :176, flip]

317  (x · y) · (y′ · x) = x · x  [235 → 19 :208,58,208]^{321,320 (x′ · y) · x = x′ · (y · x)  [235 → 205, flip]}^{354,353 (x · x) · y = x · (x · y)  [317 → 6 :321,208]}^{887  (x · (y · y)) · y′ = x · y  [99 → 6 :316,354,44,53,206]}^{909  (x · y′) · y = x  [6 → 887 :354,44,53,5,53, flip]}^{995  □  [56,207,909]}

2