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