λ 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, 0xc28f5c29); uint32_t x54, uint32_t x55 = mulx_u32(x51, 0xffffffe7); 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 = addcarryx_u32(0x0, x55, x57); uint32_t x69, uint8_t x70 = addcarryx_u32(x67, x58, x60); uint32_t x72, uint8_t x73 = addcarryx_u32(x70, x61, x63); uint32_t x75, uint8_t x76 = addcarryx_u32(x73, x64, x51); uint32_t _, uint8_t x79 = addcarryx_u32(0x0, x21, x54); uint32_t x81, uint8_t x82 = addcarryx_u32(x79, x36, x66); uint32_t x84, uint8_t x85 = addcarryx_u32(x82, x39, x69); uint32_t x87, uint8_t x88 = addcarryx_u32(x85, x42, x72); uint32_t x90, uint8_t x91 = addcarryx_u32(x88, x45, x75); uint32_t x93, uint8_t x94 = addcarryx_u32(x91, x48, x76); uint32_t x96, uint32_t x97 = mulx_u32(x7, x13); uint32_t x99, uint32_t x100 = mulx_u32(x7, x15); uint32_t x102, uint32_t x103 = mulx_u32(x7, x17); uint32_t x105, uint32_t x106 = mulx_u32(x7, x19); uint32_t x108, uint32_t x109 = mulx_u32(x7, x18); uint32_t x111, uint8_t x112 = addcarryx_u32(0x0, x97, x99); uint32_t x114, uint8_t x115 = addcarryx_u32(x112, x100, x102); uint32_t x117, uint8_t x118 = addcarryx_u32(x115, x103, x105); uint32_t x120, uint8_t x121 = addcarryx_u32(x118, x106, x108); uint32_t x123, uint8_t _ = addcarryx_u32(0x0, x121, x109); uint32_t x126, uint8_t x127 = addcarryx_u32(0x0, x81, x96); uint32_t x129, uint8_t x130 = addcarryx_u32(x127, x84, x111); uint32_t x132, uint8_t x133 = addcarryx_u32(x130, x87, x114); uint32_t x135, uint8_t x136 = addcarryx_u32(x133, x90, x117); uint32_t x138, uint8_t x139 = addcarryx_u32(x136, x93, x120); uint32_t x141, uint8_t x142 = addcarryx_u32(x139, x94, x123); uint32_t x144, uint32_t _ = mulx_u32(x126, 0xc28f5c29); uint32_t x147, uint32_t x148 = mulx_u32(x144, 0xffffffe7); uint32_t x150, uint32_t x151 = mulx_u32(x144, 0xffffffff); uint32_t x153, uint32_t x154 = mulx_u32(x144, 0xffffffff); uint32_t x156, uint32_t x157 = mulx_u32(x144, 0xffffffff); uint32_t x159, uint8_t x160 = addcarryx_u32(0x0, x148, x150); uint32_t x162, uint8_t x163 = addcarryx_u32(x160, x151, x153); uint32_t x165, uint8_t x166 = addcarryx_u32(x163, x154, x156); uint32_t x168, uint8_t x169 = addcarryx_u32(x166, x157, x144); uint32_t _, uint8_t x172 = addcarryx_u32(0x0, x126, x147); uint32_t x174, uint8_t x175 = addcarryx_u32(x172, x129, x159); uint32_t x177, uint8_t x178 = addcarryx_u32(x175, x132, x162); uint32_t x180, uint8_t x181 = addcarryx_u32(x178, x135, x165); uint32_t x183, uint8_t x184 = addcarryx_u32(x181, x138, x168); uint32_t x186, uint8_t x187 = addcarryx_u32(x184, x141, x169); uint8_t x188 = (x187 + x142); uint32_t x190, uint32_t x191 = mulx_u32(x9, x13); uint32_t x193, uint32_t x194 = mulx_u32(x9, x15); uint32_t x196, uint32_t x197 = mulx_u32(x9, x17); uint32_t x199, uint32_t x200 = mulx_u32(x9, x19); uint32_t x202, uint32_t x203 = mulx_u32(x9, x18); uint32_t x205, uint8_t x206 = addcarryx_u32(0x0, x191, x193); uint32_t x208, uint8_t x209 = addcarryx_u32(x206, x194, x196); uint32_t x211, uint8_t x212 = addcarryx_u32(x209, x197, x199); uint32_t x214, uint8_t x215 = addcarryx_u32(x212, x200, x202); uint32_t x217, uint8_t _ = addcarryx_u32(0x0, x215, x203); uint32_t x220, uint8_t x221 = addcarryx_u32(0x0, x174, x190); uint32_t x223, uint8_t x224 = addcarryx_u32(x221, x177, x205); uint32_t x226, uint8_t x227 = addcarryx_u32(x224, x180, x208); uint32_t x229, uint8_t x230 = addcarryx_u32(x227, x183, x211); uint32_t x232, uint8_t x233 = addcarryx_u32(x230, x186, x214); uint32_t x235, uint8_t x236 = addcarryx_u32(x233, x188, x217); uint32_t x238, uint32_t _ = mulx_u32(x220, 0xc28f5c29); uint32_t x241, uint32_t x242 = mulx_u32(x238, 0xffffffe7); uint32_t x244, uint32_t x245 = mulx_u32(x238, 0xffffffff); uint32_t x247, uint32_t x248 = mulx_u32(x238, 0xffffffff); uint32_t x250, uint32_t x251 = mulx_u32(x238, 0xffffffff); uint32_t x253, uint8_t x254 = addcarryx_u32(0x0, x242, x244); uint32_t x256, uint8_t x257 = addcarryx_u32(x254, x245, x247); uint32_t x259, uint8_t x260 = addcarryx_u32(x257, x248, x250); uint32_t x262, uint8_t x263 = addcarryx_u32(x260, x251, x238); uint32_t _, uint8_t x266 = addcarryx_u32(0x0, x220, x241); uint32_t x268, uint8_t x269 = addcarryx_u32(x266, x223, x253); uint32_t x271, uint8_t x272 = addcarryx_u32(x269, x226, x256); uint32_t x274, uint8_t x275 = addcarryx_u32(x272, x229, x259); uint32_t x277, uint8_t x278 = addcarryx_u32(x275, x232, x262); uint32_t x280, uint8_t x281 = addcarryx_u32(x278, x235, x263); uint8_t x282 = (x281 + x236); uint32_t x284, uint32_t x285 = mulx_u32(x11, x13); uint32_t x287, uint32_t x288 = mulx_u32(x11, x15); uint32_t x290, uint32_t x291 = mulx_u32(x11, x17); uint32_t x293, uint32_t x294 = mulx_u32(x11, x19); uint32_t x296, uint32_t x297 = mulx_u32(x11, x18); uint32_t x299, uint8_t x300 = addcarryx_u32(0x0, x285, x287); uint32_t x302, uint8_t x303 = addcarryx_u32(x300, x288, x290); uint32_t x305, uint8_t x306 = addcarryx_u32(x303, x291, x293); uint32_t x308, uint8_t x309 = addcarryx_u32(x306, x294, x296); uint32_t x311, uint8_t _ = addcarryx_u32(0x0, x309, x297); uint32_t x314, uint8_t x315 = addcarryx_u32(0x0, x268, x284); uint32_t x317, uint8_t x318 = addcarryx_u32(x315, x271, x299); uint32_t x320, uint8_t x321 = addcarryx_u32(x318, x274, x302); uint32_t x323, uint8_t x324 = addcarryx_u32(x321, x277, x305); uint32_t x326, uint8_t x327 = addcarryx_u32(x324, x280, x308); uint32_t x329, uint8_t x330 = addcarryx_u32(x327, x282, x311); uint32_t x332, uint32_t _ = mulx_u32(x314, 0xc28f5c29); uint32_t x335, uint32_t x336 = mulx_u32(x332, 0xffffffe7); uint32_t x338, uint32_t x339 = mulx_u32(x332, 0xffffffff); uint32_t x341, uint32_t x342 = mulx_u32(x332, 0xffffffff); uint32_t x344, uint32_t x345 = mulx_u32(x332, 0xffffffff); uint32_t x347, uint8_t x348 = addcarryx_u32(0x0, x336, x338); uint32_t x350, uint8_t x351 = addcarryx_u32(x348, x339, x341); uint32_t x353, uint8_t x354 = addcarryx_u32(x351, x342, x344); uint32_t x356, uint8_t x357 = addcarryx_u32(x354, x345, x332); uint32_t _, uint8_t x360 = addcarryx_u32(0x0, x314, x335); uint32_t x362, uint8_t x363 = addcarryx_u32(x360, x317, x347); uint32_t x365, uint8_t x366 = addcarryx_u32(x363, x320, x350); uint32_t x368, uint8_t x369 = addcarryx_u32(x366, x323, x353); uint32_t x371, uint8_t x372 = addcarryx_u32(x369, x326, x356); uint32_t x374, uint8_t x375 = addcarryx_u32(x372, x329, x357); uint8_t x376 = (x375 + x330); uint32_t x378, uint32_t x379 = mulx_u32(x10, x13); uint32_t x381, uint32_t x382 = mulx_u32(x10, x15); uint32_t x384, uint32_t x385 = mulx_u32(x10, x17); uint32_t x387, uint32_t x388 = mulx_u32(x10, x19); uint32_t x390, uint32_t x391 = mulx_u32(x10, x18); uint32_t x393, uint8_t x394 = addcarryx_u32(0x0, x379, x381); uint32_t x396, uint8_t x397 = addcarryx_u32(x394, x382, x384); uint32_t x399, uint8_t x400 = addcarryx_u32(x397, x385, x387); uint32_t x402, uint8_t x403 = addcarryx_u32(x400, x388, x390); uint32_t x405, uint8_t _ = addcarryx_u32(0x0, x403, x391); uint32_t x408, uint8_t x409 = addcarryx_u32(0x0, x362, x378); uint32_t x411, uint8_t x412 = addcarryx_u32(x409, x365, x393); uint32_t x414, uint8_t x415 = addcarryx_u32(x412, x368, x396); uint32_t x417, uint8_t x418 = addcarryx_u32(x415, x371, x399); uint32_t x420, uint8_t x421 = addcarryx_u32(x418, x374, x402); uint32_t x423, uint8_t x424 = addcarryx_u32(x421, x376, x405); uint32_t x426, uint32_t _ = mulx_u32(x408, 0xc28f5c29); uint32_t x429, uint32_t x430 = mulx_u32(x426, 0xffffffe7); uint32_t x432, uint32_t x433 = mulx_u32(x426, 0xffffffff); uint32_t x435, uint32_t x436 = mulx_u32(x426, 0xffffffff); uint32_t x438, uint32_t x439 = mulx_u32(x426, 0xffffffff); uint32_t x441, uint8_t x442 = addcarryx_u32(0x0, x430, x432); uint32_t x444, uint8_t x445 = addcarryx_u32(x442, x433, x435); uint32_t x447, uint8_t x448 = addcarryx_u32(x445, x436, x438); uint32_t x450, uint8_t x451 = addcarryx_u32(x448, x439, x426); uint32_t _, uint8_t x454 = addcarryx_u32(0x0, x408, x429); uint32_t x456, uint8_t x457 = addcarryx_u32(x454, x411, x441); uint32_t x459, uint8_t x460 = addcarryx_u32(x457, x414, x444); uint32_t x462, uint8_t x463 = addcarryx_u32(x460, x417, x447); uint32_t x465, uint8_t x466 = addcarryx_u32(x463, x420, x450); uint32_t x468, uint8_t x469 = addcarryx_u32(x466, x423, x451); uint8_t x470 = (x469 + x424); uint32_t x472, uint8_t x473 = subborrow_u32(0x0, x456, 0xffffffe7); uint32_t x475, uint8_t x476 = subborrow_u32(x473, x459, 0xffffffff); uint32_t x478, uint8_t x479 = subborrow_u32(x476, x462, 0xffffffff); uint32_t x481, uint8_t x482 = subborrow_u32(x479, x465, 0xffffffff); uint32_t x484, uint8_t x485 = subborrow_u32(x482, x468, 0x1); uint32_t _, uint8_t x488 = subborrow_u32(x485, x470, 0x0); uint32_t x489 = cmovznz32(x488, x484, x468); uint32_t x490 = cmovznz32(x488, x481, x465); uint32_t x491 = cmovznz32(x488, x478, x462); uint32_t x492 = cmovznz32(x488, x475, x459); uint32_t x493 = cmovznz32(x488, x472, x456); return (x489, x490, x491, x492, x493)) (x, x0)%core : word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)