A = X1^2
U = a2*ZZ1
t0 = 8*U
B = A-t0
C = A*U
YY = Y1^2
YY2 = 2*YY
Z3 = 2*YY2
X3 = B^2
t1 = Y1+B
t2 = t1^2
t3 = t2-YY
V = t3-X3
t4 = YY2-C
t5 = a*t4
t6 = 64*C
t7 = X3+t6
t8 = t7+t5
Y3 = V*t8
ZZ3 = Z3^2