VADDSS X11, X9, X11                     // c4413258db
	VADDSUBPD (BX), X9, X2                  // c4e131d013 or c5b1d013
	VADDSUBPD (R11), X9, X2                 // c4c131d013
	VADDSUBPD X2, X9, X2                    // c4e131d0d2 or c5b1d0d2
	VADDSUBPD X11, X9, X2                   // c4c131d0d3
	VADDSUBPD (BX), X9, X11                 // c46131d01b or c531d01b

:= arg1[5] x6 := arg1[6] x7 := arg1[7] x8 := arg1[8] x9 := arg1[0] var x10 uint64 var x11 uint64 x11, x10 = bits.Mul64(x9, arg2[8]) var x12 uint64 var x13 uint64 x13, x12 = bits.Mul64(x9, arg2[7]) var x14 uint64 var x15 uint64 x15, x14 = bits.Mul64(x9, arg2[6]) var x16 uint64 var x17 uint64 x17, x16 = bits.Mul64(x9, arg2[5]) var x18 uint64 var x19 uint64 x19, x18 = bits.Mul64(x9, arg2[4]) var x20 uint64 var x21 uint64 x21, x20 = bits.Mul64(x9, arg2[3]) var x22 uint64 var x23 uint64 x23, x22 = bits.Mul64(x9,...