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