λ x x0 : word32 * word32 * word32 * word32 * word32 * word32, Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, uint32_t x25, uint32_t x26 = mulx_u32(x5, x15); uint32_t x28, uint32_t x29 = mulx_u32(x5, x17); uint32_t x31, uint32_t x32 = mulx_u32(x5, x19); uint32_t x34, uint32_t x35 = mulx_u32(x5, x21); uint32_t x37, uint32_t x38 = mulx_u32(x5, x23); uint32_t x40, uint32_t x41 = mulx_u32(x5, x22); uint32_t x43, uint8_t x44 = addcarryx_u32(0x0, x26, x28); uint32_t x46, uint8_t x47 = addcarryx_u32(x44, x29, x31); uint32_t x49, uint8_t x50 = addcarryx_u32(x47, x32, x34); uint32_t x52, uint8_t x53 = addcarryx_u32(x50, x35, x37); uint32_t x55, uint8_t x56 = addcarryx_u32(x53, x38, x40); uint32_t x58, uint8_t _ = addcarryx_u32(0x0, x56, x41); uint32_t x61, uint32_t _ = mulx_u32(x25, 0xcccccccd); uint32_t x64, uint32_t x65 = mulx_u32(x61, 0xfffffffb); uint32_t x67, uint32_t x68 = mulx_u32(x61, 0xffffffff); uint32_t x70, uint32_t x71 = mulx_u32(x61, 0xffffffff); uint32_t x73, uint32_t x74 = mulx_u32(x61, 0xffffffff); uint32_t x76, uint32_t x77 = mulx_u32(x61, 0xffffffff); uint32_t x79, uint8_t x80 = mulx_u32_out_u8(x61, 0x3f); uint32_t x82, uint8_t x83 = addcarryx_u32(0x0, x65, x67); uint32_t x85, uint8_t x86 = addcarryx_u32(x83, x68, x70); uint32_t x88, uint8_t x89 = addcarryx_u32(x86, x71, x73); uint32_t x91, uint8_t x92 = addcarryx_u32(x89, x74, x76); uint32_t x94, uint8_t x95 = addcarryx_u32(x92, x77, x79); uint8_t x96 = (x95 + x80); uint32_t _, uint8_t x99 = addcarryx_u32(0x0, x25, x64); uint32_t x101, uint8_t x102 = addcarryx_u32(x99, x43, x82); uint32_t x104, uint8_t x105 = addcarryx_u32(x102, x46, x85); uint32_t x107, uint8_t x108 = addcarryx_u32(x105, x49, x88); uint32_t x110, uint8_t x111 = addcarryx_u32(x108, x52, x91); uint32_t x113, uint8_t x114 = addcarryx_u32(x111, x55, x94); uint32_t x116, uint8_t x117 = addcarryx_u32(x114, x58, x96); uint32_t x119, uint32_t x120 = mulx_u32(x7, x15); uint32_t x122, uint32_t x123 = mulx_u32(x7, x17); uint32_t x125, uint32_t x126 = mulx_u32(x7, x19); uint32_t x128, uint32_t x129 = mulx_u32(x7, x21); uint32_t x131, uint32_t x132 = mulx_u32(x7, x23); uint32_t x134, uint32_t x135 = mulx_u32(x7, x22); uint32_t x137, uint8_t x138 = addcarryx_u32(0x0, x120, x122); uint32_t x140, uint8_t x141 = addcarryx_u32(x138, x123, x125); uint32_t x143, uint8_t x144 = addcarryx_u32(x141, x126, x128); uint32_t x146, uint8_t x147 = addcarryx_u32(x144, x129, x131); uint32_t x149, uint8_t x150 = addcarryx_u32(x147, x132, x134); uint32_t x152, uint8_t _ = addcarryx_u32(0x0, x150, x135); uint32_t x155, uint8_t x156 = addcarryx_u32(0x0, x101, x119); uint32_t x158, uint8_t x159 = addcarryx_u32(x156, x104, x137); uint32_t x161, uint8_t x162 = addcarryx_u32(x159, x107, x140); uint32_t x164, uint8_t x165 = addcarryx_u32(x162, x110, x143); uint32_t x167, uint8_t x168 = addcarryx_u32(x165, x113, x146); uint32_t x170, uint8_t x171 = addcarryx_u32(x168, x116, x149); uint32_t x173, uint8_t x174 = addcarryx_u32(x171, x117, x152); uint32_t x176, uint32_t _ = mulx_u32(x155, 0xcccccccd); uint32_t x179, uint32_t x180 = mulx_u32(x176, 0xfffffffb); uint32_t x182, uint32_t x183 = mulx_u32(x176, 0xffffffff); uint32_t x185, uint32_t x186 = mulx_u32(x176, 0xffffffff); uint32_t x188, uint32_t x189 = mulx_u32(x176, 0xffffffff); uint32_t x191, uint32_t x192 = mulx_u32(x176, 0xffffffff); uint32_t x194, uint8_t x195 = mulx_u32_out_u8(x176, 0x3f); uint32_t x197, uint8_t x198 = addcarryx_u32(0x0, x180, x182); uint32_t x200, uint8_t x201 = addcarryx_u32(x198, x183, x185); uint32_t x203, uint8_t x204 = addcarryx_u32(x201, x186, x188); uint32_t x206, uint8_t x207 = addcarryx_u32(x204, x189, x191); uint32_t x209, uint8_t x210 = addcarryx_u32(x207, x192, x194); uint8_t x211 = (x210 + x195); uint32_t _, uint8_t x214 = addcarryx_u32(0x0, x155, x179); uint32_t x216, uint8_t x217 = addcarryx_u32(x214, x158, x197); uint32_t x219, uint8_t x220 = addcarryx_u32(x217, x161, x200); uint32_t x222, uint8_t x223 = addcarryx_u32(x220, x164, x203); uint32_t x225, uint8_t x226 = addcarryx_u32(x223, x167, x206); uint32_t x228, uint8_t x229 = addcarryx_u32(x226, x170, x209); uint32_t x231, uint8_t x232 = addcarryx_u32(x229, x173, x211); uint8_t x233 = (x232 + x174); uint32_t x235, uint32_t x236 = mulx_u32(x9, x15); uint32_t x238, uint32_t x239 = mulx_u32(x9, x17); uint32_t x241, uint32_t x242 = mulx_u32(x9, x19); uint32_t x244, uint32_t x245 = mulx_u32(x9, x21); uint32_t x247, uint32_t x248 = mulx_u32(x9, x23); uint32_t x250, uint32_t x251 = mulx_u32(x9, x22); uint32_t x253, uint8_t x254 = addcarryx_u32(0x0, x236, x238); uint32_t x256, uint8_t x257 = addcarryx_u32(x254, x239, x241); uint32_t x259, uint8_t x260 = addcarryx_u32(x257, x242, x244); uint32_t x262, uint8_t x263 = addcarryx_u32(x260, x245, x247); uint32_t x265, uint8_t x266 = addcarryx_u32(x263, x248, x250); uint32_t x268, uint8_t _ = addcarryx_u32(0x0, x266, x251); uint32_t x271, uint8_t x272 = addcarryx_u32(0x0, x216, x235); uint32_t x274, uint8_t x275 = addcarryx_u32(x272, x219, x253); uint32_t x277, uint8_t x278 = addcarryx_u32(x275, x222, x256); uint32_t x280, uint8_t x281 = addcarryx_u32(x278, x225, x259); uint32_t x283, uint8_t x284 = addcarryx_u32(x281, x228, x262); uint32_t x286, uint8_t x287 = addcarryx_u32(x284, x231, x265); uint32_t x289, uint8_t x290 = addcarryx_u32(x287, x233, x268); uint32_t x292, uint32_t _ = mulx_u32(x271, 0xcccccccd); uint32_t x295, uint32_t x296 = mulx_u32(x292, 0xfffffffb); uint32_t x298, uint32_t x299 = mulx_u32(x292, 0xffffffff); uint32_t x301, uint32_t x302 = mulx_u32(x292, 0xffffffff); uint32_t x304, uint32_t x305 = mulx_u32(x292, 0xffffffff); uint32_t x307, uint32_t x308 = mulx_u32(x292, 0xffffffff); uint32_t x310, uint8_t x311 = mulx_u32_out_u8(x292, 0x3f); uint32_t x313, uint8_t x314 = addcarryx_u32(0x0, x296, x298); uint32_t x316, uint8_t x317 = addcarryx_u32(x314, x299, x301); uint32_t x319, uint8_t x320 = addcarryx_u32(x317, x302, x304); uint32_t x322, uint8_t x323 = addcarryx_u32(x320, x305, x307); uint32_t x325, uint8_t x326 = addcarryx_u32(x323, x308, x310); uint8_t x327 = (x326 + x311); uint32_t _, uint8_t x330 = addcarryx_u32(0x0, x271, x295); uint32_t x332, uint8_t x333 = addcarryx_u32(x330, x274, x313); uint32_t x335, uint8_t x336 = addcarryx_u32(x333, x277, x316); uint32_t x338, uint8_t x339 = addcarryx_u32(x336, x280, x319); uint32_t x341, uint8_t x342 = addcarryx_u32(x339, x283, x322); uint32_t x344, uint8_t x345 = addcarryx_u32(x342, x286, x325); uint32_t x347, uint8_t x348 = addcarryx_u32(x345, x289, x327); uint8_t x349 = (x348 + x290); uint32_t x351, uint32_t x352 = mulx_u32(x11, x15); uint32_t x354, uint32_t x355 = mulx_u32(x11, x17); uint32_t x357, uint32_t x358 = mulx_u32(x11, x19); uint32_t x360, uint32_t x361 = mulx_u32(x11, x21); uint32_t x363, uint32_t x364 = mulx_u32(x11, x23); uint32_t x366, uint32_t x367 = mulx_u32(x11, x22); uint32_t x369, uint8_t x370 = addcarryx_u32(0x0, x352, x354); uint32_t x372, uint8_t x373 = addcarryx_u32(x370, x355, x357); uint32_t x375, uint8_t x376 = addcarryx_u32(x373, x358, x360); uint32_t x378, uint8_t x379 = addcarryx_u32(x376, x361, x363); uint32_t x381, uint8_t x382 = addcarryx_u32(x379, x364, x366); uint32_t x384, uint8_t _ = addcarryx_u32(0x0, x382, x367); uint32_t x387, uint8_t x388 = addcarryx_u32(0x0, x332, x351); uint32_t x390, uint8_t x391 = addcarryx_u32(x388, x335, x369); uint32_t x393, uint8_t x394 = addcarryx_u32(x391, x338, x372); uint32_t x396, uint8_t x397 = addcarryx_u32(x394, x341, x375); uint32_t x399, uint8_t x400 = addcarryx_u32(x397, x344, x378); uint32_t x402, uint8_t x403 = addcarryx_u32(x400, x347, x381); uint32_t x405, uint8_t x406 = addcarryx_u32(x403, x349, x384); uint32_t x408, uint32_t _ = mulx_u32(x387, 0xcccccccd); uint32_t x411, uint32_t x412 = mulx_u32(x408, 0xfffffffb); uint32_t x414, uint32_t x415 = mulx_u32(x408, 0xffffffff); uint32_t x417, uint32_t x418 = mulx_u32(x408, 0xffffffff); uint32_t x420, uint32_t x421 = mulx_u32(x408, 0xffffffff); uint32_t x423, uint32_t x424 = mulx_u32(x408, 0xffffffff); uint32_t x426, uint8_t x427 = mulx_u32_out_u8(x408, 0x3f); uint32_t x429, uint8_t x430 = addcarryx_u32(0x0, x412, x414); uint32_t x432, uint8_t x433 = addcarryx_u32(x430, x415, x417); uint32_t x435, uint8_t x436 = addcarryx_u32(x433, x418, x420); uint32_t x438, uint8_t x439 = addcarryx_u32(x436, x421, x423); uint32_t x441, uint8_t x442 = addcarryx_u32(x439, x424, x426); uint8_t x443 = (x442 + x427); uint32_t _, uint8_t x446 = addcarryx_u32(0x0, x387, x411); uint32_t x448, uint8_t x449 = addcarryx_u32(x446, x390, x429); uint32_t x451, uint8_t x452 = addcarryx_u32(x449, x393, x432); uint32_t x454, uint8_t x455 = addcarryx_u32(x452, x396, x435); uint32_t x457, uint8_t x458 = addcarryx_u32(x455, x399, x438); uint32_t x460, uint8_t x461 = addcarryx_u32(x458, x402, x441); uint32_t x463, uint8_t x464 = addcarryx_u32(x461, x405, x443); uint8_t x465 = (x464 + x406); uint32_t x467, uint32_t x468 = mulx_u32(x13, x15); uint32_t x470, uint32_t x471 = mulx_u32(x13, x17); uint32_t x473, uint32_t x474 = mulx_u32(x13, x19); uint32_t x476, uint32_t x477 = mulx_u32(x13, x21); uint32_t x479, uint32_t x480 = mulx_u32(x13, x23); uint32_t x482, uint32_t x483 = mulx_u32(x13, x22); uint32_t x485, uint8_t x486 = addcarryx_u32(0x0, x468, x470); uint32_t x488, uint8_t x489 = addcarryx_u32(x486, x471, x473); uint32_t x491, uint8_t x492 = addcarryx_u32(x489, x474, x476); uint32_t x494, uint8_t x495 = addcarryx_u32(x492, x477, x479); uint32_t x497, uint8_t x498 = addcarryx_u32(x495, x480, x482); uint32_t x500, uint8_t _ = addcarryx_u32(0x0, x498, x483); uint32_t x503, uint8_t x504 = addcarryx_u32(0x0, x448, x467); uint32_t x506, uint8_t x507 = addcarryx_u32(x504, x451, x485); uint32_t x509, uint8_t x510 = addcarryx_u32(x507, x454, x488); uint32_t x512, uint8_t x513 = addcarryx_u32(x510, x457, x491); uint32_t x515, uint8_t x516 = addcarryx_u32(x513, x460, x494); uint32_t x518, uint8_t x519 = addcarryx_u32(x516, x463, x497); uint32_t x521, uint8_t x522 = addcarryx_u32(x519, x465, x500); uint32_t x524, uint32_t _ = mulx_u32(x503, 0xcccccccd); uint32_t x527, uint32_t x528 = mulx_u32(x524, 0xfffffffb); uint32_t x530, uint32_t x531 = mulx_u32(x524, 0xffffffff); uint32_t x533, uint32_t x534 = mulx_u32(x524, 0xffffffff); uint32_t x536, uint32_t x537 = mulx_u32(x524, 0xffffffff); uint32_t x539, uint32_t x540 = mulx_u32(x524, 0xffffffff); uint32_t x542, uint8_t x543 = mulx_u32_out_u8(x524, 0x3f); uint32_t x545, uint8_t x546 = addcarryx_u32(0x0, x528, x530); uint32_t x548, uint8_t x549 = addcarryx_u32(x546, x531, x533); uint32_t x551, uint8_t x552 = addcarryx_u32(x549, x534, x536); uint32_t x554, uint8_t x555 = addcarryx_u32(x552, x537, x539); uint32_t x557, uint8_t x558 = addcarryx_u32(x555, x540, x542); uint8_t x559 = (x558 + x543); uint32_t _, uint8_t x562 = addcarryx_u32(0x0, x503, x527); uint32_t x564, uint8_t x565 = addcarryx_u32(x562, x506, x545); uint32_t x567, uint8_t x568 = addcarryx_u32(x565, x509, x548); uint32_t x570, uint8_t x571 = addcarryx_u32(x568, x512, x551); uint32_t x573, uint8_t x574 = addcarryx_u32(x571, x515, x554); uint32_t x576, uint8_t x577 = addcarryx_u32(x574, x518, x557); uint32_t x579, uint8_t x580 = addcarryx_u32(x577, x521, x559); uint8_t x581 = (x580 + x522); uint32_t x583, uint32_t x584 = mulx_u32(x12, x15); uint32_t x586, uint32_t x587 = mulx_u32(x12, x17); uint32_t x589, uint32_t x590 = mulx_u32(x12, x19); uint32_t x592, uint32_t x593 = mulx_u32(x12, x21); uint32_t x595, uint32_t x596 = mulx_u32(x12, x23); uint32_t x598, uint32_t x599 = mulx_u32(x12, x22); uint32_t x601, uint8_t x602 = addcarryx_u32(0x0, x584, x586); uint32_t x604, uint8_t x605 = addcarryx_u32(x602, x587, x589); uint32_t x607, uint8_t x608 = addcarryx_u32(x605, x590, x592); uint32_t x610, uint8_t x611 = addcarryx_u32(x608, x593, x595); uint32_t x613, uint8_t x614 = addcarryx_u32(x611, x596, x598); uint32_t x616, uint8_t _ = addcarryx_u32(0x0, x614, x599); uint32_t x619, uint8_t x620 = addcarryx_u32(0x0, x564, x583); uint32_t x622, uint8_t x623 = addcarryx_u32(x620, x567, x601); uint32_t x625, uint8_t x626 = addcarryx_u32(x623, x570, x604); uint32_t x628, uint8_t x629 = addcarryx_u32(x626, x573, x607); uint32_t x631, uint8_t x632 = addcarryx_u32(x629, x576, x610); uint32_t x634, uint8_t x635 = addcarryx_u32(x632, x579, x613); uint32_t x637, uint8_t x638 = addcarryx_u32(x635, x581, x616); uint32_t x640, uint32_t _ = mulx_u32(x619, 0xcccccccd); uint32_t x643, uint32_t x644 = mulx_u32(x640, 0xfffffffb); uint32_t x646, uint32_t x647 = mulx_u32(x640, 0xffffffff); uint32_t x649, uint32_t x650 = mulx_u32(x640, 0xffffffff); uint32_t x652, uint32_t x653 = mulx_u32(x640, 0xffffffff); uint32_t x655, uint32_t x656 = mulx_u32(x640, 0xffffffff); uint32_t x658, uint8_t x659 = mulx_u32_out_u8(x640, 0x3f); uint32_t x661, uint8_t x662 = addcarryx_u32(0x0, x644, x646); uint32_t x664, uint8_t x665 = addcarryx_u32(x662, x647, x649); uint32_t x667, uint8_t x668 = addcarryx_u32(x665, x650, x652); uint32_t x670, uint8_t x671 = addcarryx_u32(x668, x653, x655); uint32_t x673, uint8_t x674 = addcarryx_u32(x671, x656, x658); uint8_t x675 = (x674 + x659); uint32_t _, uint8_t x678 = addcarryx_u32(0x0, x619, x643); uint32_t x680, uint8_t x681 = addcarryx_u32(x678, x622, x661); uint32_t x683, uint8_t x684 = addcarryx_u32(x681, x625, x664); uint32_t x686, uint8_t x687 = addcarryx_u32(x684, x628, x667); uint32_t x689, uint8_t x690 = addcarryx_u32(x687, x631, x670); uint32_t x692, uint8_t x693 = addcarryx_u32(x690, x634, x673); uint32_t x695, uint8_t x696 = addcarryx_u32(x693, x637, x675); uint8_t x697 = (x696 + x638); uint32_t x699, uint8_t x700 = subborrow_u32(0x0, x680, 0xfffffffb); uint32_t x702, uint8_t x703 = subborrow_u32(x700, x683, 0xffffffff); uint32_t x705, uint8_t x706 = subborrow_u32(x703, x686, 0xffffffff); uint32_t x708, uint8_t x709 = subborrow_u32(x706, x689, 0xffffffff); uint32_t x711, uint8_t x712 = subborrow_u32(x709, x692, 0xffffffff); uint32_t x714, uint8_t x715 = subborrow_u32(x712, x695, 0x3f); uint32_t _, uint8_t x718 = subborrow_u32(x715, x697, 0x0); uint32_t x719 = cmovznz32(x718, x714, x695); uint32_t x720 = cmovznz32(x718, x711, x692); uint32_t x721 = cmovznz32(x718, x708, x689); uint32_t x722 = cmovznz32(x718, x705, x686); uint32_t x723 = cmovznz32(x718, x702, x683); uint32_t x724 = cmovznz32(x718, x699, x680); return (x719, x720, x721, x722, x723, x724)) (x, x0)%core : word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)