XX = X1^2 XXX = X1*XX YY = Y1^2 YYY = Y1*YY ZZ = Z1^2 ZZZ = Z1*ZZ t0 = ZZZ-XXX X3 = Y1*t0 t1 = YYY-ZZZ Y3 = X1*t1 t2 = XXX-YYY Z3 = Z1*t2