Theorem QGT-1. Test case for generalized division.

A2 =(gL)⇒ {((xx)y)(xx) = (ey)e}.

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

2 ((A · A) · B) · (A · A) ≠ (e · B) · e 3 (x · e) · e = x 5 e · (e · x) = x 8,7 e · e = e 9 e · (x · e) = (e · x) · e

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

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

14  ((A · A) · B) · (A · A) ≠ e · (B · e)  [2 :11]
15  (e · x) · (e · y) = e · (x · y)  [7 → 10 :(gL)]
25,24  (e · x) · y = e · (x · (e · y))  [5 → 15]
31  ((x · x) · y) · (x · x) = e · (y · e)  [3 → 12 :(gL) :25,8]
33  □  [31,14]