l1 = X1^2
l1 = l1 * 3
t1 = Z1^4
t1 = t1 * a
l1 = l1 + t1
Z3 = Y1 * Z1
Z3 = Z3 * 2
t2 = Y1^2
l2 = t2 * X1
l2 = l2 * 4
X3 = l1^2
t1 = l2 * 2
X3 = X3 - t1
t2 = t2^2
l3 = t2 * 8
Y3 = l2 - X3
Y3 = Y3 * l1
Y3 = Y3 - l3