R0 = X1^2
X3 = R0*X1
R0 = Y1^2
Y3 = R0*Y1
R0 = Z1^2
Z3 = R0*Z1
R0 = X3-Y3
R0 = R0^2
R1 = X3-Z3
R1 = R1^2
R2 = Y3-Z3
R2 = R2^2
Z3 = Z3+X3
Z3 = Z3+Y3
Z3 = b*Z3
R3 = R0+R2
R0 = R0+R1
R4 = R1+R3
Z3 = Z3*R4
R4 = R1-R3
R4 = R4*X3
R3 = R2-R0
R3 = Y3*R3
X3 = X3*R2
X3 = 2*X3
X3 = X3-R3
Y3 = Y3*R1
Y3 = 2*Y3
Y3 = Y3-R4