t0 = Y2*ZZ1 A = t0-Y1 t1 = X2*Z1 B = t1-X1 C = B*Z1 Z3 = C^2 D = X2*Z3 E = A^2 t2 = B*C F = X1*t2 t3 = a*Z3 t4 = E-t3 t5 = t4-D X3 = t5-F G = Z3^2 H = A*C t6 = D-X3 t7 = Y2*G t8 = H*t6 Y3 = t8-t7 ZZ3 = G