XX = X1^2
ZZ = Z1^2
t0 = X1+Z1
t1 = t0^2
t2 = t1-XX
t3 = t2-ZZ
A = 2*t3
aZZ = a*ZZ
t4 = XX-aZZ
t5 = t4^2
t6 = A*ZZ
t7 = b2*t6
X3 = t5-t7
t8 = XX+aZZ
t9 = ZZ^2
t10 = b4*t9
t11 = A*t8
Z3 = t11+t10