t0 = X2^2 t1 = Z2^2 t2 = a*t1 t3 = t0-t2 t4 = t3^2 t5 = Z2^3 t6 = X2*t5 t7 = b*t6 t8 = 8*t7 X4 = t4-t8 t9 = X2^3 t10 = Z2^2 t11 = Z2^3 t12 = b*t11 t13 = X2*t10 t14 = a*t13 t15 = t9+t14 t16 = t15+t12 t17 = Z2*t16 Z4 = 4*t17 t18 = X3*Z2 t19 = X2*Z3 t20 = Z2*Z3 t21 = a*t20 t22 = X2*X3 t23 = t22-t21 t24 = t19+t18 t25 = t23^2 t26 = Z3*t24 t27 = Z2*t26 t28 = b*t27 t29 = 4*t28 X5 = t25-t29 t30 = X3*Z2 t31 = X2*Z3 t32 = t31-t30 t33 = t32^2 Z5 = X1*t33