Theorem DUAL-GT-4. An independent self-dual 4-basis for GT.

\{ \begin{matrix}x · (x′ · y) = y & (1) \\ (y · x′) · x = y & (2) \\ x · x′ = y′ · y & (3) \\ ((x · (y · z)) · y) · u = x · (y · ((z · y) · u)) & (4) \end{matrix} \} .

The Otter proof below derives a well-known basis for GT. To show independence, we note that the first three equations are not a basis because 3 variables are required, and MACE finds 3-element nongroup models of {(1),(2),(4)}, of {(1),(3),(4)}, and of {(2),(3),(4)}.

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

1 x = x 2 B · B′ = A · A′, A · (B · B′) = A, (A · B) · C = A · (B · C) → □ 3 x · (x′ · y) = y 5 (x · y′) · y = x 7 ((x · (y · z)) · y) · u = x · (y · ((z · y) · u)) 9 x · x′ = y′ · y

17,16  (x′ · x) · y = y  [9 → 5]
18  x · (y′ · y) = x′′  [9 → 3]
19  x′′ = x · (y′ · y)  [flip 18]
22,21  x′′ = x  [5 → 16]
27,26  x · (y′ · y) = x  [19 :22, flip]
28  (x · y) · y′ = x  [21 → 5]
35,34  (x · y) · z = x · (y · z)  [16 → 7 :27,27,17]
44,43  x · (y · y′) = x  [28 :35]
45  B · B′ = A · A′ → □  [2 :44,35 :1,1]
51  x · x′ = y · y′  [43 → 3]
52  □  [51,45]