source 2008.02.25 Hisil--Wong--Carter--Dawson, plus assumption Z1=1
assume Z1 = 1
compute SC1 = S1 C1
compute E = D1^2
compute F = SC1^2
compute G = a F
compute Z3 = E+G
compute D3 = E-G
compute CC1 = C1^2
compute C3 = 2(F+CC1^2)-Z3
compute S3 = (SC1+D1)^2-E-F