A = Z1^2
E = X2*Z1
G = Y2*A
H = X1-E
I = Y1-G
II = I^2
J = Z1*H
t0 = J*H
K = 2*t0
t1 = X1+E
t2 = t1*K
t3 = 2*II
X3 = t3-t2
JJ = J^2
t4 = J+I
t5 = t4^2
t6 = X1*K
t7 = t5-JJ
t8 = t7-II
t9 = t6-X3
t10 = K^2
t11 = Y1*t10
t12 = t8*t9
Y3 = t12-t11
Z3 = 2*JJ