Theorem QUART-2. Conic construction on a quartic curve.

\{ \begin{matrix}m(x, y, m(x, y, z)) = z \\ m(x, y, z) = m(x, z, y) \\ p(z, y, v) = m(x, y, m(x, z, v)) \end{matrix} \} =(gL)⇒

{p(x, y, p(z, v, u)) = p(u, v, p(x, y, z))}.

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

2 m(x, y, m(x, y, z)) = z 3 m(x, y, z) = m(x, z, y) 4 p(z, y, v) = m(x, y, m(x, z, v)) 5 p(A, B, p(C, D, E)) ≠ p(E, D, p(A, B, C))

6  m(x, y, m(x, z, y)) = z  [3 → 2]
7  p(x, y, y) = x  [6 → 4]
8  p(x, x, y) = y  [2 → 4]
14  p(x, x, y) = p(y, z, z)  [7 → 8]
78  p(x, y, z) = p(z, y, x)  [(gL) 14]
88  p(x, y, p(z, u, u)) = p(z, y, x)  [7 → 78]
90  p(x, x, p(y, z, u)) = p(u, z, y)  [8 → 78]
272  p(x, y, p(z, u, y)) = p(x, u, z)  [(gL) 90]
286  p(x, y, p(z, u, y)) = p(z, u, p(x, v, v))  [88 → 272]
538  p(x, y, p(z, u, v)) = p(z, u, p(x, y, v))  [(gL) 286]
541  p(x, y, p(z, u, v)) = p(v, u, p(x, y, z))  [78 → 538]
542  □  [541,5]