XX = X1^2 YY = Y1^2 ZZ = Z1^2 YYYY = YY^2 t0 = ZZ^2 t1 = a*t0 t2 = 3*XX M = t2+t1 MM = M^2 t3 = X1+YY t4 = t3^2 t5 = t4-XX t6 = t5-YYYY t7 = 6*t6 E = t7-MM EE = E^2 T = 16*YYYY t8 = M+E t9 = t8^2 t10 = t9-MM t11 = t10-EE U = t11-T t12 = YY*U t13 = 4*t12 t14 = X1*EE t15 = t14-t13 X3 = 4*t15 t16 = T-U t17 = E*EE t18 = U*t16 t19 = t18-t17 t20 = Y1*t19 Y3 = 8*t20 t21 = Z1+E t22 = t21^2 t23 = t22-ZZ Z3 = t23-EE