A = X1^2
t0 = X1+1
B = a2*t0
t1 = A+B
C = 3*t1
D = Y1^2
E = D^2
Z3 = 2*Y1
ZZ3 = 4*D
t2 = X1+D
t3 = t2^2
t4 = t3-A
t5 = t4-E
F = 2*t5
t6 = C^2
t7 = 2*F
t8 = a3*ZZ3
t9 = t6-t8
X3 = t9-t7
t10 = F-X3
t11 = 8*E
t12 = C*t10
Y3 = t12-t11