t0 = X2*Z2 t1 = Y1*t0 t2 = Z1*Y2 t3 = X1*t2 X3 = t3+t1 t4 = X1*X2 t5 = Z1*Z2 t6 = t5^2 t7 = t4^2 t8 = X1^2 t9 = Z2^2 t10 = Z1^2 t11 = X2^2 t12 = t10*t11 t13 = t8*t9 t14 = Z1*Z2 t15 = X2*t14 t16 = X1*t15 t17 = a*t16 t18 = 2*t17 t19 = Y1*Y2 t20 = t6+t7 t21 = t19+t18 t22 = t13+t12 t23 = Z2*t22 t24 = Z1*t23 t25 = X2*t24 t26 = X1*t25 t27 = 2*t26 t28 = t20*t21 Y3 = t28+t27 t29 = X1*X2 t30 = Z1*Z2 t31 = t30^2 t32 = t29^2 Z3 = t31-t32