Theorem ABGT-5. A (gL)-basis for right division in Abelian groups (2).

\{ \begin{matrix}x/e = x \\ x/x = e \end{matrix} \} =(gL)⇒ \{x/((y/z)/(y/x)) = z\}.

The conclusion is another single axiom for Abelian groups in terms of right division. (Note: the first axioms we tried were {x/e = x, e/(e/x) = x}. Otter failed to find a proof. Then we found a counterexample and added axiom x/x = e to kill the unwanted model x + 3y (mod 8). Otter found a proof, but the proof did not use e/(e/x) = x. Hence the current basis.)

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

2 x/e = x 3 x/x = e 5 A/((B/C)/(B/A)) ≠ C

10  (x/e)/e = x  [2 → 2]
15  x/(x/e) = e  [2 → 3]
17  x/(y/y) = x  [3 → 2]
152  x/(x/y) = z/(z/y)  [15 → 15 :(gL)]
634  x/(x/y) = y  [17 → 152, flip]
858  (x/e)/(x/y) = y  [2 → 634]
884  x/((x/y)/e) = y  [2 → 634]
9245  (x/y)/(x/z) = (z/y)/e  [10 → 858 :(gL)]
11150  x/((y/z)/(y/x)) = z  [9245 → 884]
11151  □  [11150,5]