t0 = X3-Z3
t1 = X2+Z2
t2 = X3+Z3
t3 = X2-Z2
t4 = t2*t3
t5 = t0*t1
t6 = t5+t4
t7 = t6^2
X5 = Z1*t7
t8 = X3-Z3
t9 = X2+Z2
t10 = X3+Z3
t11 = X2-Z2
t12 = t10*t11
t13 = t8*t9
t14 = t13-t12
t15 = t14^2
Z5 = X1*t15
t16 = X2+Z2
t17 = X2-Z2
t18 = t16^2
t19 = t17^2
X4 = t18*t19
t20 = X2*Z2
t21 = 4*t20
t22 = X2-Z2
t23 = t22^2
t24 = a24*t21
t25 = X2*Z2
t26 = 4*t25
t27 = t23+t24
Z4 = t26*t27