Theorem QGT-3. A basis for Stein quasigroups.

\{ \begin{matrix}quasigroup \\ x(y(yx)) = yx \end{matrix} \} ⇒ \{x(xy) = yx\}.

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

4 x\(x · y) = y 7,6 (x/y) · y = x 8 (x · y)/y = x 10 x · (y · (y · x)) = y · x 12 A · (A · B) ≠ B · A

13  B · A ≠ A · (A · B)  [flip 12]
14  (x/y)\x = y  [6 → 4]
21,20  x · ((y/x) · y) = y  [6 → 10 :7]
33,32  ((x/y) · x) · (y · x) = x  [20 → 10 :21]
34  x/((x/y) · x) = y  [20 → 8]
37,36  x\y = (y/x) · y  [20 → 4]
38  (x/(x/y)) · x = y  [14 :37]
49,48  x/(y · x) = (x/y) · x  [34 → 34]
54  x/y = y/(y/x)  [38 → 8]
55  x/(x/y) = y/x  [flip 54]
68  (x · y)/x = (y/x) · y  [8 → 55 :49]
74  (x/y) · (y/x) = y  [55 → 6]
80  ((x/y) · x) · y = y · x  [8 → 74 :49]
132  x · y = y · (y · x)  [68 → 80 :33]
133  □  [132,13]