T1 = Z1^2
T2 = X1 - T1
T1 = X1 + T1
T2 = T2 * T1
T2 = 3 * T2
Y3 = 2 * Y1
Z3 = Y3 * Z1
Y3 = Y3^2
T3 = Y3 * X1
Y3 = Y3^2
Y3 = Y3 * half
X3 = T2^2
T1 = 2 * T3
X3 = X3 - T1
T1 = T3 - X3
T1 = T1 * T2
Y3 = T1 - Y3