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^3 t10 = Z1^2 t11 = Z1^3 t12 = b*t11 t13 = X1*t10 t14 = a*t13 t15 = t9+t14 t16 = t15+t12 t17 = Z1*t16 Z3 = 4*t17