t0 = X1+Z1 t1 = t0^2 t2 = t1-XX1 R1 = t2-ZZ1 YY1 = Y1^2 X3 = Y1*R1 t3 = ZZ1-XX1 t4 = ZZ1+XX1 Z3 = t3*t4 XX3 = X3^2 ZZ3 = Z3^2 t5 = YY1^2 t6 = a*XX3 t7 = 2*t5 t8 = t7-t6 Y3 = t8-ZZ3