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

\{ \begin{matrix}x · (x′ · y) = y \\ (x · y′) · y = x \\ x′ · x = y · y′ \\ ((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 3.38 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′ · x = y · y′ 8 ((x · (α · y)) · β) · z = x · (α · ((y · β) · z))

15  x · x′ = y · y′  [7 → 7]
16  (x · x′) · y = y′′  [7 → 5]
18,17  x · (y · y′) = x  [7 → 3]
19  x′′ = (y · y′) · x  [flip 16]
20  (A · B) · C = A · (B · C) → □  [2 :18 :15,1]
25,24  x′′ = x  [3 → 17]
28,27  (x · x′) · y = y  [19 :25, flip]
31  (x · y) · y′ = x  [24 → 5]
33  x′ · (x · y) = y  [24 → 3]
37  ((x · y) · β) · z = x · (α · (((α′ · y) · β) · z))  [3 → 8]
38  (x · β) · y = x · (α · ((α′ · β) · y))  [17 → 8]
48  x · (α · ((α′ · β) · y)) = (x · β) · y  [flip 38]
52,51  (x′ · x) · y = y  [24 → 27]
61  (x · y)′ · x = y′  [31 → 33]
76,75  (x · y)′ = y′ · x′  [33 → 61, flip]
94  (x′ · y′) · ((y · x) · z) = z  [75 → 33]
160,159 α · (((α′ · x) · β) · y) = (x · β) · y  [51 → 37 :52, flip]
167,166 x · ((x′ · β) · y) = β · y  [15 → 37 :28,160, flip]
173,172 x · (((x′ · y) · β) · z) = (y · β) · z  [3 → 37 :160, flip]
181 x · ((y · β) · ((β′ · (y′ · x′)) · z)) = z [3 → 37 :76,76,173, flip]
195,194 (x · β) · y = x · (β · y)  [48 :167, flip]
215  x · (y · (β · ((β′ · (y′ · x′)) · z))) = z  [181 :195]
233  x · (β · ((β′ · x′) · y)) = y  [3 → 194 :76, flip]
380  (x′ · y) · ((y′ · x) · z) = z  [24 → 94]
420,419 β · ((β′ · x) · y) = x · y  [233 → 3 :25, flip]
423  x · (y · ((y′ · x′) · z)) = z  [215 :420]
563  (x · y) · z = x · (y · z)  [380 → 423 :25, flip]
565  □  [563,20]