Z1Z1 = Z1^2 U2 = X2*Z1Z1 t0 = Z1*Z1Z1 S2 = Y2*t0 H = U2-X1 HH = H^2 I = 4*HH J = H*I t1 = S2-Y1 r = 2*t1 V = X1*I t2 = r^2 t3 = 2*V t4 = t2-J X3 = t4-t3 t5 = V-X3 t6 = Y1*J t7 = 2*t6 t8 = r*t5 Y3 = t8-t7 t9 = Z1+H t10 = t9^2 t11 = t10-Z1Z1 Z3 = t11-HH