t0 = Y2*ZZ1
A = t0-Y1
AA = A^2
t1 = X2*Z1
B = t1-X1
C = B*Z1
CC = C^2
t2 = X2*CC
D = 2*t2
t3 = B*C
F = X1*t3
Z3 = 2*CC
ZZ3 = Z3^2
t4 = AA-F
t5 = a*Z3
t6 = 2*t4
t7 = t6-t5
X3 = t7-D
t8 = A+C
t9 = t8^2
t10 = t9-AA
t11 = t10-CC
t12 = D-X3
t13 = Y2*ZZ3
t14 = t11*t12
Y3 = t14-t13