XX = X1^2
XXXX = XX^2
YY = Y1^2
ZZ = Z1^2
ZZZZ = ZZ^2
M = XX+ZZ
t0 = X1+Z1
t1 = t0^2
XZ = t1-M
XZXZ = XZ^2
t2 = Y1+XZ
t3 = t2^2
t4 = t3-YY
X3 = t4-XZXZ
t5 = a*XZXZ
t6 = 2*t5
t7 = 4*YY
t8 = ZZZZ+XXXX
t9 = t7+t6
t10 = XZXZ^2
t11 = t8*t9
Y3 = t11+t10
t12 = ZZZZ-XXXX
Z3 = 2*t12