H = X2-X1
HH = H^2
HHHH = HH^2
Z3 = 2*H
ZZ3 = 4*HH
t0 = H+HH
t1 = t0^2
t2 = t1-HH
t3 = t2-HHHH
J = 2*t3
t4 = Y2-Y1
r = 2*t4
V = X1*ZZ3
t5 = r^2
t6 = 2*V
t7 = t5-J
X3 = t7-t6
t8 = V-X3
t9 = Y1*J
t10 = 2*t9
t11 = r*t8
Y3 = t11-t10
t12 = a*HHHH
T3 = 16*t12