Theorem STN-6. A 1-basis for SQUAGS (2).

\{(((xx)y)x)(zy) = z\} ⇔ \{ \begin{matrix}xx = x \\ (xy)x = y \end{matrix} \} .

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

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

5  ((((x · x) · x) · y) · (((x · x) · x) · x)) · (z · y) = z  [2 → 2]
7  (((x · x) · (y · z)) · x) · y = ((u · u) · z) · u  [2 → 2]
11  (((x · x) · y) · x) · (((z · z) · u) · z) = ((v · v) · (y · u)) · v  [2 → 7]
12  ((x · x) · y) · x = ((z · z) · y) · z  [7 → 7]
15  ((x · x) · (y · z)) · x = (((u · u) · y) · u) · (((v · v) · z) · v)  [flip 11]
23,22  (((x · x) · y) · x) · (((z · z) · u) · z) = (y · y) · u  [12 → 2]
28  ((x · x) · (y · z)) · x = (y · y) · z  [15 :23]
36  (((x · y) · (x · y)) · (x · y)) · ((x · y) · (x · y)) = (x · x) · y  [28 → 28]

44 (((x · x) · ((y · y) · z)) · x) · ((u · u) · (y · z)) = ((v · v) · u) · v

[28 → 7]
46,45  (((x · x) · y) · x) · ((z · z) · u) = (y · y) · (z · u)  [28 → 2]
52  (((x · x) · y) · ((x · x) · y)) · (z · (x · y)) = ((u · u) · z) · u  [44 :46]
62,61  ((x · x) · x) · (y · x) = y  [12 → 5 :3]
79,78  (x · x) · y = x · y  [36 :62, flip]
105,104 x · (y · x) = y  [61 :79,79]
107,106 (x · y) · x = y  [52 :79,79,79,105,79, flip]
112  A · A = A → □  [4 :107 :1]
113  x · x = x  [106 → 78, flip]
115  □  [113,112]

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

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

7  B · (C · B) ≠ C  [copy,6 :3,5]
8  x · (y · x) = y  [4 → 4]
10  □  [8,7]