λ x x0 : word32 * word32 * word32 * word32 * word32, Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, uint32_t x21, uint32_t x22 = mulx_u32(x5, x13); uint32_t x24, uint32_t x25 = mulx_u32(x5, x15); uint32_t x27, uint32_t x28 = mulx_u32(x5, x17); uint32_t x30, uint32_t x31 = mulx_u32(x5, x19); uint32_t x33, uint32_t x34 = mulx_u32(x5, x18); uint32_t x36, uint8_t x37 = addcarryx_u32(0x0, x22, x24); uint32_t x39, uint8_t x40 = addcarryx_u32(x37, x25, x27); uint32_t x42, uint8_t x43 = addcarryx_u32(x40, x28, x30); uint32_t x45, uint8_t x46 = addcarryx_u32(x43, x31, x33); uint32_t x48, uint8_t _ = addcarryx_u32(0x0, x46, x34); uint32_t x51, uint32_t _ = mulx_u32(x21, 0xcccccccd); uint32_t x54, uint32_t x55 = mulx_u32(x51, 0xfffffffb); uint32_t x57, uint32_t x58 = mulx_u32(x51, 0xffffffff); uint32_t x60, uint32_t x61 = mulx_u32(x51, 0xffffffff); uint32_t x63, uint32_t x64 = mulx_u32(x51, 0xffffffff); uint32_t x66, uint8_t x67 = mulx_u32_out_u8(x51, 0x3); uint32_t x69, uint8_t x70 = addcarryx_u32(0x0, x55, x57); uint32_t x72, uint8_t x73 = addcarryx_u32(x70, x58, x60); uint32_t x75, uint8_t x76 = addcarryx_u32(x73, x61, x63); uint32_t x78, uint8_t x79 = addcarryx_u32(x76, x64, x66); uint8_t x80 = (x79 + x67); uint32_t _, uint8_t x83 = addcarryx_u32(0x0, x21, x54); uint32_t x85, uint8_t x86 = addcarryx_u32(x83, x36, x69); uint32_t x88, uint8_t x89 = addcarryx_u32(x86, x39, x72); uint32_t x91, uint8_t x92 = addcarryx_u32(x89, x42, x75); uint32_t x94, uint8_t x95 = addcarryx_u32(x92, x45, x78); uint32_t x97, uint8_t x98 = addcarryx_u32(x95, x48, x80); uint32_t x100, uint32_t x101 = mulx_u32(x7, x13); uint32_t x103, uint32_t x104 = mulx_u32(x7, x15); uint32_t x106, uint32_t x107 = mulx_u32(x7, x17); uint32_t x109, uint32_t x110 = mulx_u32(x7, x19); uint32_t x112, uint32_t x113 = mulx_u32(x7, x18); uint32_t x115, uint8_t x116 = addcarryx_u32(0x0, x101, x103); uint32_t x118, uint8_t x119 = addcarryx_u32(x116, x104, x106); uint32_t x121, uint8_t x122 = addcarryx_u32(x119, x107, x109); uint32_t x124, uint8_t x125 = addcarryx_u32(x122, x110, x112); uint32_t x127, uint8_t _ = addcarryx_u32(0x0, x125, x113); uint32_t x130, uint8_t x131 = addcarryx_u32(0x0, x85, x100); uint32_t x133, uint8_t x134 = addcarryx_u32(x131, x88, x115); uint32_t x136, uint8_t x137 = addcarryx_u32(x134, x91, x118); uint32_t x139, uint8_t x140 = addcarryx_u32(x137, x94, x121); uint32_t x142, uint8_t x143 = addcarryx_u32(x140, x97, x124); uint32_t x145, uint8_t x146 = addcarryx_u32(x143, x98, x127); uint32_t x148, uint32_t _ = mulx_u32(x130, 0xcccccccd); uint32_t x151, uint32_t x152 = mulx_u32(x148, 0xfffffffb); uint32_t x154, uint32_t x155 = mulx_u32(x148, 0xffffffff); uint32_t x157, uint32_t x158 = mulx_u32(x148, 0xffffffff); uint32_t x160, uint32_t x161 = mulx_u32(x148, 0xffffffff); uint32_t x163, uint8_t x164 = mulx_u32_out_u8(x148, 0x3); uint32_t x166, uint8_t x167 = addcarryx_u32(0x0, x152, x154); uint32_t x169, uint8_t x170 = addcarryx_u32(x167, x155, x157); uint32_t x172, uint8_t x173 = addcarryx_u32(x170, x158, x160); uint32_t x175, uint8_t x176 = addcarryx_u32(x173, x161, x163); uint8_t x177 = (x176 + x164); uint32_t _, uint8_t x180 = addcarryx_u32(0x0, x130, x151); uint32_t x182, uint8_t x183 = addcarryx_u32(x180, x133, x166); uint32_t x185, uint8_t x186 = addcarryx_u32(x183, x136, x169); uint32_t x188, uint8_t x189 = addcarryx_u32(x186, x139, x172); uint32_t x191, uint8_t x192 = addcarryx_u32(x189, x142, x175); uint32_t x194, uint8_t x195 = addcarryx_u32(x192, x145, x177); uint8_t x196 = (x195 + x146); uint32_t x198, uint32_t x199 = mulx_u32(x9, x13); uint32_t x201, uint32_t x202 = mulx_u32(x9, x15); uint32_t x204, uint32_t x205 = mulx_u32(x9, x17); uint32_t x207, uint32_t x208 = mulx_u32(x9, x19); uint32_t x210, uint32_t x211 = mulx_u32(x9, x18); uint32_t x213, uint8_t x214 = addcarryx_u32(0x0, x199, x201); uint32_t x216, uint8_t x217 = addcarryx_u32(x214, x202, x204); uint32_t x219, uint8_t x220 = addcarryx_u32(x217, x205, x207); uint32_t x222, uint8_t x223 = addcarryx_u32(x220, x208, x210); uint32_t x225, uint8_t _ = addcarryx_u32(0x0, x223, x211); uint32_t x228, uint8_t x229 = addcarryx_u32(0x0, x182, x198); uint32_t x231, uint8_t x232 = addcarryx_u32(x229, x185, x213); uint32_t x234, uint8_t x235 = addcarryx_u32(x232, x188, x216); uint32_t x237, uint8_t x238 = addcarryx_u32(x235, x191, x219); uint32_t x240, uint8_t x241 = addcarryx_u32(x238, x194, x222); uint32_t x243, uint8_t x244 = addcarryx_u32(x241, x196, x225); uint32_t x246, uint32_t _ = mulx_u32(x228, 0xcccccccd); uint32_t x249, uint32_t x250 = mulx_u32(x246, 0xfffffffb); uint32_t x252, uint32_t x253 = mulx_u32(x246, 0xffffffff); uint32_t x255, uint32_t x256 = mulx_u32(x246, 0xffffffff); uint32_t x258, uint32_t x259 = mulx_u32(x246, 0xffffffff); uint32_t x261, uint8_t x262 = mulx_u32_out_u8(x246, 0x3); uint32_t x264, uint8_t x265 = addcarryx_u32(0x0, x250, x252); uint32_t x267, uint8_t x268 = addcarryx_u32(x265, x253, x255); uint32_t x270, uint8_t x271 = addcarryx_u32(x268, x256, x258); uint32_t x273, uint8_t x274 = addcarryx_u32(x271, x259, x261); uint8_t x275 = (x274 + x262); uint32_t _, uint8_t x278 = addcarryx_u32(0x0, x228, x249); uint32_t x280, uint8_t x281 = addcarryx_u32(x278, x231, x264); uint32_t x283, uint8_t x284 = addcarryx_u32(x281, x234, x267); uint32_t x286, uint8_t x287 = addcarryx_u32(x284, x237, x270); uint32_t x289, uint8_t x290 = addcarryx_u32(x287, x240, x273); uint32_t x292, uint8_t x293 = addcarryx_u32(x290, x243, x275); uint8_t x294 = (x293 + x244); uint32_t x296, uint32_t x297 = mulx_u32(x11, x13); uint32_t x299, uint32_t x300 = mulx_u32(x11, x15); uint32_t x302, uint32_t x303 = mulx_u32(x11, x17); uint32_t x305, uint32_t x306 = mulx_u32(x11, x19); uint32_t x308, uint32_t x309 = mulx_u32(x11, x18); uint32_t x311, uint8_t x312 = addcarryx_u32(0x0, x297, x299); uint32_t x314, uint8_t x315 = addcarryx_u32(x312, x300, x302); uint32_t x317, uint8_t x318 = addcarryx_u32(x315, x303, x305); uint32_t x320, uint8_t x321 = addcarryx_u32(x318, x306, x308); uint32_t x323, uint8_t _ = addcarryx_u32(0x0, x321, x309); uint32_t x326, uint8_t x327 = addcarryx_u32(0x0, x280, x296); uint32_t x329, uint8_t x330 = addcarryx_u32(x327, x283, x311); uint32_t x332, uint8_t x333 = addcarryx_u32(x330, x286, x314); uint32_t x335, uint8_t x336 = addcarryx_u32(x333, x289, x317); uint32_t x338, uint8_t x339 = addcarryx_u32(x336, x292, x320); uint32_t x341, uint8_t x342 = addcarryx_u32(x339, x294, x323); uint32_t x344, uint32_t _ = mulx_u32(x326, 0xcccccccd); uint32_t x347, uint32_t x348 = mulx_u32(x344, 0xfffffffb); uint32_t x350, uint32_t x351 = mulx_u32(x344, 0xffffffff); uint32_t x353, uint32_t x354 = mulx_u32(x344, 0xffffffff); uint32_t x356, uint32_t x357 = mulx_u32(x344, 0xffffffff); uint32_t x359, uint8_t x360 = mulx_u32_out_u8(x344, 0x3); uint32_t x362, uint8_t x363 = addcarryx_u32(0x0, x348, x350); uint32_t x365, uint8_t x366 = addcarryx_u32(x363, x351, x353); uint32_t x368, uint8_t x369 = addcarryx_u32(x366, x354, x356); uint32_t x371, uint8_t x372 = addcarryx_u32(x369, x357, x359); uint8_t x373 = (x372 + x360); uint32_t _, uint8_t x376 = addcarryx_u32(0x0, x326, x347); uint32_t x378, uint8_t x379 = addcarryx_u32(x376, x329, x362); uint32_t x381, uint8_t x382 = addcarryx_u32(x379, x332, x365); uint32_t x384, uint8_t x385 = addcarryx_u32(x382, x335, x368); uint32_t x387, uint8_t x388 = addcarryx_u32(x385, x338, x371); uint32_t x390, uint8_t x391 = addcarryx_u32(x388, x341, x373); uint8_t x392 = (x391 + x342); uint32_t x394, uint32_t x395 = mulx_u32(x10, x13); uint32_t x397, uint32_t x398 = mulx_u32(x10, x15); uint32_t x400, uint32_t x401 = mulx_u32(x10, x17); uint32_t x403, uint32_t x404 = mulx_u32(x10, x19); uint32_t x406, uint32_t x407 = mulx_u32(x10, x18); uint32_t x409, uint8_t x410 = addcarryx_u32(0x0, x395, x397); uint32_t x412, uint8_t x413 = addcarryx_u32(x410, x398, x400); uint32_t x415, uint8_t x416 = addcarryx_u32(x413, x401, x403); uint32_t x418, uint8_t x419 = addcarryx_u32(x416, x404, x406); uint32_t x421, uint8_t _ = addcarryx_u32(0x0, x419, x407); uint32_t x424, uint8_t x425 = addcarryx_u32(0x0, x378, x394); uint32_t x427, uint8_t x428 = addcarryx_u32(x425, x381, x409); uint32_t x430, uint8_t x431 = addcarryx_u32(x428, x384, x412); uint32_t x433, uint8_t x434 = addcarryx_u32(x431, x387, x415); uint32_t x436, uint8_t x437 = addcarryx_u32(x434, x390, x418); uint32_t x439, uint8_t x440 = addcarryx_u32(x437, x392, x421); uint32_t x442, uint32_t _ = mulx_u32(x424, 0xcccccccd); uint32_t x445, uint32_t x446 = mulx_u32(x442, 0xfffffffb); uint32_t x448, uint32_t x449 = mulx_u32(x442, 0xffffffff); uint32_t x451, uint32_t x452 = mulx_u32(x442, 0xffffffff); uint32_t x454, uint32_t x455 = mulx_u32(x442, 0xffffffff); uint32_t x457, uint8_t x458 = mulx_u32_out_u8(x442, 0x3); uint32_t x460, uint8_t x461 = addcarryx_u32(0x0, x446, x448); uint32_t x463, uint8_t x464 = addcarryx_u32(x461, x449, x451); uint32_t x466, uint8_t x467 = addcarryx_u32(x464, x452, x454); uint32_t x469, uint8_t x470 = addcarryx_u32(x467, x455, x457); uint8_t x471 = (x470 + x458); uint32_t _, uint8_t x474 = addcarryx_u32(0x0, x424, x445); uint32_t x476, uint8_t x477 = addcarryx_u32(x474, x427, x460); uint32_t x479, uint8_t x480 = addcarryx_u32(x477, x430, x463); uint32_t x482, uint8_t x483 = addcarryx_u32(x480, x433, x466); uint32_t x485, uint8_t x486 = addcarryx_u32(x483, x436, x469); uint32_t x488, uint8_t x489 = addcarryx_u32(x486, x439, x471); uint8_t x490 = (x489 + x440); uint32_t x492, uint8_t x493 = subborrow_u32(0x0, x476, 0xfffffffb); uint32_t x495, uint8_t x496 = subborrow_u32(x493, x479, 0xffffffff); uint32_t x498, uint8_t x499 = subborrow_u32(x496, x482, 0xffffffff); uint32_t x501, uint8_t x502 = subborrow_u32(x499, x485, 0xffffffff); uint32_t x504, uint8_t x505 = subborrow_u32(x502, x488, 0x3); uint32_t _, uint8_t x508 = subborrow_u32(x505, x490, 0x0); uint32_t x509 = cmovznz32(x508, x504, x488); uint32_t x510 = cmovznz32(x508, x501, x485); uint32_t x511 = cmovznz32(x508, x498, x482); uint32_t x512 = cmovznz32(x508, x495, x479); uint32_t x513 = cmovznz32(x508, x492, x476); return (x509, x510, x511, x512, x513)) (x, x0)%core : word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)