Theorem DUAL-GT-5. An independent self-dual 2-basis schema for GT.

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

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

7  (x · (α · y)) · ((z · (α · u))′ · (α · y))′ = (x · z) · (α · u)  [3 → 3]
16,15  ((x · (y · (α · z))′) · y) · (α · z) = x  [3 → 7, flip]
28,27  (((x · (β · (α · y))′) · β) · α)′ · x = y  [15 → 5]
45  (x · y)′ · (x · (y · z)) = z  [27 → 5 :28]
99  ((x · y)′ · x)′ · z = y · z  [45 → 45]
139,138 x · ((y · x)′ · (y · z)) = z  [45 → 99, flip]
140  ((x · y)′ · x)′ = y  [99 → 15 :16, flip]
144  (x′ · (y · z)′)′ = y · (z · x)  [45 → 140]
154  (x · (y · x)′)′ = y  [140 → 140]
170  x · (y · ((x · y)′ · z)) = z  [154 → 45]
276  ((x · (y · z)′) · y) · z = x  [138 → 15 :139]
279  ((x · y) · z) · (y · z)′ = x  [138 → 3 :139]
309  ((x · y) · (z · y)′) · z = x  [140 → 276]
419  x′ · (((x · y) · (z · y)′) · (z · u)) = u  [309 → 45]
435,434 x · (y′ · y) = x  [154 → 144, flip]
480  (x · y′) · y = x  [276 → 434 :435, flip]
489  ((x′ · x) · y′)′ = y  [434 → 154]
493  (x · y) · y′ = x  [434 → 279 :435]
521,520 (x · y) · z = x · (y · z)  [279 → 480, flip]
553,552 x · (y · y′) = x  [493 :521]
556 (x′ · (x · y′))′ = y [489 :521]
580,579 x′ · (x · y) = y  [419 :521,521,521,139]
634  B · B′ = A · A′ → □  [2 :553,521 :1,1]
635  x′′ = x  [556 :580]
648,647 x · (y · x)′ = y′  [154 → 635, flip]
675  x · x′ = y · y′  [552 → 170 :648]
676  □  [675,634]