t0 = X3-Z3
t1 = X2-Z2
X2 = X2+Z2
Z2 = X3+Z3
Z3 = t0*X2
Z2 = Z2*t1
t0 = t1^2
t1 = X2^2
X3 = Z3+Z2
Z2 = Z3-Z2
X4 = t1*t0
t1 = t1-t0
Z2 = Z2^2
Z3 = t1 * a24
X5 = X3^2
t0 = t0+Z3
Z5 = X1*Z2
Z4 = t1*t0