t0 = Z2*Z3 t1 = X2*X3 t2 = t1-t0 t3 = t2^2 X5 = Z1*t3 t4 = Z2*X3 t5 = X2*Z3 t6 = t5-t4 t7 = t6^2 Z5 = X1*t7 t8 = X2^2 t9 = Z2^2 t10 = t8-t9 X4 = t10^2 t11 = X2^2 t12 = Z2^2 t13 = X2*Z2 t14 = a*t13 t15 = t11+t14 t16 = t15+t12 t17 = Z2*t16 t18 = X2*t17 Z4 = 4*t18