t0 = X1^2
t1 = Z1^2
t2 = t0-t1
X3 = t2^2
t3 = X1^2
t4 = Z1^2
t5 = X1*Z1
t6 = a*t5
t7 = t3+t6
t8 = t7+t4
t9 = Z1*t8
t10 = X1*t9
Z3 = 4*t10