E1 = R1+Y1
E2 = R2+Y2
XX1XX2 = XX1*XX2
R1R2 = R1*R2
Y1Y2 = Y1*Y2
F = ZZ1+XX1XX2
G = 2*R1R2
t0 = E1*E2
t1 = t0-R1R2
X3 = t1-Y1Y2
t2 = XX1+ZZ1
t3 = XX2+ZZ2
t4 = t2*t3
t5 = a*G
t6 = 4*Y1Y2
t7 = t6+t5
t8 = t4-F
t9 = t8*G
t10 = F*t7
Y3 = t10+t9
t11 = ZZ1-XX1XX2
Z3 = 2*t11
XX3 = X3^2
ZZ3 = Z3^2
t12 = X3+Z3
t13 = t12^2
t14 = t13-XX3
R3 = t14-ZZ3