λ x x0 x1 x2 x3 : word128 * word128 * word128,
let (a, b) := Interp-η
(λ var : Syntax.base_type → Type,
 λ '(x11, x12, x10, (x17, x18, x16, (x21, x22, x20)), (x27, x28, x26, (x31, x32, x30)))%core,
 uint128_t x33 = x17 + x21;
 uint128_t x34 = x18 + x22;
 uint128_t x35 = x16 + x20;
 uint128_t x36 = 0x3ffffffffffffffffffffeL + x17 - x21;
 uint128_t x37 = 0x3ffffffffffffffffffffeL + x18 - x22;
 uint128_t x38 = 0x3ffffffffffffffffffff6L + x16 - x20;
 uint256_t x39 = (uint256_t) x35 * x33 + ((uint256_t) x34 * x34 + (uint256_t) x33 * x35);
 uint256_t x40 = (uint256_t) x35 * x34 + (uint256_t) x34 * x35 + 0x5 * ((uint256_t) x33 * x33);
 uint256_t x41 = (uint256_t) x35 * x35 + 0x5 * ((uint256_t) x34 * x33 + (uint256_t) x33 * x34);
 uint128_t x42 = (uint128_t) (x41 >> 0x55);
 uint128_t x43 = (uint128_t) x41 & 0x1fffffffffffffffffffffL;
 uint256_t x44 = x42 + x40;
 uint128_t x45 = (uint128_t) (x44 >> 0x55);
 uint128_t x46 = (uint128_t) x44 & 0x1fffffffffffffffffffffL;
 uint256_t x47 = x45 + x39;
 uint128_t x48 = (uint128_t) (x47 >> 0x55);
 uint128_t x49 = (uint128_t) x47 & 0x1fffffffffffffffffffffL;
 uint128_t x50 = x43 + 0x5 * x48;
 uint128_t x51 = x50 >> 0x55;
 uint128_t x52 = x50 & 0x1fffffffffffffffffffffL;
 uint128_t x53 = x51 + x46;
 uint128_t x54 = x53 >> 0x55;
 uint128_t x55 = x53 & 0x1fffffffffffffffffffffL;
 uint128_t x56 = x54 + x49;
 uint256_t x57 = (uint256_t) x38 * x36 + ((uint256_t) x37 * x37 + (uint256_t) x36 * x38);
 uint256_t x58 = (uint256_t) x38 * x37 + (uint256_t) x37 * x38 + 0x5 * ((uint256_t) x36 * x36);
 uint256_t x59 = (uint256_t) x38 * x38 + 0x5 * ((uint256_t) x37 * x36 + (uint256_t) x36 * x37);
 uint128_t x60 = (uint128_t) (x59 >> 0x55);
 uint128_t x61 = (uint128_t) x59 & 0x1fffffffffffffffffffffL;
 uint256_t x62 = x60 + x58;
 uint128_t x63 = (uint128_t) (x62 >> 0x55);
 uint128_t x64 = (uint128_t) x62 & 0x1fffffffffffffffffffffL;
 uint256_t x65 = x63 + x57;
 uint128_t x66 = (uint128_t) (x65 >> 0x55);
 uint128_t x67 = (uint128_t) x65 & 0x1fffffffffffffffffffffL;
 uint128_t x68 = x61 + 0x5 * x66;
 uint128_t x69 = x68 >> 0x55;
 uint128_t x70 = x68 & 0x1fffffffffffffffffffffL;
 uint128_t x71 = x69 + x64;
 uint128_t x72 = x71 >> 0x55;
 uint128_t x73 = x71 & 0x1fffffffffffffffffffffL;
 uint128_t x74 = x72 + x67;
 uint256_t x75 = (uint256_t) x52 * x74 + ((uint256_t) x55 * x73 + (uint256_t) x56 * x70);
 uint256_t x76 = (uint256_t) x52 * x73 + (uint256_t) x55 * x70 + 0x5 * ((uint256_t) x56 * x74);
 uint256_t x77 = (uint256_t) x52 * x70 + 0x5 * ((uint256_t) x55 * x74 + (uint256_t) x56 * x73);
 uint128_t x78 = (uint128_t) (x77 >> 0x55);
 uint128_t x79 = (uint128_t) x77 & 0x1fffffffffffffffffffffL;
 uint256_t x80 = x78 + x76;
 uint128_t x81 = (uint128_t) (x80 >> 0x55);
 uint128_t x82 = (uint128_t) x80 & 0x1fffffffffffffffffffffL;
 uint256_t x83 = x81 + x75;
 uint128_t x84 = (uint128_t) (x83 >> 0x55);
 uint128_t x85 = (uint128_t) x83 & 0x1fffffffffffffffffffffL;
 uint128_t x86 = x79 + 0x5 * x84;
 uint128_t x87 = x86 >> 0x55;
 uint128_t x88 = x86 & 0x1fffffffffffffffffffffL;
 uint128_t x89 = x87 + x82;
 uint128_t x90 = x89 >> 0x55;
 uint128_t x91 = x89 & 0x1fffffffffffffffffffffL;
 uint128_t x92 = x90 + x85;
 uint128_t x93 = 0x3ffffffffffffffffffffeL + x56 - x74;
 uint128_t x94 = 0x3ffffffffffffffffffffeL + x55 - x73;
 uint128_t x95 = 0x3ffffffffffffffffffff6L + x52 - x70;
 uint128_t x96 = 0x1db41 * x93;
 uint128_t x97 = 0x1db41 * x94;
 uint128_t x98 = 0x1db41 * x95;
 uint128_t x99 = x98 >> 0x55;
 uint128_t x100 = x98 & 0x1fffffffffffffffffffffL;
 uint128_t x101 = x99 + x97;
 uint128_t x102 = x101 >> 0x55;
 uint128_t x103 = x101 & 0x1fffffffffffffffffffffL;
 uint128_t x104 = x102 + x96;
 uint128_t x105 = x104 >> 0x55;
 uint128_t x106 = x104 & 0x1fffffffffffffffffffffL;
 uint128_t x107 = x100 + 0x5 * x105;
 uint128_t x108 = x107 >> 0x55;
 uint128_t x109 = x107 & 0x1fffffffffffffffffffffL;
 uint128_t x110 = x108 + x103;
 uint128_t x111 = x110 >> 0x55;
 uint128_t x112 = x110 & 0x1fffffffffffffffffffffL;
 uint128_t x113 = x111 + x106;
 uint128_t x114 = x56 + x113;
 uint128_t x115 = x55 + x112;
 uint128_t x116 = x52 + x109;
 uint256_t x117 = (uint256_t) x95 * x114 + ((uint256_t) x94 * x115 + (uint256_t) x93 * x116);
 uint256_t x118 = (uint256_t) x95 * x115 + (uint256_t) x94 * x116 + 0x5 * ((uint256_t) x93 * x114);
 uint256_t x119 = (uint256_t) x95 * x116 + 0x5 * ((uint256_t) x94 * x114 + (uint256_t) x93 * x115);
 uint128_t x120 = (uint128_t) (x119 >> 0x55);
 uint128_t x121 = (uint128_t) x119 & 0x1fffffffffffffffffffffL;
 uint256_t x122 = x120 + x118;
 uint128_t x123 = (uint128_t) (x122 >> 0x55);
 uint128_t x124 = (uint128_t) x122 & 0x1fffffffffffffffffffffL;
 uint256_t x125 = x123 + x117;
 uint128_t x126 = (uint128_t) (x125 >> 0x55);
 uint128_t x127 = (uint128_t) x125 & 0x1fffffffffffffffffffffL;
 uint128_t x128 = x121 + 0x5 * x126;
 uint128_t x129 = x128 >> 0x55;
 uint128_t x130 = x128 & 0x1fffffffffffffffffffffL;
 uint128_t x131 = x129 + x124;
 uint128_t x132 = x131 >> 0x55;
 uint128_t x133 = x131 & 0x1fffffffffffffffffffffL;
 uint128_t x134 = x132 + x127;
 uint128_t x135 = x27 + x31;
 uint128_t x136 = x28 + x32;
 uint128_t x137 = x26 + x30;
 uint128_t x138 = 0x3ffffffffffffffffffffeL + x27 - x31;
 uint128_t x139 = 0x3ffffffffffffffffffffeL + x28 - x32;
 uint128_t x140 = 0x3ffffffffffffffffffff6L + x26 - x30;
 uint256_t x141 = (uint256_t) x137 * x36 + ((uint256_t) x136 * x37 + (uint256_t) x135 * x38);
 uint256_t x142 = (uint256_t) x137 * x37 + (uint256_t) x136 * x38 + 0x5 * ((uint256_t) x135 * x36);
 uint256_t x143 = (uint256_t) x137 * x38 + 0x5 * ((uint256_t) x136 * x36 + (uint256_t) x135 * x37);
 uint128_t x144 = (uint128_t) (x143 >> 0x55);
 uint128_t x145 = (uint128_t) x143 & 0x1fffffffffffffffffffffL;
 uint256_t x146 = x144 + x142;
 uint128_t x147 = (uint128_t) (x146 >> 0x55);
 uint128_t x148 = (uint128_t) x146 & 0x1fffffffffffffffffffffL;
 uint256_t x149 = x147 + x141;
 uint128_t x150 = (uint128_t) (x149 >> 0x55);
 uint128_t x151 = (uint128_t) x149 & 0x1fffffffffffffffffffffL;
 uint128_t x152 = x145 + 0x5 * x150;
 uint128_t x153 = x152 >> 0x55;
 uint128_t x154 = x152 & 0x1fffffffffffffffffffffL;
 uint128_t x155 = x153 + x148;
 uint128_t x156 = x155 >> 0x55;
 uint128_t x157 = x155 & 0x1fffffffffffffffffffffL;
 uint128_t x158 = x156 + x151;
 uint256_t x159 = (uint256_t) x140 * x33 + ((uint256_t) x139 * x34 + (uint256_t) x138 * x35);
 uint256_t x160 = (uint256_t) x140 * x34 + (uint256_t) x139 * x35 + 0x5 * ((uint256_t) x138 * x33);
 uint256_t x161 = (uint256_t) x140 * x35 + 0x5 * ((uint256_t) x139 * x33 + (uint256_t) x138 * x34);
 uint128_t x162 = (uint128_t) (x161 >> 0x55);
 uint128_t x163 = (uint128_t) x161 & 0x1fffffffffffffffffffffL;
 uint256_t x164 = x162 + x160;
 uint128_t x165 = (uint128_t) (x164 >> 0x55);
 uint128_t x166 = (uint128_t) x164 & 0x1fffffffffffffffffffffL;
 uint256_t x167 = x165 + x159;
 uint128_t x168 = (uint128_t) (x167 >> 0x55);
 uint128_t x169 = (uint128_t) x167 & 0x1fffffffffffffffffffffL;
 uint128_t x170 = x163 + 0x5 * x168;
 uint128_t x171 = x170 >> 0x55;
 uint128_t x172 = x170 & 0x1fffffffffffffffffffffL;
 uint128_t x173 = x171 + x166;
 uint128_t x174 = x173 >> 0x55;
 uint128_t x175 = x173 & 0x1fffffffffffffffffffffL;
 uint128_t x176 = x174 + x169;
 uint128_t x177 = x176 + x158;
 uint128_t x178 = x175 + x157;
 uint128_t x179 = x172 + x154;
 uint128_t x180 = x176 + x158;
 uint128_t x181 = x175 + x157;
 uint128_t x182 = x172 + x154;
 uint256_t x183 = (uint256_t) x179 * x180 + ((uint256_t) x178 * x181 + (uint256_t) x177 * x182);
 uint256_t x184 = (uint256_t) x179 * x181 + (uint256_t) x178 * x182 + 0x5 * ((uint256_t) x177 * x180);
 uint256_t x185 = (uint256_t) x179 * x182 + 0x5 * ((uint256_t) x178 * x180 + (uint256_t) x177 * x181);
 uint128_t x186 = (uint128_t) (x185 >> 0x55);
 uint128_t x187 = (uint128_t) x185 & 0x1fffffffffffffffffffffL;
 uint256_t x188 = x186 + x184;
 uint128_t x189 = (uint128_t) (x188 >> 0x55);
 uint128_t x190 = (uint128_t) x188 & 0x1fffffffffffffffffffffL;
 uint256_t x191 = x189 + x183;
 uint128_t x192 = (uint128_t) (x191 >> 0x55);
 uint128_t x193 = (uint128_t) x191 & 0x1fffffffffffffffffffffL;
 uint128_t x194 = x187 + 0x5 * x192;
 uint128_t x195 = x194 >> 0x55;
 uint128_t x196 = x194 & 0x1fffffffffffffffffffffL;
 uint128_t x197 = x195 + x190;
 uint128_t x198 = x197 >> 0x55;
 uint128_t x199 = x197 & 0x1fffffffffffffffffffffL;
 uint128_t x200 = x198 + x193;
 uint128_t x201 = 0x3ffffffffffffffffffffeL + x176 - x158;
 uint128_t x202 = 0x3ffffffffffffffffffffeL + x175 - x157;
 uint128_t x203 = 0x3ffffffffffffffffffff6L + x172 - x154;
 uint128_t x204 = 0x3ffffffffffffffffffffeL + x176 - x158;
 uint128_t x205 = 0x3ffffffffffffffffffffeL + x175 - x157;
 uint128_t x206 = 0x3ffffffffffffffffffff6L + x172 - x154;
 uint256_t x207 = (uint256_t) x203 * x204 + ((uint256_t) x202 * x205 + (uint256_t) x201 * x206);
 uint256_t x208 = (uint256_t) x203 * x205 + (uint256_t) x202 * x206 + 0x5 * ((uint256_t) x201 * x204);
 uint256_t x209 = (uint256_t) x203 * x206 + 0x5 * ((uint256_t) x202 * x204 + (uint256_t) x201 * x205);
 uint128_t x210 = (uint128_t) (x209 >> 0x55);
 uint128_t x211 = (uint128_t) x209 & 0x1fffffffffffffffffffffL;
 uint256_t x212 = x210 + x208;
 uint128_t x213 = (uint128_t) (x212 >> 0x55);
 uint128_t x214 = (uint128_t) x212 & 0x1fffffffffffffffffffffL;
 uint256_t x215 = x213 + x207;
 uint128_t x216 = (uint128_t) (x215 >> 0x55);
 uint128_t x217 = (uint128_t) x215 & 0x1fffffffffffffffffffffL;
 uint128_t x218 = x211 + 0x5 * x216;
 uint128_t x219 = x218 >> 0x55;
 uint128_t x220 = x218 & 0x1fffffffffffffffffffffL;
 uint128_t x221 = x219 + x214;
 uint128_t x222 = x221 >> 0x55;
 uint128_t x223 = x221 & 0x1fffffffffffffffffffffL;
 uint128_t x224 = x222 + x217;
 uint256_t x225 = (uint256_t) x10 * x224 + ((uint256_t) x12 * x223 + (uint256_t) x11 * x220);
 uint256_t x226 = (uint256_t) x10 * x223 + (uint256_t) x12 * x220 + 0x5 * ((uint256_t) x11 * x224);
 uint256_t x227 = (uint256_t) x10 * x220 + 0x5 * ((uint256_t) x12 * x224 + (uint256_t) x11 * x223);
 uint128_t x228 = (uint128_t) (x227 >> 0x55);
 uint128_t x229 = (uint128_t) x227 & 0x1fffffffffffffffffffffL;
 uint256_t x230 = x228 + x226;
 uint128_t x231 = (uint128_t) (x230 >> 0x55);
 uint128_t x232 = (uint128_t) x230 & 0x1fffffffffffffffffffffL;
 uint256_t x233 = x231 + x225;
 uint128_t x234 = (uint128_t) (x233 >> 0x55);
 uint128_t x235 = (uint128_t) x233 & 0x1fffffffffffffffffffffL;
 uint128_t x236 = x229 + 0x5 * x234;
 uint128_t x237 = x236 >> 0x55;
 uint128_t x238 = x236 & 0x1fffffffffffffffffffffL;
 uint128_t x239 = x237 + x232;
 uint128_t x240 = x239 >> 0x55;
 uint128_t x241 = x239 & 0x1fffffffffffffffffffffL;
 uint128_t x242 = x240 + x235;
 return (Return x92, Return x91, Return x88, (Return x134, Return x133, Return x130), (Return x200, Return x199, Return x196, (Return x242, Return x241, Return x238))))
(x, (x0, x1), (x2, x3))%core in
(let (a0, b0) := a in
(a0, b0), let (a0, b0) := b in
(a0, b0))%core
     : word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 * (word128 * word128 * word128) * (word128 * word128 * word128 * (word128 * word128 * word128))