λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64, Interp-η (λ var : Syntax.base_type → Type, λ '(x14, x15, x13, x11, x9, x7, x5, (x26, x27, x25, x23, x21, x19, x17))%core, uint64_t x29, uint64_t x30 = mulx_u64(x5, x17); uint64_t x32, uint64_t x33 = mulx_u64(x5, x19); uint64_t x35, uint64_t x36 = mulx_u64(x5, x21); uint64_t x38, uint64_t x39 = mulx_u64(x5, x23); uint64_t x41, uint64_t x42 = mulx_u64(x5, x25); uint64_t x44, uint64_t x45 = mulx_u64(x5, x27); uint64_t x47, uint64_t x48 = mulx_u64(x5, x26); uint64_t x50, uint8_t x51 = addcarryx_u64(0x0, x30, x32); uint64_t x53, uint8_t x54 = addcarryx_u64(x51, x33, x35); uint64_t x56, uint8_t x57 = addcarryx_u64(x54, x36, x38); uint64_t x59, uint8_t x60 = addcarryx_u64(x57, x39, x41); uint64_t x62, uint8_t x63 = addcarryx_u64(x60, x42, x44); uint64_t x65, uint8_t x66 = addcarryx_u64(x63, x45, x47); uint64_t x68, uint8_t _ = addcarryx_u64(0x0, x66, x48); uint64_t x71, uint64_t x72 = mulx_u64(x29, 0xffffffffffffffffL); uint64_t x74, uint64_t x75 = mulx_u64(x29, 0xffffffffffffffffL); uint64_t x77, uint64_t x78 = mulx_u64(x29, 0xffffffffffffffffL); uint64_t x80, uint64_t x81 = mulx_u64(x29, 0xfffffffffffeffffL); uint64_t x83, uint64_t x84 = mulx_u64(x29, 0xffffffffffffffffL); uint64_t x86, uint64_t x87 = mulx_u64(x29, 0xffffffffffffffffL); uint64_t x89, uint64_t x90 = mulx_u64(x29, 0xffffffff); uint64_t x92, uint8_t x93 = addcarryx_u64(0x0, x72, x74); uint64_t x95, uint8_t x96 = addcarryx_u64(x93, x75, x77); uint64_t x98, uint8_t x99 = addcarryx_u64(x96, x78, x80); uint64_t x101, uint8_t x102 = addcarryx_u64(x99, x81, x83); uint64_t x104, uint8_t x105 = addcarryx_u64(x102, x84, x86); uint64_t x107, uint8_t x108 = addcarryx_u64(x105, x87, x89); uint64_t x110, uint8_t _ = addcarryx_u64(0x0, x108, x90); uint64_t _, uint8_t x114 = addcarryx_u64(0x0, x29, x71); uint64_t x116, uint8_t x117 = addcarryx_u64(x114, x50, x92); uint64_t x119, uint8_t x120 = addcarryx_u64(x117, x53, x95); uint64_t x122, uint8_t x123 = addcarryx_u64(x120, x56, x98); uint64_t x125, uint8_t x126 = addcarryx_u64(x123, x59, x101); uint64_t x128, uint8_t x129 = addcarryx_u64(x126, x62, x104); uint64_t x131, uint8_t x132 = addcarryx_u64(x129, x65, x107); uint64_t x134, uint8_t x135 = addcarryx_u64(x132, x68, x110); uint64_t x137, uint64_t x138 = mulx_u64(x7, x17); uint64_t x140, uint64_t x141 = mulx_u64(x7, x19); uint64_t x143, uint64_t x144 = mulx_u64(x7, x21); uint64_t x146, uint64_t x147 = mulx_u64(x7, x23); uint64_t x149, uint64_t x150 = mulx_u64(x7, x25); uint64_t x152, uint64_t x153 = mulx_u64(x7, x27); uint64_t x155, uint64_t x156 = mulx_u64(x7, x26); uint64_t x158, uint8_t x159 = addcarryx_u64(0x0, x138, x140); uint64_t x161, uint8_t x162 = addcarryx_u64(x159, x141, x143); uint64_t x164, uint8_t x165 = addcarryx_u64(x162, x144, x146); uint64_t x167, uint8_t x168 = addcarryx_u64(x165, x147, x149); uint64_t x170, uint8_t x171 = addcarryx_u64(x168, x150, x152); uint64_t x173, uint8_t x174 = addcarryx_u64(x171, x153, x155); uint64_t x176, uint8_t _ = addcarryx_u64(0x0, x174, x156); uint64_t x179, uint8_t x180 = addcarryx_u64(0x0, x116, x137); uint64_t x182, uint8_t x183 = addcarryx_u64(x180, x119, x158); uint64_t x185, uint8_t x186 = addcarryx_u64(x183, x122, x161); uint64_t x188, uint8_t x189 = addcarryx_u64(x186, x125, x164); uint64_t x191, uint8_t x192 = addcarryx_u64(x189, x128, x167); uint64_t x194, uint8_t x195 = addcarryx_u64(x192, x131, x170); uint64_t x197, uint8_t x198 = addcarryx_u64(x195, x134, x173); uint64_t x200, uint8_t x201 = addcarryx_u64(x198, x135, x176); uint64_t x203, uint64_t x204 = mulx_u64(x179, 0xffffffffffffffffL); uint64_t x206, uint64_t x207 = mulx_u64(x179, 0xffffffffffffffffL); uint64_t x209, uint64_t x210 = mulx_u64(x179, 0xffffffffffffffffL); uint64_t x212, uint64_t x213 = mulx_u64(x179, 0xfffffffffffeffffL); uint64_t x215, uint64_t x216 = mulx_u64(x179, 0xffffffffffffffffL); uint64_t x218, uint64_t x219 = mulx_u64(x179, 0xffffffffffffffffL); uint64_t x221, uint64_t x222 = mulx_u64(x179, 0xffffffff); uint64_t x224, uint8_t x225 = addcarryx_u64(0x0, x204, x206); uint64_t x227, uint8_t x228 = addcarryx_u64(x225, x207, x209); uint64_t x230, uint8_t x231 = addcarryx_u64(x228, x210, x212); uint64_t x233, uint8_t x234 = addcarryx_u64(x231, x213, x215); uint64_t x236, uint8_t x237 = addcarryx_u64(x234, x216, x218); uint64_t x239, uint8_t x240 = addcarryx_u64(x237, x219, x221); uint64_t x242, uint8_t _ = addcarryx_u64(0x0, x240, x222); uint64_t _, uint8_t x246 = addcarryx_u64(0x0, x179, x203); uint64_t x248, uint8_t x249 = addcarryx_u64(x246, x182, x224); uint64_t x251, uint8_t x252 = addcarryx_u64(x249, x185, x227); uint64_t x254, uint8_t x255 = addcarryx_u64(x252, x188, x230); uint64_t x257, uint8_t x258 = addcarryx_u64(x255, x191, x233); uint64_t x260, uint8_t x261 = addcarryx_u64(x258, x194, x236); uint64_t x263, uint8_t x264 = addcarryx_u64(x261, x197, x239); uint64_t x266, uint8_t x267 = addcarryx_u64(x264, x200, x242); uint8_t x268 = (x267 + x201); uint64_t x270, uint64_t x271 = mulx_u64(x9, x17); uint64_t x273, uint64_t x274 = mulx_u64(x9, x19); uint64_t x276, uint64_t x277 = mulx_u64(x9, x21); uint64_t x279, uint64_t x280 = mulx_u64(x9, x23); uint64_t x282, uint64_t x283 = mulx_u64(x9, x25); uint64_t x285, uint64_t x286 = mulx_u64(x9, x27); uint64_t x288, uint64_t x289 = mulx_u64(x9, x26); uint64_t x291, uint8_t x292 = addcarryx_u64(0x0, x271, x273); uint64_t x294, uint8_t x295 = addcarryx_u64(x292, x274, x276); uint64_t x297, uint8_t x298 = addcarryx_u64(x295, x277, x279); uint64_t x300, uint8_t x301 = addcarryx_u64(x298, x280, x282); uint64_t x303, uint8_t x304 = addcarryx_u64(x301, x283, x285); uint64_t x306, uint8_t x307 = addcarryx_u64(x304, x286, x288); uint64_t x309, uint8_t _ = addcarryx_u64(0x0, x307, x289); uint64_t x312, uint8_t x313 = addcarryx_u64(0x0, x248, x270); uint64_t x315, uint8_t x316 = addcarryx_u64(x313, x251, x291); uint64_t x318, uint8_t x319 = addcarryx_u64(x316, x254, x294); uint64_t x321, uint8_t x322 = addcarryx_u64(x319, x257, x297); uint64_t x324, uint8_t x325 = addcarryx_u64(x322, x260, x300); uint64_t x327, uint8_t x328 = addcarryx_u64(x325, x263, x303); uint64_t x330, uint8_t x331 = addcarryx_u64(x328, x266, x306); uint64_t x333, uint8_t x334 = addcarryx_u64(x331, x268, x309); uint64_t x336, uint64_t x337 = mulx_u64(x312, 0xffffffffffffffffL); uint64_t x339, uint64_t x340 = mulx_u64(x312, 0xffffffffffffffffL); uint64_t x342, uint64_t x343 = mulx_u64(x312, 0xffffffffffffffffL); uint64_t x345, uint64_t x346 = mulx_u64(x312, 0xfffffffffffeffffL); uint64_t x348, uint64_t x349 = mulx_u64(x312, 0xffffffffffffffffL); uint64_t x351, uint64_t x352 = mulx_u64(x312, 0xffffffffffffffffL); uint64_t x354, uint64_t x355 = mulx_u64(x312, 0xffffffff); uint64_t x357, uint8_t x358 = addcarryx_u64(0x0, x337, x339); uint64_t x360, uint8_t x361 = addcarryx_u64(x358, x340, x342); uint64_t x363, uint8_t x364 = addcarryx_u64(x361, x343, x345); uint64_t x366, uint8_t x367 = addcarryx_u64(x364, x346, x348); uint64_t x369, uint8_t x370 = addcarryx_u64(x367, x349, x351); uint64_t x372, uint8_t x373 = addcarryx_u64(x370, x352, x354); uint64_t x375, uint8_t _ = addcarryx_u64(0x0, x373, x355); uint64_t _, uint8_t x379 = addcarryx_u64(0x0, x312, x336); uint64_t x381, uint8_t x382 = addcarryx_u64(x379, x315, x357); uint64_t x384, uint8_t x385 = addcarryx_u64(x382, x318, x360); uint64_t x387, uint8_t x388 = addcarryx_u64(x385, x321, x363); uint64_t x390, uint8_t x391 = addcarryx_u64(x388, x324, x366); uint64_t x393, uint8_t x394 = addcarryx_u64(x391, x327, x369); uint64_t x396, uint8_t x397 = addcarryx_u64(x394, x330, x372); uint64_t x399, uint8_t x400 = addcarryx_u64(x397, x333, x375); uint8_t x401 = (x400 + x334); uint64_t x403, uint64_t x404 = mulx_u64(x11, x17); uint64_t x406, uint64_t x407 = mulx_u64(x11, x19); uint64_t x409, uint64_t x410 = mulx_u64(x11, x21); uint64_t x412, uint64_t x413 = mulx_u64(x11, x23); uint64_t x415, uint64_t x416 = mulx_u64(x11, x25); uint64_t x418, uint64_t x419 = mulx_u64(x11, x27); uint64_t x421, uint64_t x422 = mulx_u64(x11, x26); uint64_t x424, uint8_t x425 = addcarryx_u64(0x0, x404, x406); uint64_t x427, uint8_t x428 = addcarryx_u64(x425, x407, x409); uint64_t x430, uint8_t x431 = addcarryx_u64(x428, x410, x412); uint64_t x433, uint8_t x434 = addcarryx_u64(x431, x413, x415); uint64_t x436, uint8_t x437 = addcarryx_u64(x434, x416, x418); uint64_t x439, uint8_t x440 = addcarryx_u64(x437, x419, x421); uint64_t x442, uint8_t _ = addcarryx_u64(0x0, x440, x422); uint64_t x445, uint8_t x446 = addcarryx_u64(0x0, x381, x403); uint64_t x448, uint8_t x449 = addcarryx_u64(x446, x384, x424); uint64_t x451, uint8_t x452 = addcarryx_u64(x449, x387, x427); uint64_t x454, uint8_t x455 = addcarryx_u64(x452, x390, x430); uint64_t x457, uint8_t x458 = addcarryx_u64(x455, x393, x433); uint64_t x460, uint8_t x461 = addcarryx_u64(x458, x396, x436); uint64_t x463, uint8_t x464 = addcarryx_u64(x461, x399, x439); uint64_t x466, uint8_t x467 = addcarryx_u64(x464, x401, x442); uint64_t x469, uint64_t x470 = mulx_u64(x445, 0xffffffffffffffffL); uint64_t x472, uint64_t x473 = mulx_u64(x445, 0xffffffffffffffffL); uint64_t x475, uint64_t x476 = mulx_u64(x445, 0xffffffffffffffffL); uint64_t x478, uint64_t x479 = mulx_u64(x445, 0xfffffffffffeffffL); uint64_t x481, uint64_t x482 = mulx_u64(x445, 0xffffffffffffffffL); uint64_t x484, uint64_t x485 = mulx_u64(x445, 0xffffffffffffffffL); uint64_t x487, uint64_t x488 = mulx_u64(x445, 0xffffffff); uint64_t x490, uint8_t x491 = addcarryx_u64(0x0, x470, x472); uint64_t x493, uint8_t x494 = addcarryx_u64(x491, x473, x475); uint64_t x496, uint8_t x497 = addcarryx_u64(x494, x476, x478); uint64_t x499, uint8_t x500 = addcarryx_u64(x497, x479, x481); uint64_t x502, uint8_t x503 = addcarryx_u64(x500, x482, x484); uint64_t x505, uint8_t x506 = addcarryx_u64(x503, x485, x487); uint64_t x508, uint8_t _ = addcarryx_u64(0x0, x506, x488); uint64_t _, uint8_t x512 = addcarryx_u64(0x0, x445, x469); uint64_t x514, uint8_t x515 = addcarryx_u64(x512, x448, x490); uint64_t x517, uint8_t x518 = addcarryx_u64(x515, x451, x493); uint64_t x520, uint8_t x521 = addcarryx_u64(x518, x454, x496); uint64_t x523, uint8_t x524 = addcarryx_u64(x521, x457, x499); uint64_t x526, uint8_t x527 = addcarryx_u64(x524, x460, x502); uint64_t x529, uint8_t x530 = addcarryx_u64(x527, x463, x505); uint64_t x532, uint8_t x533 = addcarryx_u64(x530, x466, x508); uint8_t x534 = (x533 + x467); uint64_t x536, uint64_t x537 = mulx_u64(x13, x17); uint64_t x539, uint64_t x540 = mulx_u64(x13, x19); uint64_t x542, uint64_t x543 = mulx_u64(x13, x21); uint64_t x545, uint64_t x546 = mulx_u64(x13, x23); uint64_t x548, uint64_t x549 = mulx_u64(x13, x25); uint64_t x551, uint64_t x552 = mulx_u64(x13, x27); uint64_t x554, uint64_t x555 = mulx_u64(x13, x26); uint64_t x557, uint8_t x558 = addcarryx_u64(0x0, x537, x539); uint64_t x560, uint8_t x561 = addcarryx_u64(x558, x540, x542); uint64_t x563, uint8_t x564 = addcarryx_u64(x561, x543, x545); uint64_t x566, uint8_t x567 = addcarryx_u64(x564, x546, x548); uint64_t x569, uint8_t x570 = addcarryx_u64(x567, x549, x551); uint64_t x572, uint8_t x573 = addcarryx_u64(x570, x552, x554); uint64_t x575, uint8_t _ = addcarryx_u64(0x0, x573, x555); uint64_t x578, uint8_t x579 = addcarryx_u64(0x0, x514, x536); uint64_t x581, uint8_t x582 = addcarryx_u64(x579, x517, x557); uint64_t x584, uint8_t x585 = addcarryx_u64(x582, x520, x560); uint64_t x587, uint8_t x588 = addcarryx_u64(x585, x523, x563); uint64_t x590, uint8_t x591 = addcarryx_u64(x588, x526, x566); uint64_t x593, uint8_t x594 = addcarryx_u64(x591, x529, x569); uint64_t x596, uint8_t x597 = addcarryx_u64(x594, x532, x572); uint64_t x599, uint8_t x600 = addcarryx_u64(x597, x534, x575); uint64_t x602, uint64_t x603 = mulx_u64(x578, 0xffffffffffffffffL); uint64_t x605, uint64_t x606 = mulx_u64(x578, 0xffffffffffffffffL); uint64_t x608, uint64_t x609 = mulx_u64(x578, 0xffffffffffffffffL); uint64_t x611, uint64_t x612 = mulx_u64(x578, 0xfffffffffffeffffL); uint64_t x614, uint64_t x615 = mulx_u64(x578, 0xffffffffffffffffL); uint64_t x617, uint64_t x618 = mulx_u64(x578, 0xffffffffffffffffL); uint64_t x620, uint64_t x621 = mulx_u64(x578, 0xffffffff); uint64_t x623, uint8_t x624 = addcarryx_u64(0x0, x603, x605); uint64_t x626, uint8_t x627 = addcarryx_u64(x624, x606, x608); uint64_t x629, uint8_t x630 = addcarryx_u64(x627, x609, x611); uint64_t x632, uint8_t x633 = addcarryx_u64(x630, x612, x614); uint64_t x635, uint8_t x636 = addcarryx_u64(x633, x615, x617); uint64_t x638, uint8_t x639 = addcarryx_u64(x636, x618, x620); uint64_t x641, uint8_t _ = addcarryx_u64(0x0, x639, x621); uint64_t _, uint8_t x645 = addcarryx_u64(0x0, x578, x602); uint64_t x647, uint8_t x648 = addcarryx_u64(x645, x581, x623); uint64_t x650, uint8_t x651 = addcarryx_u64(x648, x584, x626); uint64_t x653, uint8_t x654 = addcarryx_u64(x651, x587, x629); uint64_t x656, uint8_t x657 = addcarryx_u64(x654, x590, x632); uint64_t x659, uint8_t x660 = addcarryx_u64(x657, x593, x635); uint64_t x662, uint8_t x663 = addcarryx_u64(x660, x596, x638); uint64_t x665, uint8_t x666 = addcarryx_u64(x663, x599, x641); uint8_t x667 = (x666 + x600); uint64_t x669, uint64_t x670 = mulx_u64(x15, x17); uint64_t x672, uint64_t x673 = mulx_u64(x15, x19); uint64_t x675, uint64_t x676 = mulx_u64(x15, x21); uint64_t x678, uint64_t x679 = mulx_u64(x15, x23); uint64_t x681, uint64_t x682 = mulx_u64(x15, x25); uint64_t x684, uint64_t x685 = mulx_u64(x15, x27); uint64_t x687, uint64_t x688 = mulx_u64(x15, x26); uint64_t x690, uint8_t x691 = addcarryx_u64(0x0, x670, x672); uint64_t x693, uint8_t x694 = addcarryx_u64(x691, x673, x675); uint64_t x696, uint8_t x697 = addcarryx_u64(x694, x676, x678); uint64_t x699, uint8_t x700 = addcarryx_u64(x697, x679, x681); uint64_t x702, uint8_t x703 = addcarryx_u64(x700, x682, x684); uint64_t x705, uint8_t x706 = addcarryx_u64(x703, x685, x687); uint64_t x708, uint8_t _ = addcarryx_u64(0x0, x706, x688); uint64_t x711, uint8_t x712 = addcarryx_u64(0x0, x647, x669); uint64_t x714, uint8_t x715 = addcarryx_u64(x712, x650, x690); uint64_t x717, uint8_t x718 = addcarryx_u64(x715, x653, x693); uint64_t x720, uint8_t x721 = addcarryx_u64(x718, x656, x696); uint64_t x723, uint8_t x724 = addcarryx_u64(x721, x659, x699); uint64_t x726, uint8_t x727 = addcarryx_u64(x724, x662, x702); uint64_t x729, uint8_t x730 = addcarryx_u64(x727, x665, x705); uint64_t x732, uint8_t x733 = addcarryx_u64(x730, x667, x708); uint64_t x735, uint64_t x736 = mulx_u64(x711, 0xffffffffffffffffL); uint64_t x738, uint64_t x739 = mulx_u64(x711, 0xffffffffffffffffL); uint64_t x741, uint64_t x742 = mulx_u64(x711, 0xffffffffffffffffL); uint64_t x744, uint64_t x745 = mulx_u64(x711, 0xfffffffffffeffffL); uint64_t x747, uint64_t x748 = mulx_u64(x711, 0xffffffffffffffffL); uint64_t x750, uint64_t x751 = mulx_u64(x711, 0xffffffffffffffffL); uint64_t x753, uint64_t x754 = mulx_u64(x711, 0xffffffff); uint64_t x756, uint8_t x757 = addcarryx_u64(0x0, x736, x738); uint64_t x759, uint8_t x760 = addcarryx_u64(x757, x739, x741); uint64_t x762, uint8_t x763 = addcarryx_u64(x760, x742, x744); uint64_t x765, uint8_t x766 = addcarryx_u64(x763, x745, x747); uint64_t x768, uint8_t x769 = addcarryx_u64(x766, x748, x750); uint64_t x771, uint8_t x772 = addcarryx_u64(x769, x751, x753); uint64_t x774, uint8_t _ = addcarryx_u64(0x0, x772, x754); uint64_t _, uint8_t x778 = addcarryx_u64(0x0, x711, x735); uint64_t x780, uint8_t x781 = addcarryx_u64(x778, x714, x756); uint64_t x783, uint8_t x784 = addcarryx_u64(x781, x717, x759); uint64_t x786, uint8_t x787 = addcarryx_u64(x784, x720, x762); uint64_t x789, uint8_t x790 = addcarryx_u64(x787, x723, x765); uint64_t x792, uint8_t x793 = addcarryx_u64(x790, x726, x768); uint64_t x795, uint8_t x796 = addcarryx_u64(x793, x729, x771); uint64_t x798, uint8_t x799 = addcarryx_u64(x796, x732, x774); uint8_t x800 = (x799 + x733); uint64_t x802, uint64_t x803 = mulx_u64(x14, x17); uint64_t x805, uint64_t x806 = mulx_u64(x14, x19); uint64_t x808, uint64_t x809 = mulx_u64(x14, x21); uint64_t x811, uint64_t x812 = mulx_u64(x14, x23); uint64_t x814, uint64_t x815 = mulx_u64(x14, x25); uint64_t x817, uint64_t x818 = mulx_u64(x14, x27); uint64_t x820, uint64_t x821 = mulx_u64(x14, x26); uint64_t x823, uint8_t x824 = addcarryx_u64(0x0, x803, x805); uint64_t x826, uint8_t x827 = addcarryx_u64(x824, x806, x808); uint64_t x829, uint8_t x830 = addcarryx_u64(x827, x809, x811); uint64_t x832, uint8_t x833 = addcarryx_u64(x830, x812, x814); uint64_t x835, uint8_t x836 = addcarryx_u64(x833, x815, x817); uint64_t x838, uint8_t x839 = addcarryx_u64(x836, x818, x820); uint64_t x841, uint8_t _ = addcarryx_u64(0x0, x839, x821); uint64_t x844, uint8_t x845 = addcarryx_u64(0x0, x780, x802); uint64_t x847, uint8_t x848 = addcarryx_u64(x845, x783, x823); uint64_t x850, uint8_t x851 = addcarryx_u64(x848, x786, x826); uint64_t x853, uint8_t x854 = addcarryx_u64(x851, x789, x829); uint64_t x856, uint8_t x857 = addcarryx_u64(x854, x792, x832); uint64_t x859, uint8_t x860 = addcarryx_u64(x857, x795, x835); uint64_t x862, uint8_t x863 = addcarryx_u64(x860, x798, x838); uint64_t x865, uint8_t x866 = addcarryx_u64(x863, x800, x841); uint64_t x868, uint64_t x869 = mulx_u64(x844, 0xffffffffffffffffL); uint64_t x871, uint64_t x872 = mulx_u64(x844, 0xffffffffffffffffL); uint64_t x874, uint64_t x875 = mulx_u64(x844, 0xffffffffffffffffL); uint64_t x877, uint64_t x878 = mulx_u64(x844, 0xfffffffffffeffffL); uint64_t x880, uint64_t x881 = mulx_u64(x844, 0xffffffffffffffffL); uint64_t x883, uint64_t x884 = mulx_u64(x844, 0xffffffffffffffffL); uint64_t x886, uint64_t x887 = mulx_u64(x844, 0xffffffff); uint64_t x889, uint8_t x890 = addcarryx_u64(0x0, x869, x871); uint64_t x892, uint8_t x893 = addcarryx_u64(x890, x872, x874); uint64_t x895, uint8_t x896 = addcarryx_u64(x893, x875, x877); uint64_t x898, uint8_t x899 = addcarryx_u64(x896, x878, x880); uint64_t x901, uint8_t x902 = addcarryx_u64(x899, x881, x883); uint64_t x904, uint8_t x905 = addcarryx_u64(x902, x884, x886); uint64_t x907, uint8_t _ = addcarryx_u64(0x0, x905, x887); uint64_t _, uint8_t x911 = addcarryx_u64(0x0, x844, x868); uint64_t x913, uint8_t x914 = addcarryx_u64(x911, x847, x889); uint64_t x916, uint8_t x917 = addcarryx_u64(x914, x850, x892); uint64_t x919, uint8_t x920 = addcarryx_u64(x917, x853, x895); uint64_t x922, uint8_t x923 = addcarryx_u64(x920, x856, x898); uint64_t x925, uint8_t x926 = addcarryx_u64(x923, x859, x901); uint64_t x928, uint8_t x929 = addcarryx_u64(x926, x862, x904); uint64_t x931, uint8_t x932 = addcarryx_u64(x929, x865, x907); uint8_t x933 = (x932 + x866); uint64_t x935, uint8_t x936 = subborrow_u64(0x0, x913, 0xffffffffffffffffL); uint64_t x938, uint8_t x939 = subborrow_u64(x936, x916, 0xffffffffffffffffL); uint64_t x941, uint8_t x942 = subborrow_u64(x939, x919, 0xffffffffffffffffL); uint64_t x944, uint8_t x945 = subborrow_u64(x942, x922, 0xfffffffffffeffffL); uint64_t x947, uint8_t x948 = subborrow_u64(x945, x925, 0xffffffffffffffffL); uint64_t x950, uint8_t x951 = subborrow_u64(x948, x928, 0xffffffffffffffffL); uint64_t x953, uint8_t x954 = subborrow_u64(x951, x931, 0xffffffff); uint64_t _, uint8_t x957 = subborrow_u64(x954, x933, 0x0); uint64_t x958 = cmovznz(x957, x953, x931); uint64_t x959 = cmovznz(x957, x950, x928); uint64_t x960 = cmovznz(x957, x947, x925); uint64_t x961 = cmovznz(x957, x944, x922); uint64_t x962 = cmovznz(x957, x941, x919); uint64_t x963 = cmovznz(x957, x938, x916); uint64_t x964 = cmovznz(x957, x935, x913); return (x958, x959, x960, x961, x962, x963, x964)) (x, x0)%core : word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)