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