Theorem ABGT-7. A (gL)-basis for Abelian groups with double inversion (1).

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

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

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

8  (A · ((C · (A · B)) · (e · B))) · e ≠ C  [copy,7 :3]
13  (e · x) · (y · (x · e)) = y  [4 → 5]
19,18  (x · y) · x = y  [5 → 5]
21,20  e · (e · x) = x  [4 → 5]
22  x · (x · e) = e  [4 → 5]
35  x · (x · y) = y  [20 → 22 :(gL) :21]
41  (x · y) · y = x  [18 → 35]
43  x · y = y · x  [5 → 35]
44  (x · y) · (z · (y · u)) = (x · v) · (z · (v · u))  [13 → 13 :(gL) :(gL)]
46  (e · x) · y = (x · e) · y  [18 → 13]
54  (A · (((A · B) · C) · (e · B))) · e ≠ C  [43 → 8]
65,64  (x · y) · (z · (y · x)) = z  [43 → 5]
84  (x · y) · z = (x · u) · (y · (u · z))  [35 → 44]
129,128 ((x · y) · e) · z = (e · (y · x)) · z  [43 → 46, flip]
473 e · ((((A · B) · C) · (e · B)) · A) ≠ C [64 → 54 :129,65]
540,539 ((x · y) · z) · u = x · (z · (y · u))  [41 → 84]
593  C ≠ C  [473 :540,6,19,6]
594  □  [593,1]

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

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

5  (e · (x · (e · e))) · (e · e) = y · ((x · (y · z)) · (e · z))  [3 → 3]
7  x · ((y · (x · z)) · (e · z)) = u · ((y · (u · v)) · (e · v))  [5 → 5]
8  x · (((y · (e · e)) · (x · z)) · (e · z)) = y  [3 → 5, flip]
11,10  (e · x) · (e · e) = e · (x · (e · e))  [5 → 3 :4]
13,12  e · (((x · (e · y)) · (e · y)) · (e · e)) = x  [3 → 10, flip]
14  (x · (e · ((x · e) · (e · e)))) · (e · e) = e  [10 → 3]
16  e · (e · (e · (e · (e · (e · (e · e)))))) = e  [10 → 8 :11,11,11,11,11]
19,18  e · (((x · y) · y) · (e · e)) = x  [12 → 12 :13]

20  e · (((x · (e · e)) · y) · y) = x  [18 → 8 :19]
24  ((x · e) · x) · (e · e) = e  [18 → 14]
27,26  e · (e · e) = e  [24 → 24]
29,28  e · e = e  [16 :27,27,27]
30  ((x · e) · x) · e = e  [24 :29]
34  e · (((x · e) · y) · y) = x  [20 :29]
36  e · (((x · y) · y) · e) = x  [18 :29]
41,40  (e · x) · e = e · (x · e)  [10 :29,29]
44  (x · ((y · (x · z)) · (e · z))) · e = y  [3 :29]
46  e · A = A · e, A · (B · A) = B → □  [2 :29 :1]
47  e · ((e · x) · x) = (y · e) · y  [30 → 34]
49,48  e · ((e · x) · x) = e  [28 → 34]
50  (x · e) · x = e  [flip 47 :49]
53,52  e · (e · x) = x  [50 → 34]
54  ((x · e) · y) · y = e · x  [34 → 52, flip]
62  (e · x) · x = e  [48 → 52 :29, flip]
64  x · (e · x) = e  [52 → 62]
67,66  x · ((y · (x · z)) · (e · z)) = e · y  [64 → 7 :53, flip]
68  x · ((y · e) · x) = e · y  [64 → 7 :53,67]
71,70  e · (x · e) = x  [44 :67,41]
75,74  (x · y) · y = x  [36 :71]
76  x · e = e · x  [54 :75]
77  e · x = x · e  [flip 76]
109,108 x · (y · x) = y  [74 → 68 :71]
112  □  [46 :109 :77,1]