source 2007 Bernstein--Lange parameter a2 assume a2 = 2 a compute A = X1^2 compute U = a2 ZZ1 compute B = A-8 U compute C = A U compute YY = Y1^2 compute YY2 = 2 YY compute Z3 = 2 YY2 compute X3 = B^2 compute V = (Y1+B)^2-YY-X3 compute Y3 = V(X3+64 C+a(YY2-C)) compute ZZ3 = Z3^2