XX = X1^2 YY = Y1^2 t0 = c2*Z1 ZZ = t0^2 D = XX+YY DD = D^2 t1 = XX-YY t2 = D*t1 H = 2*t2 t3 = YY*ZZ P = DD-t3 t4 = XX*ZZ Q = DD-t4 T = H+Q U = H-P t5 = U*X1 X3 = P*t5 t6 = T*Y1 Y3 = Q*t6 t7 = U*Z1 Z3 = T*t7