XX = X1^2 YY = Y1^2 YYYY = YY^2 ZZ = Z1^2 t0 = X1+YY t1 = t0^2 t2 = t1-XX t3 = t2-YYYY S = 2*t3 t4 = ZZ^2 t5 = a*t4 t6 = 3*XX M = t6+t5 t7 = M^2 t8 = 2*S T = t7-t8 X3 = T t9 = S-T t10 = 8*YYYY t11 = M*t9 Y3 = t11-t10 t12 = Y1+Z1 t13 = t12^2 t14 = t13-YY Z3 = t14-ZZ