t0 = X1^2
t1 = Z1^2
t2 = a*t1
t3 = t0-t2
t4 = t3^2
t5 = Z1^3
t6 = X1*t5
t7 = b*t6
t8 = 8*t7
X3 = t4-t8
t9 = X1^2
t10 = Z1^2
t11 = a*t10
t12 = t9+t11
t13 = Z1^4
t14 = b*t13
t15 = Z1*t12
t16 = X1*t15
t17 = t16+t14
Z3 = 4*t17