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