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