Theorem ABGT-3. Existence of inverses under (gL). The type is ⟨2, 2, 0⟩ with operations +, ·, and e.

\{ \begin{matrix}x + e = x \\ e + x = x \\ x · (y · x) = y \\ x · y = y · x \end{matrix} \} =(gL)⇒ \{∀y∃x(x + y = e)\}.

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

2 x + e = x 3 e + x = x 4 x · (y · x) = y 5 x · y = y · x 6 x + A = e → $Answer(x) 7 x + e = x

12  e + (x + A) = e → $Answer(x)  [3 → 6]
14  (e + x) · (y · x) = y  [3 → 4]
20  x · (e + (y · x)) = y  [3 → 4]
28  (x · y) · y = x  [4 → 5, flip]
31,30  e + (x · y) = y · x  [3 → 5]
33,32  x · (x · y) = y  [20 :31]
47  (x + y) · (z · y) = (x + u) · (z · u)  [14 → 14 :(gL)]
56  x · (y · e) = (x + z) · (y · z)  [2 → 47]
75  (x + y) · ((x + z) · y) = z  [47 → 32]
242,241 (x + y) · (z · y) = x · (e · z)  [5 → 56, flip]
243  x · (e · (x + y)) = y  [75 → 56 :7,242, flip]
294  e · (x + y) = x · y  [243 → 32, flip]
322,321 x + y = e · (x · y)  [294 → 32, flip]
355  e · (x · A) = e → $Answer(x)  [12 :322,322,33]
356  e · x = e → $Answer(x · A)  [28 → 355]
358  $Answer((e · e) · A)  [356,32]