double MRG32k5a (void);