λ 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))