Theorem DUAL-GT-6. An independent self-dual 3-basis schema for GT.

\{ \begin{matrix}x · (x′ · y) = y \\ (x · y′) · y = x \\ ((x · α) · y) · (β · z) = (x · α) · (y · (β · z)) \end{matrix} \}⇒\{ \begin{matrix}x · x′ = y · y′ \\ x · (y · y′) = x \\ (x · y) · z = x · (y · z) \end{matrix} \} .

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

1 x = x 2 B · B′ = A · A′, A · (B · B′) = A, (A · B) · C = A · (B · C) → □ 4,3 x · (x′ · y) = y 6,5 (x · y′) · y = x 7 ((x · α) · y) · (β · z) = (x · α) · (y · (β · z))

9  x′′ · y = x · y  [3 → 3, flip]
13  x′′ = x  [9 → 5 :6, flip]
15  x′ · (x · y) = y  [9 → 3]
17  (x · y) · y′ = x  [13 → 5]
21  (x · y) · (β · z) = x · (y · (β · z))  [5 → 7 :6]
27  x · (y · x)′ = y′  [15 → 17]
31  (x · y)′ = y′ · x′  [17 → 27, flip]
35  (x · (y · z)) · (z′ · y′) = x  [31 → 17]
54,53  (x · y) · z = x · (y · z)  [3 → 21 :4]
58,57  x · (y · y′) = x  [35 :54,54,4]
59  B · B′ = A · A′ → □  [2 :58,54 :1,1]
63  x · x′ = y · y′  [57 → 3]
64  □  [63,59]