Theorem ABGT-6. A (gL)-basis for left and right division in Abelian groups. The type is ⟨2, 0⟩.

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

In view of [?], this gives us all Abelian group axioms satisfied by both left division \ and right division /.

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

3,2 x | x = e 5,4 e | (e | x) = x 7,6 (x | e) | e = x 8 e | (x | e) = (e | x) | e

9 (e | x) | e = e | (x | e) [flip 8]

11 (A | B) | (((A | C) | (D | D)) | B) ≠ C

12  (A | B) | (((A | C) | e) | B) ≠ C  [copy,11 :3]
13  (e | x) | (e | y) = e | (x | y)  [6 → 9 :(gL) :3]
15  (x | y) | e = (x | e) | (y | e)  [4 → 9 :(gL) :3]
23,22  (e | x) | y = e | (x | (e | y))  [4 → 13]
24  (x | y) | (e | z) = (x | e) | (y | z)  [4 → 13 :(gL) :3]
25  x | (y | (e | z)) = e | (y | (x | z))  [13 → 13 :(gL) :5]
26  x | (y | e) = e | (y | (x | e))  [9 → 13 :(gL) :5]
27  ((x | y) | z) | e = ((x | e) | z) | y  [15 → 15 :(gL) :7]
39  (A | B) | (((A | e) | (C | e)) | B) ≠ C  [15 → 12]
53,52  (x | y) | e = e | (y | x)  [15 → 26 :7]
67,66  ((x | e) | y) | z = e | (y | (x | z))  [27 :53, flip]
71  (A | B) | (e | ((C | e) | (A | B))) ≠ C  [39 :67]
80  (x | y) | (e | y) = x  [2 → 24 :53,5]
113  x | e = y | (e | (x | y))  [2 → 25 :23,5]
137,136 (x | (y | z)) | z = (x | e) | y  [80 → 24 :5]
183  x | (e | ((y | e) | x)) = y  [113 → 113 :53,137,3,5, flip]
185  □  [183,71]