source 2008 Bernstein--Lange--Rezaeian-Farashahi "Binary Edwards Curves", plus specialization to Z1=1, plus simplification
assume Z1 = 1
compute A = X1^2
compute B = Y1^2
compute Z3 = A
compute ZZ3 = A^2
compute X3 = ZZ3 + a6
compute XZ3 = X3 Z3
compute Y3 = B (B + X3 + Z3) + a6 ZZ3 + XZ3