A2 = X2^2
B2 = X2*Z2
C2 = Z2^2
A1 = X1^2
B1 = X1*Z1
C1 = Z1^2
A1A2 = A1*A2
B1B2 = B1*B2
C1C2 = C1*C2
Y1Y2 = Y1*Y2
E = C1C2+A1A2
t0 = A1+C1
t1 = A2+C2
t2 = t0*t1
F = t2-E
G = 2*B1B2
t3 = B1+Y1
t4 = B2+Y2
t5 = t3*t4
t6 = t5-B1B2
X3 = t6-Y1Y2
t7 = a*G
t8 = Y1Y2+t7
t9 = G*F
t10 = E*t8
Y3 = t10+t9
Z3 = C1C2-A1A2