XX = X2^2
ZZ = Z2^2
t0 = X2+Z2
t1 = t0^2
t2 = t1-XX
t3 = t2-ZZ
E = 2*t3
aZZ = a*ZZ
t4 = XX-aZZ
t5 = t4^2
t6 = E*ZZ
t7 = b2*t6
X4 = t5-t7
t8 = XX+aZZ
t9 = ZZ^2
t10 = b4*t9
t11 = E*t8
Z4 = t11+t10
A = X2*X3
B = Z2*Z3
C = X2*Z3
D = Z2*X3
t12 = a*B
t13 = A-t12
t14 = C+D
t15 = t13^2
t16 = B*t14
t17 = b4*t16
X5 = t15-t17
t18 = C-D
t19 = t18^2
Z5 = X1*t19