Theorem ABGT-8. A (gL)-basis for Abelian groups with double inversion (2).

\{ \begin{matrix}ee = e \\ (xe)e = x \\ x(xy) = y \end{matrix} \} \underleftarrow{=(gL)⇒} \{(x(((xy)z)(ye)))(ee) = z\}.

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

1 x = x 3,2 e · e = e 5,4 (x · e) · e = x 7,6 x · (y · x) = y 8 (A · (((A · B) · C) · (B · e))) · (e · e) ≠ C

9  (A · (((A · B) · C) · (B · e))) · e ≠ C  [copy,8 :3]
11,10  (x · y) · x = y  [6 → 6]
12  e · x = x · e  [4 → 6]
14,13  x · (x · e) = e  [4 → 10]
17,16  e · (e · x) = x  [12 → 12 :5]
30  x · (x · y) = z · (z · y)  [13 → 13 :(gL)]
34,33  x · (x · y) = y  [13 → 30 :14,17, flip]
39  (x · y) · y = x  [10 → 30 :34]
41  x · y = y · x  [6 → 30 :34]
45  (x · y) · z = z · (y · x)  [41 → 41]
121  (x · y) · (z · u) = (u · z) · (y · x)  [41 → 45]
126  e · ((((A · B) · C) · (B · e)) · A) ≠ C  [45 → 9]
218  (x · y) · (z · u) = (x · z) · (y · u)  [(gL) 121]
222,221 ((x · y) · z) · (y · u) = x · (z · u)  [39 → 218, flip]
250  C ≠ C  [126 :222,11,7]
251  □  [250,1]

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

1 x = x 2 e · e = e, (A · e) · e = A, A · (B · A) = B → □ 3 (x · (((x · y) · z) · (y · e))) · (e · e) = z

8,7  (((x · e) · y) · z) · (y · e) = (x · z) · (e · e)  [3 → 3, flip]
10  x · (((y · x) · (e · e)) · e) = (y · (e · e)) · (e · e)  [3 → 7 :8]
14,13  ((x · e) · ((x · y) · (e · e))) · (e · e) = y  [7 → 3]
15  (e · e) · ((x · (e · e)) · e) = x · (e · e)  [13 → 10 :14]
18,17  (e · e) · (x · e) = x  [13 → 15 :14]
23  ((e · e) · e) · (e · e) = e  [17 → 13]
29,28  (e · (x · (e · e))) · (e · e) = x · e  [17 → 3]
35  ((e · e) · e) · e = e  [23 → 28 :18, flip]
40,39  (e · e) · e = e  [17 → 28 :18, flip]
41  (((x · e) · e) · y) · e = (x · y) · e  [7 → 28 :29, flip]

46,45  e · e = e  [35 :40]^{54,53  e · (x · e) = x  [17 :46]}^{58  x · (((y · x) · e) · e) = (y · e) · e  [10 :46,46,46]}^{65  (A · e) · e = A, A · (B · A) = B → □  [2 :46 :1]}^{68  ((x · e) · e) · y = x · y  [41 → 53 :54, flip]}^{87,86  (x · e) · e = x  [68 → 53 :54, flip]}^{90  A · (B · A) = B → □  [65 :87 :1]}^{91  x · (y · x) = y  [58 :87,87]}^{93  □  [91,90]}

2