Theorem QGT-2. A (gL)-basis for generalized division in Abelian groups.

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

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

1 x = x 2 (A · ((A · B) · A)) · A = B, A · ((A · (B · A)) · A) = B → □ 4,3 (x · e) · e = x 6,5 e · (e · x) = x 8,7 e · e = e 9 e · (x · e) = (e · x) · e

10 (e · x) · e = e · (x · e) [flip 9]

12 ((x · x) · e) · (x · x) = e

14  (e · x) · (e · y) = e · (x · y)  [7 → 10 :(gL)]
16  (x · y) · e = (x · e) · (y · e)  [7 → 10 :(gL)]
24,23  (e · x) · y = e · (x · (e · y))  [5 → 14]
25  (x · y) · (e · z) = (x · e) · (y · z)  [7 → 14 :(gL)]
27  x · (y · e) = e · (y · (x · e))  [10 → 14 :(gL) :6]
30  ((x · x) · y) · (x · x) = e · (y · e)  [3 → 12 :(gL) :24,8]
63  x · y = e · ((y · e) · (x · e))  [3 → 27]
66,65  (x · y) · e = e · (y · x)  [16 → 27 :4]
74  (x · e) · (y · e) = e · (y · x)  [3 → 27]
108,107 ((x · y) · z) · (e · u) = e · (z · (e · ((y · x) · u)))  [65 → 25 :(gL) :24]
111  x · ((y · z) · u) = z · ((y · x) · u)  [25 → 25 :108,24,6,6,66,6]
160  (x · x) · (y · (x · x)) = e · (y · e)  [30 → 30 :(gL) :66,6]
175  (x · y) · (z · e) = e · (y · (e · (z · x)))  [7 → 74 :(gL) :24]
294,293 (x · x) · ((x · x) · y) = y  [65 → 160 :(gL) :6]
411  (x · (x · x)) · (x · e) = e  [160 → 175 :8,8,8]
445  (x · (x · x)) · (x · y) = y  [293 → 411 :(gL) :294]
467  (x · y) · ((y · y) · y) = x  [63 → 445 :66,66,24,6,6]
645  (x · ((y · y) · y)) · y = x  [467 → 467 :294]
1087,1086 x · ((x · (y · x)) · x) = y  [467 → 111, flip]
1102  (A · ((A · B) · A)) · A = B → □  [2 :1087 :1]
1106  (x · ((x · y) · x)) · x = y  [111 → 645]
1108  □  [1106,1102]