t0 = X1+Z1
t1 = t0^2
t2 = t1-XX1
R1 = t2-ZZ1
R2 = 2*X2
t3 = XX1*XX2
A = 2*t3
B = 2*ZZ1
C = R1*R2
D = Y1*Y2
t4 = R1+Y1
t5 = R2+Y2
t6 = t4*t5
t7 = t6-C
X3 = t7-D
Z3 = B-A
XX3 = X3^2
ZZ3 = Z3^2
t8 = A+B
F = t8+C
t9 = XX1+ZZ1
t10 = XX2+1
t11 = t9*t10
t12 = t11+D
t13 = k*C
t14 = 2*t12
G = t14+t13
H = XX3+ZZ3
t15 = F*G
Y3 = t15-H