From 3dcce26ee10c8b8f2fa0d954bfaed46818ba2dbc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 7 Apr 2017 16:35:38 -0400 Subject: Add Ladderstep130 display log --- .../IntegrationTestLadderstep130Display.log | 1565 ++++++++++++++++++++ 1 file changed, 1565 insertions(+) create mode 100644 src/Specific/IntegrationTestLadderstep130Display.log (limited to 'src/Specific/IntegrationTestLadderstep130Display.log') diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log new file mode 100644 index 000000000..3f81634e7 --- /dev/null +++ b/src/Specific/IntegrationTestLadderstep130Display.log @@ -0,0 +1,1565 @@ +fun x x0 x1 x2 x3 x4 : word128 * word128 * word128 => +(let (x5, _) := + let (x5, _) := + Eta.InterpEta + (fun var : Syntax.base_type -> Type => + λ + '(x14, x15, x13, (x18, x19, x17), (x24, x25, x23, (x28, x29, x27)), + (x34, x35, x33, (x38, x39, x37)))%core, + uint128_t x40 = x24 + x28; + uint128_t x41 = x25 + x29; + uint128_t x42 = x23 + x27; + uint128_t x43 = Const 77371252455336267181195262 + x24; + uint128_t x44 = x43 - x28; + uint128_t x45 = Const 77371252455336267181195262 + x25; + uint128_t x46 = x45 - x29; + uint128_t x47 = Const 77371252455336267181195254 + x23; + uint128_t x48 = x47 - x27; + Tbase (Syntax.TWord 8) x49 = x42 * x40; + Tbase (Syntax.TWord 8) x50 = x41 * x41; + Tbase (Syntax.TWord 8) x51 = x40 * x42; + Tbase (Syntax.TWord 8) x52 = x50 + x51; + Tbase (Syntax.TWord 8) x53 = x49 + x52; + Tbase (Syntax.TWord 8) x54 = x42 * x41; + Tbase (Syntax.TWord 8) x55 = x41 * x42; + Tbase (Syntax.TWord 8) x56 = x54 + x55; + Tbase (Syntax.TWord 8) x57 = x40 * x40; + Tbase (Syntax.TWord 8) x58 = Const 5 * x57; + Tbase (Syntax.TWord 8) x59 = x56 + x58; + Tbase (Syntax.TWord 8) x60 = x42 * x42; + Tbase (Syntax.TWord 8) x61 = x41 * x40; + Tbase (Syntax.TWord 8) x62 = x40 * x41; + Tbase (Syntax.TWord 8) x63 = x61 + x62; + Tbase (Syntax.TWord 8) x64 = Const 5 * x63; + Tbase (Syntax.TWord 8) x65 = x60 + x64; + uint128_t x66 = (uint128_t) (x65 >> Const 85); + Tbase (Syntax.TWord 8) x67 = x66 + x59; + uint128_t x68 = (uint128_t) (x67 >> Const 85); + Tbase (Syntax.TWord 8) x69 = x68 + x53; + uint128_t x70 = (uint128_t) x65 & Const 38685626227668133590597631; + uint128_t x71 = (uint128_t) (x69 >> Const 85); + uint128_t x72 = (uint128_t) Const 5 * x71; + uint128_t x73 = x70 + x72; + uint8_t x74 = (uint8_t) (x73 >> Const 85); + uint128_t x75 = (uint128_t) x67 & Const 38685626227668133590597631; + uint128_t x76 = (uint128_t) x74 + x75; + bool x77 = (bool) (x76 >> Const 85); + uint128_t x78 = (uint128_t) x69 & Const 38685626227668133590597631; + uint128_t x79 = (uint128_t) x77 + x78; + uint128_t x80 = x76 & Const 38685626227668133590597631; + uint128_t x81 = x73 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x82 = x48 * x44; + Tbase (Syntax.TWord 8) x83 = x46 * x46; + Tbase (Syntax.TWord 8) x84 = x44 * x48; + Tbase (Syntax.TWord 8) x85 = x83 + x84; + Tbase (Syntax.TWord 8) x86 = x82 + x85; + Tbase (Syntax.TWord 8) x87 = x48 * x46; + Tbase (Syntax.TWord 8) x88 = x46 * x48; + Tbase (Syntax.TWord 8) x89 = x87 + x88; + Tbase (Syntax.TWord 8) x90 = x44 * x44; + Tbase (Syntax.TWord 8) x91 = Const 5 * x90; + Tbase (Syntax.TWord 8) x92 = x89 + x91; + Tbase (Syntax.TWord 8) x93 = x48 * x48; + Tbase (Syntax.TWord 8) x94 = x46 * x44; + Tbase (Syntax.TWord 8) x95 = x44 * x46; + Tbase (Syntax.TWord 8) x96 = x94 + x95; + Tbase (Syntax.TWord 8) x97 = Const 5 * x96; + Tbase (Syntax.TWord 8) x98 = x93 + x97; + uint128_t x99 = (uint128_t) (x98 >> Const 85); + Tbase (Syntax.TWord 8) x100 = x99 + x92; + uint128_t x101 = (uint128_t) (x100 >> Const 85); + Tbase (Syntax.TWord 8) x102 = x101 + x86; + uint128_t x103 = (uint128_t) x98 & Const 38685626227668133590597631; + uint128_t x104 = (uint128_t) (x102 >> Const 85); + uint128_t x105 = (uint128_t) Const 5 * x104; + uint128_t x106 = x103 + x105; + uint8_t x107 = (uint8_t) (x106 >> Const 85); + uint128_t x108 = (uint128_t) x100 & Const 38685626227668133590597631; + uint128_t x109 = (uint128_t) x107 + x108; + bool x110 = (bool) (x109 >> Const 85); + uint128_t x111 = (uint128_t) x102 & Const 38685626227668133590597631; + uint128_t x112 = (uint128_t) x110 + x111; + uint128_t x113 = x109 & Const 38685626227668133590597631; + uint128_t x114 = x106 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x115 = x81 * x112; + Tbase (Syntax.TWord 8) x116 = x80 * x113; + Tbase (Syntax.TWord 8) x117 = x79 * x114; + Tbase (Syntax.TWord 8) x118 = x116 + x117; + Tbase (Syntax.TWord 8) x119 = x115 + x118; + Tbase (Syntax.TWord 8) x120 = x81 * x113; + Tbase (Syntax.TWord 8) x121 = x80 * x114; + Tbase (Syntax.TWord 8) x122 = x120 + x121; + Tbase (Syntax.TWord 8) x123 = x79 * x112; + Tbase (Syntax.TWord 8) x124 = Const 5 * x123; + Tbase (Syntax.TWord 8) x125 = x122 + x124; + Tbase (Syntax.TWord 8) x126 = x81 * x114; + Tbase (Syntax.TWord 8) x127 = x80 * x112; + Tbase (Syntax.TWord 8) x128 = x79 * x113; + Tbase (Syntax.TWord 8) x129 = x127 + x128; + Tbase (Syntax.TWord 8) x130 = Const 5 * x129; + Tbase (Syntax.TWord 8) x131 = x126 + x130; + uint128_t x132 = (uint128_t) (x131 >> Const 85); + Tbase (Syntax.TWord 8) x133 = x132 + x125; + uint128_t x134 = (uint128_t) (x133 >> Const 85); + Tbase (Syntax.TWord 8) x135 = x134 + x119; + uint128_t x136 = (uint128_t) x131 & Const 38685626227668133590597631; + uint128_t x137 = (uint128_t) (x135 >> Const 85); + uint128_t x138 = (uint128_t) Const 5 * x137; + uint128_t x139 = x136 + x138; + uint8_t x140 = (uint8_t) (x139 >> Const 85); + uint128_t x141 = (uint128_t) x133 & Const 38685626227668133590597631; + uint128_t x142 = (uint128_t) x140 + x141; + bool x143 = (bool) (x142 >> Const 85); + uint128_t x144 = (uint128_t) x135 & Const 38685626227668133590597631; + uint128_t x145 = (uint128_t) x143 + x144; + uint128_t x146 = x142 & Const 38685626227668133590597631; + uint128_t x147 = x139 & Const 38685626227668133590597631; + uint128_t x148 = Const 77371252455336267181195262 + x79; + uint128_t x149 = x148 - x112; + uint128_t x150 = Const 77371252455336267181195262 + x80; + uint128_t x151 = x150 - x113; + uint128_t x152 = Const 77371252455336267181195254 + x81; + uint128_t x153 = x152 - x114; + Tbase (Syntax.TWord 8) x154 = x13 * x149; + Tbase (Syntax.TWord 8) x155 = x15 * x151; + Tbase (Syntax.TWord 8) x156 = x14 * x153; + Tbase (Syntax.TWord 8) x157 = x155 + x156; + Tbase (Syntax.TWord 8) x158 = x154 + x157; + Tbase (Syntax.TWord 8) x159 = x13 * x151; + Tbase (Syntax.TWord 8) x160 = x15 * x153; + Tbase (Syntax.TWord 8) x161 = x159 + x160; + Tbase (Syntax.TWord 8) x162 = x14 * x149; + Tbase (Syntax.TWord 8) x163 = Const 5 * x162; + Tbase (Syntax.TWord 8) x164 = x161 + x163; + Tbase (Syntax.TWord 8) x165 = x13 * x153; + Tbase (Syntax.TWord 8) x166 = x15 * x149; + Tbase (Syntax.TWord 8) x167 = x14 * x151; + Tbase (Syntax.TWord 8) x168 = x166 + x167; + Tbase (Syntax.TWord 8) x169 = Const 5 * x168; + Tbase (Syntax.TWord 8) x170 = x165 + x169; + uint128_t x171 = (uint128_t) (x170 >> Const 85); + Tbase (Syntax.TWord 8) x172 = x171 + x164; + uint128_t x173 = (uint128_t) (x172 >> Const 85); + Tbase (Syntax.TWord 8) x174 = x173 + x158; + uint128_t x175 = (uint128_t) x170 & Const 38685626227668133590597631; + uint128_t x176 = (uint128_t) (x174 >> Const 85); + uint128_t x177 = (uint128_t) Const 5 * x176; + uint128_t x178 = x175 + x177; + uint8_t x179 = (uint8_t) (x178 >> Const 85); + uint128_t x180 = (uint128_t) x172 & Const 38685626227668133590597631; + uint128_t x181 = (uint128_t) x179 + x180; + bool x182 = (bool) (x181 >> Const 85); + uint128_t x183 = (uint128_t) x174 & Const 38685626227668133590597631; + uint128_t x184 = (uint128_t) x182 + x183; + uint128_t x185 = x181 & Const 38685626227668133590597631; + uint128_t x186 = x178 & Const 38685626227668133590597631; + uint128_t x187 = x79 + x184; + uint128_t x188 = x80 + x185; + uint128_t x189 = x81 + x186; + Tbase (Syntax.TWord 8) x190 = x153 * x187; + Tbase (Syntax.TWord 8) x191 = x151 * x188; + Tbase (Syntax.TWord 8) x192 = x149 * x189; + Tbase (Syntax.TWord 8) x193 = x191 + x192; + Tbase (Syntax.TWord 8) x194 = x190 + x193; + Tbase (Syntax.TWord 8) x195 = x153 * x188; + Tbase (Syntax.TWord 8) x196 = x151 * x189; + Tbase (Syntax.TWord 8) x197 = x195 + x196; + Tbase (Syntax.TWord 8) x198 = x149 * x187; + Tbase (Syntax.TWord 8) x199 = Const 5 * x198; + Tbase (Syntax.TWord 8) x200 = x197 + x199; + Tbase (Syntax.TWord 8) x201 = x153 * x189; + Tbase (Syntax.TWord 8) x202 = x151 * x187; + Tbase (Syntax.TWord 8) x203 = x149 * x188; + Tbase (Syntax.TWord 8) x204 = x202 + x203; + Tbase (Syntax.TWord 8) x205 = Const 5 * x204; + Tbase (Syntax.TWord 8) x206 = x201 + x205; + uint128_t x207 = (uint128_t) (x206 >> Const 85); + Tbase (Syntax.TWord 8) x208 = x207 + x200; + uint128_t x209 = (uint128_t) (x208 >> Const 85); + Tbase (Syntax.TWord 8) x210 = x209 + x194; + uint128_t x211 = (uint128_t) x206 & Const 38685626227668133590597631; + uint128_t x212 = (uint128_t) (x210 >> Const 85); + uint128_t x213 = (uint128_t) Const 5 * x212; + uint128_t x214 = x211 + x213; + uint8_t x215 = (uint8_t) (x214 >> Const 85); + uint128_t x216 = (uint128_t) x208 & Const 38685626227668133590597631; + uint128_t x217 = (uint128_t) x215 + x216; + bool x218 = (bool) (x217 >> Const 85); + uint128_t x219 = (uint128_t) x210 & Const 38685626227668133590597631; + uint128_t x220 = (uint128_t) x218 + x219; + uint128_t x221 = x217 & Const 38685626227668133590597631; + uint128_t x222 = x214 & Const 38685626227668133590597631; + uint128_t x223 = x34 + x38; + uint128_t x224 = x35 + x39; + uint128_t x225 = x33 + x37; + uint128_t x226 = Const 77371252455336267181195262 + x34; + uint128_t x227 = x226 - x38; + uint128_t x228 = Const 77371252455336267181195262 + x35; + uint128_t x229 = x228 - x39; + uint128_t x230 = Const 77371252455336267181195254 + x33; + uint128_t x231 = x230 - x37; + Tbase (Syntax.TWord 8) x232 = x225 * x44; + Tbase (Syntax.TWord 8) x233 = x224 * x46; + Tbase (Syntax.TWord 8) x234 = x223 * x48; + Tbase (Syntax.TWord 8) x235 = x233 + x234; + Tbase (Syntax.TWord 8) x236 = x232 + x235; + Tbase (Syntax.TWord 8) x237 = x225 * x46; + Tbase (Syntax.TWord 8) x238 = x224 * x48; + Tbase (Syntax.TWord 8) x239 = x237 + x238; + Tbase (Syntax.TWord 8) x240 = x223 * x44; + Tbase (Syntax.TWord 8) x241 = Const 5 * x240; + Tbase (Syntax.TWord 8) x242 = x239 + x241; + Tbase (Syntax.TWord 8) x243 = x225 * x48; + Tbase (Syntax.TWord 8) x244 = x224 * x44; + Tbase (Syntax.TWord 8) x245 = x223 * x46; + Tbase (Syntax.TWord 8) x246 = x244 + x245; + Tbase (Syntax.TWord 8) x247 = Const 5 * x246; + Tbase (Syntax.TWord 8) x248 = x243 + x247; + uint128_t x249 = (uint128_t) (x248 >> Const 85); + Tbase (Syntax.TWord 8) x250 = x249 + x242; + uint128_t x251 = (uint128_t) (x250 >> Const 85); + Tbase (Syntax.TWord 8) x252 = x251 + x236; + uint128_t x253 = (uint128_t) x248 & Const 38685626227668133590597631; + uint128_t x254 = (uint128_t) (x252 >> Const 85); + uint128_t x255 = (uint128_t) Const 5 * x254; + uint128_t x256 = x253 + x255; + uint8_t x257 = (uint8_t) (x256 >> Const 85); + uint128_t x258 = (uint128_t) x250 & Const 38685626227668133590597631; + uint128_t x259 = (uint128_t) x257 + x258; + bool x260 = (bool) (x259 >> Const 85); + uint128_t x261 = (uint128_t) x252 & Const 38685626227668133590597631; + uint128_t x262 = (uint128_t) x260 + x261; + uint128_t x263 = x259 & Const 38685626227668133590597631; + uint128_t x264 = x256 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x265 = x231 * x40; + Tbase (Syntax.TWord 8) x266 = x229 * x41; + Tbase (Syntax.TWord 8) x267 = x227 * x42; + Tbase (Syntax.TWord 8) x268 = x266 + x267; + Tbase (Syntax.TWord 8) x269 = x265 + x268; + Tbase (Syntax.TWord 8) x270 = x231 * x41; + Tbase (Syntax.TWord 8) x271 = x229 * x42; + Tbase (Syntax.TWord 8) x272 = x270 + x271; + Tbase (Syntax.TWord 8) x273 = x227 * x40; + Tbase (Syntax.TWord 8) x274 = Const 5 * x273; + Tbase (Syntax.TWord 8) x275 = x272 + x274; + Tbase (Syntax.TWord 8) x276 = x231 * x42; + Tbase (Syntax.TWord 8) x277 = x229 * x40; + Tbase (Syntax.TWord 8) x278 = x227 * x41; + Tbase (Syntax.TWord 8) x279 = x277 + x278; + Tbase (Syntax.TWord 8) x280 = Const 5 * x279; + Tbase (Syntax.TWord 8) x281 = x276 + x280; + uint128_t x282 = (uint128_t) (x281 >> Const 85); + Tbase (Syntax.TWord 8) x283 = x282 + x275; + uint128_t x284 = (uint128_t) (x283 >> Const 85); + Tbase (Syntax.TWord 8) x285 = x284 + x269; + uint128_t x286 = (uint128_t) x281 & Const 38685626227668133590597631; + uint128_t x287 = (uint128_t) (x285 >> Const 85); + uint128_t x288 = (uint128_t) Const 5 * x287; + uint128_t x289 = x286 + x288; + uint8_t x290 = (uint8_t) (x289 >> Const 85); + uint128_t x291 = (uint128_t) x283 & Const 38685626227668133590597631; + uint128_t x292 = (uint128_t) x290 + x291; + bool x293 = (bool) (x292 >> Const 85); + uint128_t x294 = (uint128_t) x285 & Const 38685626227668133590597631; + uint128_t x295 = (uint128_t) x293 + x294; + uint128_t x296 = x292 & Const 38685626227668133590597631; + uint128_t x297 = x289 & Const 38685626227668133590597631; + uint128_t x298 = x295 + x262; + uint128_t x299 = x296 + x263; + uint128_t x300 = x297 + x264; + uint128_t x301 = x295 + x262; + uint128_t x302 = x296 + x263; + uint128_t x303 = x297 + x264; + Tbase (Syntax.TWord 8) x304 = x300 * x301; + Tbase (Syntax.TWord 8) x305 = x299 * x302; + Tbase (Syntax.TWord 8) x306 = x298 * x303; + Tbase (Syntax.TWord 8) x307 = x305 + x306; + Tbase (Syntax.TWord 8) x308 = x304 + x307; + Tbase (Syntax.TWord 8) x309 = x300 * x302; + Tbase (Syntax.TWord 8) x310 = x299 * x303; + Tbase (Syntax.TWord 8) x311 = x309 + x310; + Tbase (Syntax.TWord 8) x312 = x298 * x301; + Tbase (Syntax.TWord 8) x313 = Const 5 * x312; + Tbase (Syntax.TWord 8) x314 = x311 + x313; + Tbase (Syntax.TWord 8) x315 = x300 * x303; + Tbase (Syntax.TWord 8) x316 = x299 * x301; + Tbase (Syntax.TWord 8) x317 = x298 * x302; + Tbase (Syntax.TWord 8) x318 = x316 + x317; + Tbase (Syntax.TWord 8) x319 = Const 5 * x318; + Tbase (Syntax.TWord 8) x320 = x315 + x319; + uint128_t x321 = (uint128_t) (x320 >> Const 85); + Tbase (Syntax.TWord 8) x322 = x321 + x314; + uint128_t x323 = (uint128_t) (x322 >> Const 85); + Tbase (Syntax.TWord 8) x324 = x323 + x308; + uint128_t x325 = (uint128_t) x320 & Const 38685626227668133590597631; + uint128_t x326 = (uint128_t) (x324 >> Const 85); + uint128_t x327 = (uint128_t) Const 5 * x326; + uint128_t x328 = x325 + x327; + uint8_t x329 = (uint8_t) (x328 >> Const 85); + uint128_t x330 = (uint128_t) x322 & Const 38685626227668133590597631; + uint128_t x331 = (uint128_t) x329 + x330; + bool x332 = (bool) (x331 >> Const 85); + uint128_t x333 = (uint128_t) x324 & Const 38685626227668133590597631; + uint128_t x334 = (uint128_t) x332 + x333; + uint128_t x335 = x331 & Const 38685626227668133590597631; + uint128_t x336 = x328 & Const 38685626227668133590597631; + uint128_t x337 = Const 77371252455336267181195262 + x295; + uint128_t x338 = x337 - x262; + uint128_t x339 = Const 77371252455336267181195262 + x296; + uint128_t x340 = x339 - x263; + uint128_t x341 = Const 77371252455336267181195254 + x297; + uint128_t x342 = x341 - x264; + uint128_t x343 = Const 77371252455336267181195262 + x295; + uint128_t x344 = x343 - x262; + uint128_t x345 = Const 77371252455336267181195262 + x296; + uint128_t x346 = x345 - x263; + uint128_t x347 = Const 77371252455336267181195254 + x297; + uint128_t x348 = x347 - x264; + Tbase (Syntax.TWord 8) x349 = x342 * x344; + Tbase (Syntax.TWord 8) x350 = x340 * x346; + Tbase (Syntax.TWord 8) x351 = x338 * x348; + Tbase (Syntax.TWord 8) x352 = x350 + x351; + Tbase (Syntax.TWord 8) x353 = x349 + x352; + Tbase (Syntax.TWord 8) x354 = x342 * x346; + Tbase (Syntax.TWord 8) x355 = x340 * x348; + Tbase (Syntax.TWord 8) x356 = x354 + x355; + Tbase (Syntax.TWord 8) x357 = x338 * x344; + Tbase (Syntax.TWord 8) x358 = Const 5 * x357; + Tbase (Syntax.TWord 8) x359 = x356 + x358; + Tbase (Syntax.TWord 8) x360 = x342 * x348; + Tbase (Syntax.TWord 8) x361 = x340 * x344; + Tbase (Syntax.TWord 8) x362 = x338 * x346; + Tbase (Syntax.TWord 8) x363 = x361 + x362; + Tbase (Syntax.TWord 8) x364 = Const 5 * x363; + Tbase (Syntax.TWord 8) x365 = x360 + x364; + uint128_t x366 = (uint128_t) (x365 >> Const 85); + Tbase (Syntax.TWord 8) x367 = x366 + x359; + uint128_t x368 = (uint128_t) (x367 >> Const 85); + Tbase (Syntax.TWord 8) x369 = x368 + x353; + uint128_t x370 = (uint128_t) x365 & Const 38685626227668133590597631; + uint128_t x371 = (uint128_t) (x369 >> Const 85); + uint128_t x372 = (uint128_t) Const 5 * x371; + uint128_t x373 = x370 + x372; + uint8_t x374 = (uint8_t) (x373 >> Const 85); + uint128_t x375 = (uint128_t) x367 & Const 38685626227668133590597631; + uint128_t x376 = (uint128_t) x374 + x375; + bool x377 = (bool) (x376 >> Const 85); + uint128_t x378 = (uint128_t) x369 & Const 38685626227668133590597631; + uint128_t x379 = (uint128_t) x377 + x378; + uint128_t x380 = x376 & Const 38685626227668133590597631; + uint128_t x381 = x373 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x382 = x17 * x379; + Tbase (Syntax.TWord 8) x383 = x19 * x380; + Tbase (Syntax.TWord 8) x384 = x18 * x381; + Tbase (Syntax.TWord 8) x385 = x383 + x384; + Tbase (Syntax.TWord 8) x386 = x382 + x385; + Tbase (Syntax.TWord 8) x387 = x17 * x380; + Tbase (Syntax.TWord 8) x388 = x19 * x381; + Tbase (Syntax.TWord 8) x389 = x387 + x388; + Tbase (Syntax.TWord 8) x390 = x18 * x379; + Tbase (Syntax.TWord 8) x391 = Const 5 * x390; + Tbase (Syntax.TWord 8) x392 = x389 + x391; + Tbase (Syntax.TWord 8) x393 = x17 * x381; + Tbase (Syntax.TWord 8) x394 = x19 * x379; + Tbase (Syntax.TWord 8) x395 = x18 * x380; + Tbase (Syntax.TWord 8) x396 = x394 + x395; + Tbase (Syntax.TWord 8) x397 = Const 5 * x396; + Tbase (Syntax.TWord 8) x398 = x393 + x397; + uint128_t x399 = (uint128_t) (x398 >> Const 85); + Tbase (Syntax.TWord 8) x400 = x399 + x392; + uint128_t x401 = (uint128_t) (x400 >> Const 85); + Tbase (Syntax.TWord 8) x402 = x401 + x386; + uint128_t x403 = (uint128_t) x398 & Const 38685626227668133590597631; + uint128_t x404 = (uint128_t) (x402 >> Const 85); + uint128_t x405 = (uint128_t) Const 5 * x404; + uint128_t x406 = x403 + x405; + uint8_t x407 = (uint8_t) (x406 >> Const 85); + uint128_t x408 = (uint128_t) x400 & Const 38685626227668133590597631; + uint128_t x409 = (uint128_t) x407 + x408; + bool x410 = (bool) (x409 >> Const 85); + uint128_t x411 = (uint128_t) x402 & Const 38685626227668133590597631; + uint128_t x412 = (uint128_t) x410 + x411; + uint128_t x413 = x409 & Const 38685626227668133590597631; + uint128_t x414 = x406 & Const 38685626227668133590597631; + (Return x145, Return x146, Return x147, + (Return x220, Return x221, Return x222), + (Return x334, Return x335, Return x336, + (Return x412, Return x413, Return x414)))) + (x, x0, (x1, x2), (x3, x4)) in + x5 in + x5, +let (_, y) := + let (x5, _) := + Eta.InterpEta + (fun var : Syntax.base_type -> Type => + λ + '(x14, x15, x13, (x18, x19, x17), (x24, x25, x23, (x28, x29, x27)), + (x34, x35, x33, (x38, x39, x37)))%core, + uint128_t x40 = x24 + x28; + uint128_t x41 = x25 + x29; + uint128_t x42 = x23 + x27; + uint128_t x43 = Const 77371252455336267181195262 + x24; + uint128_t x44 = x43 - x28; + uint128_t x45 = Const 77371252455336267181195262 + x25; + uint128_t x46 = x45 - x29; + uint128_t x47 = Const 77371252455336267181195254 + x23; + uint128_t x48 = x47 - x27; + Tbase (Syntax.TWord 8) x49 = x42 * x40; + Tbase (Syntax.TWord 8) x50 = x41 * x41; + Tbase (Syntax.TWord 8) x51 = x40 * x42; + Tbase (Syntax.TWord 8) x52 = x50 + x51; + Tbase (Syntax.TWord 8) x53 = x49 + x52; + Tbase (Syntax.TWord 8) x54 = x42 * x41; + Tbase (Syntax.TWord 8) x55 = x41 * x42; + Tbase (Syntax.TWord 8) x56 = x54 + x55; + Tbase (Syntax.TWord 8) x57 = x40 * x40; + Tbase (Syntax.TWord 8) x58 = Const 5 * x57; + Tbase (Syntax.TWord 8) x59 = x56 + x58; + Tbase (Syntax.TWord 8) x60 = x42 * x42; + Tbase (Syntax.TWord 8) x61 = x41 * x40; + Tbase (Syntax.TWord 8) x62 = x40 * x41; + Tbase (Syntax.TWord 8) x63 = x61 + x62; + Tbase (Syntax.TWord 8) x64 = Const 5 * x63; + Tbase (Syntax.TWord 8) x65 = x60 + x64; + uint128_t x66 = (uint128_t) (x65 >> Const 85); + Tbase (Syntax.TWord 8) x67 = x66 + x59; + uint128_t x68 = (uint128_t) (x67 >> Const 85); + Tbase (Syntax.TWord 8) x69 = x68 + x53; + uint128_t x70 = (uint128_t) x65 & Const 38685626227668133590597631; + uint128_t x71 = (uint128_t) (x69 >> Const 85); + uint128_t x72 = (uint128_t) Const 5 * x71; + uint128_t x73 = x70 + x72; + uint8_t x74 = (uint8_t) (x73 >> Const 85); + uint128_t x75 = (uint128_t) x67 & Const 38685626227668133590597631; + uint128_t x76 = (uint128_t) x74 + x75; + bool x77 = (bool) (x76 >> Const 85); + uint128_t x78 = (uint128_t) x69 & Const 38685626227668133590597631; + uint128_t x79 = (uint128_t) x77 + x78; + uint128_t x80 = x76 & Const 38685626227668133590597631; + uint128_t x81 = x73 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x82 = x48 * x44; + Tbase (Syntax.TWord 8) x83 = x46 * x46; + Tbase (Syntax.TWord 8) x84 = x44 * x48; + Tbase (Syntax.TWord 8) x85 = x83 + x84; + Tbase (Syntax.TWord 8) x86 = x82 + x85; + Tbase (Syntax.TWord 8) x87 = x48 * x46; + Tbase (Syntax.TWord 8) x88 = x46 * x48; + Tbase (Syntax.TWord 8) x89 = x87 + x88; + Tbase (Syntax.TWord 8) x90 = x44 * x44; + Tbase (Syntax.TWord 8) x91 = Const 5 * x90; + Tbase (Syntax.TWord 8) x92 = x89 + x91; + Tbase (Syntax.TWord 8) x93 = x48 * x48; + Tbase (Syntax.TWord 8) x94 = x46 * x44; + Tbase (Syntax.TWord 8) x95 = x44 * x46; + Tbase (Syntax.TWord 8) x96 = x94 + x95; + Tbase (Syntax.TWord 8) x97 = Const 5 * x96; + Tbase (Syntax.TWord 8) x98 = x93 + x97; + uint128_t x99 = (uint128_t) (x98 >> Const 85); + Tbase (Syntax.TWord 8) x100 = x99 + x92; + uint128_t x101 = (uint128_t) (x100 >> Const 85); + Tbase (Syntax.TWord 8) x102 = x101 + x86; + uint128_t x103 = (uint128_t) x98 & Const 38685626227668133590597631; + uint128_t x104 = (uint128_t) (x102 >> Const 85); + uint128_t x105 = (uint128_t) Const 5 * x104; + uint128_t x106 = x103 + x105; + uint8_t x107 = (uint8_t) (x106 >> Const 85); + uint128_t x108 = (uint128_t) x100 & Const 38685626227668133590597631; + uint128_t x109 = (uint128_t) x107 + x108; + bool x110 = (bool) (x109 >> Const 85); + uint128_t x111 = (uint128_t) x102 & Const 38685626227668133590597631; + uint128_t x112 = (uint128_t) x110 + x111; + uint128_t x113 = x109 & Const 38685626227668133590597631; + uint128_t x114 = x106 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x115 = x81 * x112; + Tbase (Syntax.TWord 8) x116 = x80 * x113; + Tbase (Syntax.TWord 8) x117 = x79 * x114; + Tbase (Syntax.TWord 8) x118 = x116 + x117; + Tbase (Syntax.TWord 8) x119 = x115 + x118; + Tbase (Syntax.TWord 8) x120 = x81 * x113; + Tbase (Syntax.TWord 8) x121 = x80 * x114; + Tbase (Syntax.TWord 8) x122 = x120 + x121; + Tbase (Syntax.TWord 8) x123 = x79 * x112; + Tbase (Syntax.TWord 8) x124 = Const 5 * x123; + Tbase (Syntax.TWord 8) x125 = x122 + x124; + Tbase (Syntax.TWord 8) x126 = x81 * x114; + Tbase (Syntax.TWord 8) x127 = x80 * x112; + Tbase (Syntax.TWord 8) x128 = x79 * x113; + Tbase (Syntax.TWord 8) x129 = x127 + x128; + Tbase (Syntax.TWord 8) x130 = Const 5 * x129; + Tbase (Syntax.TWord 8) x131 = x126 + x130; + uint128_t x132 = (uint128_t) (x131 >> Const 85); + Tbase (Syntax.TWord 8) x133 = x132 + x125; + uint128_t x134 = (uint128_t) (x133 >> Const 85); + Tbase (Syntax.TWord 8) x135 = x134 + x119; + uint128_t x136 = (uint128_t) x131 & Const 38685626227668133590597631; + uint128_t x137 = (uint128_t) (x135 >> Const 85); + uint128_t x138 = (uint128_t) Const 5 * x137; + uint128_t x139 = x136 + x138; + uint8_t x140 = (uint8_t) (x139 >> Const 85); + uint128_t x141 = (uint128_t) x133 & Const 38685626227668133590597631; + uint128_t x142 = (uint128_t) x140 + x141; + bool x143 = (bool) (x142 >> Const 85); + uint128_t x144 = (uint128_t) x135 & Const 38685626227668133590597631; + uint128_t x145 = (uint128_t) x143 + x144; + uint128_t x146 = x142 & Const 38685626227668133590597631; + uint128_t x147 = x139 & Const 38685626227668133590597631; + uint128_t x148 = Const 77371252455336267181195262 + x79; + uint128_t x149 = x148 - x112; + uint128_t x150 = Const 77371252455336267181195262 + x80; + uint128_t x151 = x150 - x113; + uint128_t x152 = Const 77371252455336267181195254 + x81; + uint128_t x153 = x152 - x114; + Tbase (Syntax.TWord 8) x154 = x13 * x149; + Tbase (Syntax.TWord 8) x155 = x15 * x151; + Tbase (Syntax.TWord 8) x156 = x14 * x153; + Tbase (Syntax.TWord 8) x157 = x155 + x156; + Tbase (Syntax.TWord 8) x158 = x154 + x157; + Tbase (Syntax.TWord 8) x159 = x13 * x151; + Tbase (Syntax.TWord 8) x160 = x15 * x153; + Tbase (Syntax.TWord 8) x161 = x159 + x160; + Tbase (Syntax.TWord 8) x162 = x14 * x149; + Tbase (Syntax.TWord 8) x163 = Const 5 * x162; + Tbase (Syntax.TWord 8) x164 = x161 + x163; + Tbase (Syntax.TWord 8) x165 = x13 * x153; + Tbase (Syntax.TWord 8) x166 = x15 * x149; + Tbase (Syntax.TWord 8) x167 = x14 * x151; + Tbase (Syntax.TWord 8) x168 = x166 + x167; + Tbase (Syntax.TWord 8) x169 = Const 5 * x168; + Tbase (Syntax.TWord 8) x170 = x165 + x169; + uint128_t x171 = (uint128_t) (x170 >> Const 85); + Tbase (Syntax.TWord 8) x172 = x171 + x164; + uint128_t x173 = (uint128_t) (x172 >> Const 85); + Tbase (Syntax.TWord 8) x174 = x173 + x158; + uint128_t x175 = (uint128_t) x170 & Const 38685626227668133590597631; + uint128_t x176 = (uint128_t) (x174 >> Const 85); + uint128_t x177 = (uint128_t) Const 5 * x176; + uint128_t x178 = x175 + x177; + uint8_t x179 = (uint8_t) (x178 >> Const 85); + uint128_t x180 = (uint128_t) x172 & Const 38685626227668133590597631; + uint128_t x181 = (uint128_t) x179 + x180; + bool x182 = (bool) (x181 >> Const 85); + uint128_t x183 = (uint128_t) x174 & Const 38685626227668133590597631; + uint128_t x184 = (uint128_t) x182 + x183; + uint128_t x185 = x181 & Const 38685626227668133590597631; + uint128_t x186 = x178 & Const 38685626227668133590597631; + uint128_t x187 = x79 + x184; + uint128_t x188 = x80 + x185; + uint128_t x189 = x81 + x186; + Tbase (Syntax.TWord 8) x190 = x153 * x187; + Tbase (Syntax.TWord 8) x191 = x151 * x188; + Tbase (Syntax.TWord 8) x192 = x149 * x189; + Tbase (Syntax.TWord 8) x193 = x191 + x192; + Tbase (Syntax.TWord 8) x194 = x190 + x193; + Tbase (Syntax.TWord 8) x195 = x153 * x188; + Tbase (Syntax.TWord 8) x196 = x151 * x189; + Tbase (Syntax.TWord 8) x197 = x195 + x196; + Tbase (Syntax.TWord 8) x198 = x149 * x187; + Tbase (Syntax.TWord 8) x199 = Const 5 * x198; + Tbase (Syntax.TWord 8) x200 = x197 + x199; + Tbase (Syntax.TWord 8) x201 = x153 * x189; + Tbase (Syntax.TWord 8) x202 = x151 * x187; + Tbase (Syntax.TWord 8) x203 = x149 * x188; + Tbase (Syntax.TWord 8) x204 = x202 + x203; + Tbase (Syntax.TWord 8) x205 = Const 5 * x204; + Tbase (Syntax.TWord 8) x206 = x201 + x205; + uint128_t x207 = (uint128_t) (x206 >> Const 85); + Tbase (Syntax.TWord 8) x208 = x207 + x200; + uint128_t x209 = (uint128_t) (x208 >> Const 85); + Tbase (Syntax.TWord 8) x210 = x209 + x194; + uint128_t x211 = (uint128_t) x206 & Const 38685626227668133590597631; + uint128_t x212 = (uint128_t) (x210 >> Const 85); + uint128_t x213 = (uint128_t) Const 5 * x212; + uint128_t x214 = x211 + x213; + uint8_t x215 = (uint8_t) (x214 >> Const 85); + uint128_t x216 = (uint128_t) x208 & Const 38685626227668133590597631; + uint128_t x217 = (uint128_t) x215 + x216; + bool x218 = (bool) (x217 >> Const 85); + uint128_t x219 = (uint128_t) x210 & Const 38685626227668133590597631; + uint128_t x220 = (uint128_t) x218 + x219; + uint128_t x221 = x217 & Const 38685626227668133590597631; + uint128_t x222 = x214 & Const 38685626227668133590597631; + uint128_t x223 = x34 + x38; + uint128_t x224 = x35 + x39; + uint128_t x225 = x33 + x37; + uint128_t x226 = Const 77371252455336267181195262 + x34; + uint128_t x227 = x226 - x38; + uint128_t x228 = Const 77371252455336267181195262 + x35; + uint128_t x229 = x228 - x39; + uint128_t x230 = Const 77371252455336267181195254 + x33; + uint128_t x231 = x230 - x37; + Tbase (Syntax.TWord 8) x232 = x225 * x44; + Tbase (Syntax.TWord 8) x233 = x224 * x46; + Tbase (Syntax.TWord 8) x234 = x223 * x48; + Tbase (Syntax.TWord 8) x235 = x233 + x234; + Tbase (Syntax.TWord 8) x236 = x232 + x235; + Tbase (Syntax.TWord 8) x237 = x225 * x46; + Tbase (Syntax.TWord 8) x238 = x224 * x48; + Tbase (Syntax.TWord 8) x239 = x237 + x238; + Tbase (Syntax.TWord 8) x240 = x223 * x44; + Tbase (Syntax.TWord 8) x241 = Const 5 * x240; + Tbase (Syntax.TWord 8) x242 = x239 + x241; + Tbase (Syntax.TWord 8) x243 = x225 * x48; + Tbase (Syntax.TWord 8) x244 = x224 * x44; + Tbase (Syntax.TWord 8) x245 = x223 * x46; + Tbase (Syntax.TWord 8) x246 = x244 + x245; + Tbase (Syntax.TWord 8) x247 = Const 5 * x246; + Tbase (Syntax.TWord 8) x248 = x243 + x247; + uint128_t x249 = (uint128_t) (x248 >> Const 85); + Tbase (Syntax.TWord 8) x250 = x249 + x242; + uint128_t x251 = (uint128_t) (x250 >> Const 85); + Tbase (Syntax.TWord 8) x252 = x251 + x236; + uint128_t x253 = (uint128_t) x248 & Const 38685626227668133590597631; + uint128_t x254 = (uint128_t) (x252 >> Const 85); + uint128_t x255 = (uint128_t) Const 5 * x254; + uint128_t x256 = x253 + x255; + uint8_t x257 = (uint8_t) (x256 >> Const 85); + uint128_t x258 = (uint128_t) x250 & Const 38685626227668133590597631; + uint128_t x259 = (uint128_t) x257 + x258; + bool x260 = (bool) (x259 >> Const 85); + uint128_t x261 = (uint128_t) x252 & Const 38685626227668133590597631; + uint128_t x262 = (uint128_t) x260 + x261; + uint128_t x263 = x259 & Const 38685626227668133590597631; + uint128_t x264 = x256 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x265 = x231 * x40; + Tbase (Syntax.TWord 8) x266 = x229 * x41; + Tbase (Syntax.TWord 8) x267 = x227 * x42; + Tbase (Syntax.TWord 8) x268 = x266 + x267; + Tbase (Syntax.TWord 8) x269 = x265 + x268; + Tbase (Syntax.TWord 8) x270 = x231 * x41; + Tbase (Syntax.TWord 8) x271 = x229 * x42; + Tbase (Syntax.TWord 8) x272 = x270 + x271; + Tbase (Syntax.TWord 8) x273 = x227 * x40; + Tbase (Syntax.TWord 8) x274 = Const 5 * x273; + Tbase (Syntax.TWord 8) x275 = x272 + x274; + Tbase (Syntax.TWord 8) x276 = x231 * x42; + Tbase (Syntax.TWord 8) x277 = x229 * x40; + Tbase (Syntax.TWord 8) x278 = x227 * x41; + Tbase (Syntax.TWord 8) x279 = x277 + x278; + Tbase (Syntax.TWord 8) x280 = Const 5 * x279; + Tbase (Syntax.TWord 8) x281 = x276 + x280; + uint128_t x282 = (uint128_t) (x281 >> Const 85); + Tbase (Syntax.TWord 8) x283 = x282 + x275; + uint128_t x284 = (uint128_t) (x283 >> Const 85); + Tbase (Syntax.TWord 8) x285 = x284 + x269; + uint128_t x286 = (uint128_t) x281 & Const 38685626227668133590597631; + uint128_t x287 = (uint128_t) (x285 >> Const 85); + uint128_t x288 = (uint128_t) Const 5 * x287; + uint128_t x289 = x286 + x288; + uint8_t x290 = (uint8_t) (x289 >> Const 85); + uint128_t x291 = (uint128_t) x283 & Const 38685626227668133590597631; + uint128_t x292 = (uint128_t) x290 + x291; + bool x293 = (bool) (x292 >> Const 85); + uint128_t x294 = (uint128_t) x285 & Const 38685626227668133590597631; + uint128_t x295 = (uint128_t) x293 + x294; + uint128_t x296 = x292 & Const 38685626227668133590597631; + uint128_t x297 = x289 & Const 38685626227668133590597631; + uint128_t x298 = x295 + x262; + uint128_t x299 = x296 + x263; + uint128_t x300 = x297 + x264; + uint128_t x301 = x295 + x262; + uint128_t x302 = x296 + x263; + uint128_t x303 = x297 + x264; + Tbase (Syntax.TWord 8) x304 = x300 * x301; + Tbase (Syntax.TWord 8) x305 = x299 * x302; + Tbase (Syntax.TWord 8) x306 = x298 * x303; + Tbase (Syntax.TWord 8) x307 = x305 + x306; + Tbase (Syntax.TWord 8) x308 = x304 + x307; + Tbase (Syntax.TWord 8) x309 = x300 * x302; + Tbase (Syntax.TWord 8) x310 = x299 * x303; + Tbase (Syntax.TWord 8) x311 = x309 + x310; + Tbase (Syntax.TWord 8) x312 = x298 * x301; + Tbase (Syntax.TWord 8) x313 = Const 5 * x312; + Tbase (Syntax.TWord 8) x314 = x311 + x313; + Tbase (Syntax.TWord 8) x315 = x300 * x303; + Tbase (Syntax.TWord 8) x316 = x299 * x301; + Tbase (Syntax.TWord 8) x317 = x298 * x302; + Tbase (Syntax.TWord 8) x318 = x316 + x317; + Tbase (Syntax.TWord 8) x319 = Const 5 * x318; + Tbase (Syntax.TWord 8) x320 = x315 + x319; + uint128_t x321 = (uint128_t) (x320 >> Const 85); + Tbase (Syntax.TWord 8) x322 = x321 + x314; + uint128_t x323 = (uint128_t) (x322 >> Const 85); + Tbase (Syntax.TWord 8) x324 = x323 + x308; + uint128_t x325 = (uint128_t) x320 & Const 38685626227668133590597631; + uint128_t x326 = (uint128_t) (x324 >> Const 85); + uint128_t x327 = (uint128_t) Const 5 * x326; + uint128_t x328 = x325 + x327; + uint8_t x329 = (uint8_t) (x328 >> Const 85); + uint128_t x330 = (uint128_t) x322 & Const 38685626227668133590597631; + uint128_t x331 = (uint128_t) x329 + x330; + bool x332 = (bool) (x331 >> Const 85); + uint128_t x333 = (uint128_t) x324 & Const 38685626227668133590597631; + uint128_t x334 = (uint128_t) x332 + x333; + uint128_t x335 = x331 & Const 38685626227668133590597631; + uint128_t x336 = x328 & Const 38685626227668133590597631; + uint128_t x337 = Const 77371252455336267181195262 + x295; + uint128_t x338 = x337 - x262; + uint128_t x339 = Const 77371252455336267181195262 + x296; + uint128_t x340 = x339 - x263; + uint128_t x341 = Const 77371252455336267181195254 + x297; + uint128_t x342 = x341 - x264; + uint128_t x343 = Const 77371252455336267181195262 + x295; + uint128_t x344 = x343 - x262; + uint128_t x345 = Const 77371252455336267181195262 + x296; + uint128_t x346 = x345 - x263; + uint128_t x347 = Const 77371252455336267181195254 + x297; + uint128_t x348 = x347 - x264; + Tbase (Syntax.TWord 8) x349 = x342 * x344; + Tbase (Syntax.TWord 8) x350 = x340 * x346; + Tbase (Syntax.TWord 8) x351 = x338 * x348; + Tbase (Syntax.TWord 8) x352 = x350 + x351; + Tbase (Syntax.TWord 8) x353 = x349 + x352; + Tbase (Syntax.TWord 8) x354 = x342 * x346; + Tbase (Syntax.TWord 8) x355 = x340 * x348; + Tbase (Syntax.TWord 8) x356 = x354 + x355; + Tbase (Syntax.TWord 8) x357 = x338 * x344; + Tbase (Syntax.TWord 8) x358 = Const 5 * x357; + Tbase (Syntax.TWord 8) x359 = x356 + x358; + Tbase (Syntax.TWord 8) x360 = x342 * x348; + Tbase (Syntax.TWord 8) x361 = x340 * x344; + Tbase (Syntax.TWord 8) x362 = x338 * x346; + Tbase (Syntax.TWord 8) x363 = x361 + x362; + Tbase (Syntax.TWord 8) x364 = Const 5 * x363; + Tbase (Syntax.TWord 8) x365 = x360 + x364; + uint128_t x366 = (uint128_t) (x365 >> Const 85); + Tbase (Syntax.TWord 8) x367 = x366 + x359; + uint128_t x368 = (uint128_t) (x367 >> Const 85); + Tbase (Syntax.TWord 8) x369 = x368 + x353; + uint128_t x370 = (uint128_t) x365 & Const 38685626227668133590597631; + uint128_t x371 = (uint128_t) (x369 >> Const 85); + uint128_t x372 = (uint128_t) Const 5 * x371; + uint128_t x373 = x370 + x372; + uint8_t x374 = (uint8_t) (x373 >> Const 85); + uint128_t x375 = (uint128_t) x367 & Const 38685626227668133590597631; + uint128_t x376 = (uint128_t) x374 + x375; + bool x377 = (bool) (x376 >> Const 85); + uint128_t x378 = (uint128_t) x369 & Const 38685626227668133590597631; + uint128_t x379 = (uint128_t) x377 + x378; + uint128_t x380 = x376 & Const 38685626227668133590597631; + uint128_t x381 = x373 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x382 = x17 * x379; + Tbase (Syntax.TWord 8) x383 = x19 * x380; + Tbase (Syntax.TWord 8) x384 = x18 * x381; + Tbase (Syntax.TWord 8) x385 = x383 + x384; + Tbase (Syntax.TWord 8) x386 = x382 + x385; + Tbase (Syntax.TWord 8) x387 = x17 * x380; + Tbase (Syntax.TWord 8) x388 = x19 * x381; + Tbase (Syntax.TWord 8) x389 = x387 + x388; + Tbase (Syntax.TWord 8) x390 = x18 * x379; + Tbase (Syntax.TWord 8) x391 = Const 5 * x390; + Tbase (Syntax.TWord 8) x392 = x389 + x391; + Tbase (Syntax.TWord 8) x393 = x17 * x381; + Tbase (Syntax.TWord 8) x394 = x19 * x379; + Tbase (Syntax.TWord 8) x395 = x18 * x380; + Tbase (Syntax.TWord 8) x396 = x394 + x395; + Tbase (Syntax.TWord 8) x397 = Const 5 * x396; + Tbase (Syntax.TWord 8) x398 = x393 + x397; + uint128_t x399 = (uint128_t) (x398 >> Const 85); + Tbase (Syntax.TWord 8) x400 = x399 + x392; + uint128_t x401 = (uint128_t) (x400 >> Const 85); + Tbase (Syntax.TWord 8) x402 = x401 + x386; + uint128_t x403 = (uint128_t) x398 & Const 38685626227668133590597631; + uint128_t x404 = (uint128_t) (x402 >> Const 85); + uint128_t x405 = (uint128_t) Const 5 * x404; + uint128_t x406 = x403 + x405; + uint8_t x407 = (uint8_t) (x406 >> Const 85); + uint128_t x408 = (uint128_t) x400 & Const 38685626227668133590597631; + uint128_t x409 = (uint128_t) x407 + x408; + bool x410 = (bool) (x409 >> Const 85); + uint128_t x411 = (uint128_t) x402 & Const 38685626227668133590597631; + uint128_t x412 = (uint128_t) x410 + x411; + uint128_t x413 = x409 & Const 38685626227668133590597631; + uint128_t x414 = x406 & Const 38685626227668133590597631; + (Return x145, Return x146, Return x147, + (Return x220, Return x221, Return x222), + (Return x334, Return x335, Return x336, + (Return x412, Return x413, Return x414)))) + (x, x0, (x1, x2), (x3, x4)) in + x5 in +y, +(let (x5, _) := + let (_, y) := + Eta.InterpEta + (fun var : Syntax.base_type -> Type => + λ + '(x14, x15, x13, (x18, x19, x17), (x24, x25, x23, (x28, x29, x27)), + (x34, x35, x33, (x38, x39, x37)))%core, + uint128_t x40 = x24 + x28; + uint128_t x41 = x25 + x29; + uint128_t x42 = x23 + x27; + uint128_t x43 = Const 77371252455336267181195262 + x24; + uint128_t x44 = x43 - x28; + uint128_t x45 = Const 77371252455336267181195262 + x25; + uint128_t x46 = x45 - x29; + uint128_t x47 = Const 77371252455336267181195254 + x23; + uint128_t x48 = x47 - x27; + Tbase (Syntax.TWord 8) x49 = x42 * x40; + Tbase (Syntax.TWord 8) x50 = x41 * x41; + Tbase (Syntax.TWord 8) x51 = x40 * x42; + Tbase (Syntax.TWord 8) x52 = x50 + x51; + Tbase (Syntax.TWord 8) x53 = x49 + x52; + Tbase (Syntax.TWord 8) x54 = x42 * x41; + Tbase (Syntax.TWord 8) x55 = x41 * x42; + Tbase (Syntax.TWord 8) x56 = x54 + x55; + Tbase (Syntax.TWord 8) x57 = x40 * x40; + Tbase (Syntax.TWord 8) x58 = Const 5 * x57; + Tbase (Syntax.TWord 8) x59 = x56 + x58; + Tbase (Syntax.TWord 8) x60 = x42 * x42; + Tbase (Syntax.TWord 8) x61 = x41 * x40; + Tbase (Syntax.TWord 8) x62 = x40 * x41; + Tbase (Syntax.TWord 8) x63 = x61 + x62; + Tbase (Syntax.TWord 8) x64 = Const 5 * x63; + Tbase (Syntax.TWord 8) x65 = x60 + x64; + uint128_t x66 = (uint128_t) (x65 >> Const 85); + Tbase (Syntax.TWord 8) x67 = x66 + x59; + uint128_t x68 = (uint128_t) (x67 >> Const 85); + Tbase (Syntax.TWord 8) x69 = x68 + x53; + uint128_t x70 = (uint128_t) x65 & Const 38685626227668133590597631; + uint128_t x71 = (uint128_t) (x69 >> Const 85); + uint128_t x72 = (uint128_t) Const 5 * x71; + uint128_t x73 = x70 + x72; + uint8_t x74 = (uint8_t) (x73 >> Const 85); + uint128_t x75 = (uint128_t) x67 & Const 38685626227668133590597631; + uint128_t x76 = (uint128_t) x74 + x75; + bool x77 = (bool) (x76 >> Const 85); + uint128_t x78 = (uint128_t) x69 & Const 38685626227668133590597631; + uint128_t x79 = (uint128_t) x77 + x78; + uint128_t x80 = x76 & Const 38685626227668133590597631; + uint128_t x81 = x73 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x82 = x48 * x44; + Tbase (Syntax.TWord 8) x83 = x46 * x46; + Tbase (Syntax.TWord 8) x84 = x44 * x48; + Tbase (Syntax.TWord 8) x85 = x83 + x84; + Tbase (Syntax.TWord 8) x86 = x82 + x85; + Tbase (Syntax.TWord 8) x87 = x48 * x46; + Tbase (Syntax.TWord 8) x88 = x46 * x48; + Tbase (Syntax.TWord 8) x89 = x87 + x88; + Tbase (Syntax.TWord 8) x90 = x44 * x44; + Tbase (Syntax.TWord 8) x91 = Const 5 * x90; + Tbase (Syntax.TWord 8) x92 = x89 + x91; + Tbase (Syntax.TWord 8) x93 = x48 * x48; + Tbase (Syntax.TWord 8) x94 = x46 * x44; + Tbase (Syntax.TWord 8) x95 = x44 * x46; + Tbase (Syntax.TWord 8) x96 = x94 + x95; + Tbase (Syntax.TWord 8) x97 = Const 5 * x96; + Tbase (Syntax.TWord 8) x98 = x93 + x97; + uint128_t x99 = (uint128_t) (x98 >> Const 85); + Tbase (Syntax.TWord 8) x100 = x99 + x92; + uint128_t x101 = (uint128_t) (x100 >> Const 85); + Tbase (Syntax.TWord 8) x102 = x101 + x86; + uint128_t x103 = (uint128_t) x98 & Const 38685626227668133590597631; + uint128_t x104 = (uint128_t) (x102 >> Const 85); + uint128_t x105 = (uint128_t) Const 5 * x104; + uint128_t x106 = x103 + x105; + uint8_t x107 = (uint8_t) (x106 >> Const 85); + uint128_t x108 = (uint128_t) x100 & Const 38685626227668133590597631; + uint128_t x109 = (uint128_t) x107 + x108; + bool x110 = (bool) (x109 >> Const 85); + uint128_t x111 = (uint128_t) x102 & Const 38685626227668133590597631; + uint128_t x112 = (uint128_t) x110 + x111; + uint128_t x113 = x109 & Const 38685626227668133590597631; + uint128_t x114 = x106 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x115 = x81 * x112; + Tbase (Syntax.TWord 8) x116 = x80 * x113; + Tbase (Syntax.TWord 8) x117 = x79 * x114; + Tbase (Syntax.TWord 8) x118 = x116 + x117; + Tbase (Syntax.TWord 8) x119 = x115 + x118; + Tbase (Syntax.TWord 8) x120 = x81 * x113; + Tbase (Syntax.TWord 8) x121 = x80 * x114; + Tbase (Syntax.TWord 8) x122 = x120 + x121; + Tbase (Syntax.TWord 8) x123 = x79 * x112; + Tbase (Syntax.TWord 8) x124 = Const 5 * x123; + Tbase (Syntax.TWord 8) x125 = x122 + x124; + Tbase (Syntax.TWord 8) x126 = x81 * x114; + Tbase (Syntax.TWord 8) x127 = x80 * x112; + Tbase (Syntax.TWord 8) x128 = x79 * x113; + Tbase (Syntax.TWord 8) x129 = x127 + x128; + Tbase (Syntax.TWord 8) x130 = Const 5 * x129; + Tbase (Syntax.TWord 8) x131 = x126 + x130; + uint128_t x132 = (uint128_t) (x131 >> Const 85); + Tbase (Syntax.TWord 8) x133 = x132 + x125; + uint128_t x134 = (uint128_t) (x133 >> Const 85); + Tbase (Syntax.TWord 8) x135 = x134 + x119; + uint128_t x136 = (uint128_t) x131 & Const 38685626227668133590597631; + uint128_t x137 = (uint128_t) (x135 >> Const 85); + uint128_t x138 = (uint128_t) Const 5 * x137; + uint128_t x139 = x136 + x138; + uint8_t x140 = (uint8_t) (x139 >> Const 85); + uint128_t x141 = (uint128_t) x133 & Const 38685626227668133590597631; + uint128_t x142 = (uint128_t) x140 + x141; + bool x143 = (bool) (x142 >> Const 85); + uint128_t x144 = (uint128_t) x135 & Const 38685626227668133590597631; + uint128_t x145 = (uint128_t) x143 + x144; + uint128_t x146 = x142 & Const 38685626227668133590597631; + uint128_t x147 = x139 & Const 38685626227668133590597631; + uint128_t x148 = Const 77371252455336267181195262 + x79; + uint128_t x149 = x148 - x112; + uint128_t x150 = Const 77371252455336267181195262 + x80; + uint128_t x151 = x150 - x113; + uint128_t x152 = Const 77371252455336267181195254 + x81; + uint128_t x153 = x152 - x114; + Tbase (Syntax.TWord 8) x154 = x13 * x149; + Tbase (Syntax.TWord 8) x155 = x15 * x151; + Tbase (Syntax.TWord 8) x156 = x14 * x153; + Tbase (Syntax.TWord 8) x157 = x155 + x156; + Tbase (Syntax.TWord 8) x158 = x154 + x157; + Tbase (Syntax.TWord 8) x159 = x13 * x151; + Tbase (Syntax.TWord 8) x160 = x15 * x153; + Tbase (Syntax.TWord 8) x161 = x159 + x160; + Tbase (Syntax.TWord 8) x162 = x14 * x149; + Tbase (Syntax.TWord 8) x163 = Const 5 * x162; + Tbase (Syntax.TWord 8) x164 = x161 + x163; + Tbase (Syntax.TWord 8) x165 = x13 * x153; + Tbase (Syntax.TWord 8) x166 = x15 * x149; + Tbase (Syntax.TWord 8) x167 = x14 * x151; + Tbase (Syntax.TWord 8) x168 = x166 + x167; + Tbase (Syntax.TWord 8) x169 = Const 5 * x168; + Tbase (Syntax.TWord 8) x170 = x165 + x169; + uint128_t x171 = (uint128_t) (x170 >> Const 85); + Tbase (Syntax.TWord 8) x172 = x171 + x164; + uint128_t x173 = (uint128_t) (x172 >> Const 85); + Tbase (Syntax.TWord 8) x174 = x173 + x158; + uint128_t x175 = (uint128_t) x170 & Const 38685626227668133590597631; + uint128_t x176 = (uint128_t) (x174 >> Const 85); + uint128_t x177 = (uint128_t) Const 5 * x176; + uint128_t x178 = x175 + x177; + uint8_t x179 = (uint8_t) (x178 >> Const 85); + uint128_t x180 = (uint128_t) x172 & Const 38685626227668133590597631; + uint128_t x181 = (uint128_t) x179 + x180; + bool x182 = (bool) (x181 >> Const 85); + uint128_t x183 = (uint128_t) x174 & Const 38685626227668133590597631; + uint128_t x184 = (uint128_t) x182 + x183; + uint128_t x185 = x181 & Const 38685626227668133590597631; + uint128_t x186 = x178 & Const 38685626227668133590597631; + uint128_t x187 = x79 + x184; + uint128_t x188 = x80 + x185; + uint128_t x189 = x81 + x186; + Tbase (Syntax.TWord 8) x190 = x153 * x187; + Tbase (Syntax.TWord 8) x191 = x151 * x188; + Tbase (Syntax.TWord 8) x192 = x149 * x189; + Tbase (Syntax.TWord 8) x193 = x191 + x192; + Tbase (Syntax.TWord 8) x194 = x190 + x193; + Tbase (Syntax.TWord 8) x195 = x153 * x188; + Tbase (Syntax.TWord 8) x196 = x151 * x189; + Tbase (Syntax.TWord 8) x197 = x195 + x196; + Tbase (Syntax.TWord 8) x198 = x149 * x187; + Tbase (Syntax.TWord 8) x199 = Const 5 * x198; + Tbase (Syntax.TWord 8) x200 = x197 + x199; + Tbase (Syntax.TWord 8) x201 = x153 * x189; + Tbase (Syntax.TWord 8) x202 = x151 * x187; + Tbase (Syntax.TWord 8) x203 = x149 * x188; + Tbase (Syntax.TWord 8) x204 = x202 + x203; + Tbase (Syntax.TWord 8) x205 = Const 5 * x204; + Tbase (Syntax.TWord 8) x206 = x201 + x205; + uint128_t x207 = (uint128_t) (x206 >> Const 85); + Tbase (Syntax.TWord 8) x208 = x207 + x200; + uint128_t x209 = (uint128_t) (x208 >> Const 85); + Tbase (Syntax.TWord 8) x210 = x209 + x194; + uint128_t x211 = (uint128_t) x206 & Const 38685626227668133590597631; + uint128_t x212 = (uint128_t) (x210 >> Const 85); + uint128_t x213 = (uint128_t) Const 5 * x212; + uint128_t x214 = x211 + x213; + uint8_t x215 = (uint8_t) (x214 >> Const 85); + uint128_t x216 = (uint128_t) x208 & Const 38685626227668133590597631; + uint128_t x217 = (uint128_t) x215 + x216; + bool x218 = (bool) (x217 >> Const 85); + uint128_t x219 = (uint128_t) x210 & Const 38685626227668133590597631; + uint128_t x220 = (uint128_t) x218 + x219; + uint128_t x221 = x217 & Const 38685626227668133590597631; + uint128_t x222 = x214 & Const 38685626227668133590597631; + uint128_t x223 = x34 + x38; + uint128_t x224 = x35 + x39; + uint128_t x225 = x33 + x37; + uint128_t x226 = Const 77371252455336267181195262 + x34; + uint128_t x227 = x226 - x38; + uint128_t x228 = Const 77371252455336267181195262 + x35; + uint128_t x229 = x228 - x39; + uint128_t x230 = Const 77371252455336267181195254 + x33; + uint128_t x231 = x230 - x37; + Tbase (Syntax.TWord 8) x232 = x225 * x44; + Tbase (Syntax.TWord 8) x233 = x224 * x46; + Tbase (Syntax.TWord 8) x234 = x223 * x48; + Tbase (Syntax.TWord 8) x235 = x233 + x234; + Tbase (Syntax.TWord 8) x236 = x232 + x235; + Tbase (Syntax.TWord 8) x237 = x225 * x46; + Tbase (Syntax.TWord 8) x238 = x224 * x48; + Tbase (Syntax.TWord 8) x239 = x237 + x238; + Tbase (Syntax.TWord 8) x240 = x223 * x44; + Tbase (Syntax.TWord 8) x241 = Const 5 * x240; + Tbase (Syntax.TWord 8) x242 = x239 + x241; + Tbase (Syntax.TWord 8) x243 = x225 * x48; + Tbase (Syntax.TWord 8) x244 = x224 * x44; + Tbase (Syntax.TWord 8) x245 = x223 * x46; + Tbase (Syntax.TWord 8) x246 = x244 + x245; + Tbase (Syntax.TWord 8) x247 = Const 5 * x246; + Tbase (Syntax.TWord 8) x248 = x243 + x247; + uint128_t x249 = (uint128_t) (x248 >> Const 85); + Tbase (Syntax.TWord 8) x250 = x249 + x242; + uint128_t x251 = (uint128_t) (x250 >> Const 85); + Tbase (Syntax.TWord 8) x252 = x251 + x236; + uint128_t x253 = (uint128_t) x248 & Const 38685626227668133590597631; + uint128_t x254 = (uint128_t) (x252 >> Const 85); + uint128_t x255 = (uint128_t) Const 5 * x254; + uint128_t x256 = x253 + x255; + uint8_t x257 = (uint8_t) (x256 >> Const 85); + uint128_t x258 = (uint128_t) x250 & Const 38685626227668133590597631; + uint128_t x259 = (uint128_t) x257 + x258; + bool x260 = (bool) (x259 >> Const 85); + uint128_t x261 = (uint128_t) x252 & Const 38685626227668133590597631; + uint128_t x262 = (uint128_t) x260 + x261; + uint128_t x263 = x259 & Const 38685626227668133590597631; + uint128_t x264 = x256 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x265 = x231 * x40; + Tbase (Syntax.TWord 8) x266 = x229 * x41; + Tbase (Syntax.TWord 8) x267 = x227 * x42; + Tbase (Syntax.TWord 8) x268 = x266 + x267; + Tbase (Syntax.TWord 8) x269 = x265 + x268; + Tbase (Syntax.TWord 8) x270 = x231 * x41; + Tbase (Syntax.TWord 8) x271 = x229 * x42; + Tbase (Syntax.TWord 8) x272 = x270 + x271; + Tbase (Syntax.TWord 8) x273 = x227 * x40; + Tbase (Syntax.TWord 8) x274 = Const 5 * x273; + Tbase (Syntax.TWord 8) x275 = x272 + x274; + Tbase (Syntax.TWord 8) x276 = x231 * x42; + Tbase (Syntax.TWord 8) x277 = x229 * x40; + Tbase (Syntax.TWord 8) x278 = x227 * x41; + Tbase (Syntax.TWord 8) x279 = x277 + x278; + Tbase (Syntax.TWord 8) x280 = Const 5 * x279; + Tbase (Syntax.TWord 8) x281 = x276 + x280; + uint128_t x282 = (uint128_t) (x281 >> Const 85); + Tbase (Syntax.TWord 8) x283 = x282 + x275; + uint128_t x284 = (uint128_t) (x283 >> Const 85); + Tbase (Syntax.TWord 8) x285 = x284 + x269; + uint128_t x286 = (uint128_t) x281 & Const 38685626227668133590597631; + uint128_t x287 = (uint128_t) (x285 >> Const 85); + uint128_t x288 = (uint128_t) Const 5 * x287; + uint128_t x289 = x286 + x288; + uint8_t x290 = (uint8_t) (x289 >> Const 85); + uint128_t x291 = (uint128_t) x283 & Const 38685626227668133590597631; + uint128_t x292 = (uint128_t) x290 + x291; + bool x293 = (bool) (x292 >> Const 85); + uint128_t x294 = (uint128_t) x285 & Const 38685626227668133590597631; + uint128_t x295 = (uint128_t) x293 + x294; + uint128_t x296 = x292 & Const 38685626227668133590597631; + uint128_t x297 = x289 & Const 38685626227668133590597631; + uint128_t x298 = x295 + x262; + uint128_t x299 = x296 + x263; + uint128_t x300 = x297 + x264; + uint128_t x301 = x295 + x262; + uint128_t x302 = x296 + x263; + uint128_t x303 = x297 + x264; + Tbase (Syntax.TWord 8) x304 = x300 * x301; + Tbase (Syntax.TWord 8) x305 = x299 * x302; + Tbase (Syntax.TWord 8) x306 = x298 * x303; + Tbase (Syntax.TWord 8) x307 = x305 + x306; + Tbase (Syntax.TWord 8) x308 = x304 + x307; + Tbase (Syntax.TWord 8) x309 = x300 * x302; + Tbase (Syntax.TWord 8) x310 = x299 * x303; + Tbase (Syntax.TWord 8) x311 = x309 + x310; + Tbase (Syntax.TWord 8) x312 = x298 * x301; + Tbase (Syntax.TWord 8) x313 = Const 5 * x312; + Tbase (Syntax.TWord 8) x314 = x311 + x313; + Tbase (Syntax.TWord 8) x315 = x300 * x303; + Tbase (Syntax.TWord 8) x316 = x299 * x301; + Tbase (Syntax.TWord 8) x317 = x298 * x302; + Tbase (Syntax.TWord 8) x318 = x316 + x317; + Tbase (Syntax.TWord 8) x319 = Const 5 * x318; + Tbase (Syntax.TWord 8) x320 = x315 + x319; + uint128_t x321 = (uint128_t) (x320 >> Const 85); + Tbase (Syntax.TWord 8) x322 = x321 + x314; + uint128_t x323 = (uint128_t) (x322 >> Const 85); + Tbase (Syntax.TWord 8) x324 = x323 + x308; + uint128_t x325 = (uint128_t) x320 & Const 38685626227668133590597631; + uint128_t x326 = (uint128_t) (x324 >> Const 85); + uint128_t x327 = (uint128_t) Const 5 * x326; + uint128_t x328 = x325 + x327; + uint8_t x329 = (uint8_t) (x328 >> Const 85); + uint128_t x330 = (uint128_t) x322 & Const 38685626227668133590597631; + uint128_t x331 = (uint128_t) x329 + x330; + bool x332 = (bool) (x331 >> Const 85); + uint128_t x333 = (uint128_t) x324 & Const 38685626227668133590597631; + uint128_t x334 = (uint128_t) x332 + x333; + uint128_t x335 = x331 & Const 38685626227668133590597631; + uint128_t x336 = x328 & Const 38685626227668133590597631; + uint128_t x337 = Const 77371252455336267181195262 + x295; + uint128_t x338 = x337 - x262; + uint128_t x339 = Const 77371252455336267181195262 + x296; + uint128_t x340 = x339 - x263; + uint128_t x341 = Const 77371252455336267181195254 + x297; + uint128_t x342 = x341 - x264; + uint128_t x343 = Const 77371252455336267181195262 + x295; + uint128_t x344 = x343 - x262; + uint128_t x345 = Const 77371252455336267181195262 + x296; + uint128_t x346 = x345 - x263; + uint128_t x347 = Const 77371252455336267181195254 + x297; + uint128_t x348 = x347 - x264; + Tbase (Syntax.TWord 8) x349 = x342 * x344; + Tbase (Syntax.TWord 8) x350 = x340 * x346; + Tbase (Syntax.TWord 8) x351 = x338 * x348; + Tbase (Syntax.TWord 8) x352 = x350 + x351; + Tbase (Syntax.TWord 8) x353 = x349 + x352; + Tbase (Syntax.TWord 8) x354 = x342 * x346; + Tbase (Syntax.TWord 8) x355 = x340 * x348; + Tbase (Syntax.TWord 8) x356 = x354 + x355; + Tbase (Syntax.TWord 8) x357 = x338 * x344; + Tbase (Syntax.TWord 8) x358 = Const 5 * x357; + Tbase (Syntax.TWord 8) x359 = x356 + x358; + Tbase (Syntax.TWord 8) x360 = x342 * x348; + Tbase (Syntax.TWord 8) x361 = x340 * x344; + Tbase (Syntax.TWord 8) x362 = x338 * x346; + Tbase (Syntax.TWord 8) x363 = x361 + x362; + Tbase (Syntax.TWord 8) x364 = Const 5 * x363; + Tbase (Syntax.TWord 8) x365 = x360 + x364; + uint128_t x366 = (uint128_t) (x365 >> Const 85); + Tbase (Syntax.TWord 8) x367 = x366 + x359; + uint128_t x368 = (uint128_t) (x367 >> Const 85); + Tbase (Syntax.TWord 8) x369 = x368 + x353; + uint128_t x370 = (uint128_t) x365 & Const 38685626227668133590597631; + uint128_t x371 = (uint128_t) (x369 >> Const 85); + uint128_t x372 = (uint128_t) Const 5 * x371; + uint128_t x373 = x370 + x372; + uint8_t x374 = (uint8_t) (x373 >> Const 85); + uint128_t x375 = (uint128_t) x367 & Const 38685626227668133590597631; + uint128_t x376 = (uint128_t) x374 + x375; + bool x377 = (bool) (x376 >> Const 85); + uint128_t x378 = (uint128_t) x369 & Const 38685626227668133590597631; + uint128_t x379 = (uint128_t) x377 + x378; + uint128_t x380 = x376 & Const 38685626227668133590597631; + uint128_t x381 = x373 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x382 = x17 * x379; + Tbase (Syntax.TWord 8) x383 = x19 * x380; + Tbase (Syntax.TWord 8) x384 = x18 * x381; + Tbase (Syntax.TWord 8) x385 = x383 + x384; + Tbase (Syntax.TWord 8) x386 = x382 + x385; + Tbase (Syntax.TWord 8) x387 = x17 * x380; + Tbase (Syntax.TWord 8) x388 = x19 * x381; + Tbase (Syntax.TWord 8) x389 = x387 + x388; + Tbase (Syntax.TWord 8) x390 = x18 * x379; + Tbase (Syntax.TWord 8) x391 = Const 5 * x390; + Tbase (Syntax.TWord 8) x392 = x389 + x391; + Tbase (Syntax.TWord 8) x393 = x17 * x381; + Tbase (Syntax.TWord 8) x394 = x19 * x379; + Tbase (Syntax.TWord 8) x395 = x18 * x380; + Tbase (Syntax.TWord 8) x396 = x394 + x395; + Tbase (Syntax.TWord 8) x397 = Const 5 * x396; + Tbase (Syntax.TWord 8) x398 = x393 + x397; + uint128_t x399 = (uint128_t) (x398 >> Const 85); + Tbase (Syntax.TWord 8) x400 = x399 + x392; + uint128_t x401 = (uint128_t) (x400 >> Const 85); + Tbase (Syntax.TWord 8) x402 = x401 + x386; + uint128_t x403 = (uint128_t) x398 & Const 38685626227668133590597631; + uint128_t x404 = (uint128_t) (x402 >> Const 85); + uint128_t x405 = (uint128_t) Const 5 * x404; + uint128_t x406 = x403 + x405; + uint8_t x407 = (uint8_t) (x406 >> Const 85); + uint128_t x408 = (uint128_t) x400 & Const 38685626227668133590597631; + uint128_t x409 = (uint128_t) x407 + x408; + bool x410 = (bool) (x409 >> Const 85); + uint128_t x411 = (uint128_t) x402 & Const 38685626227668133590597631; + uint128_t x412 = (uint128_t) x410 + x411; + uint128_t x413 = x409 & Const 38685626227668133590597631; + uint128_t x414 = x406 & Const 38685626227668133590597631; + (Return x145, Return x146, Return x147, + (Return x220, Return x221, Return x222), + (Return x334, Return x335, Return x336, + (Return x412, Return x413, Return x414)))) + (x, x0, (x1, x2), (x3, x4)) in + y in + x5, +let (_, y) := + let (_, y) := + Eta.InterpEta + (fun var : Syntax.base_type -> Type => + λ + '(x14, x15, x13, (x18, x19, x17), (x24, x25, x23, (x28, x29, x27)), + (x34, x35, x33, (x38, x39, x37)))%core, + uint128_t x40 = x24 + x28; + uint128_t x41 = x25 + x29; + uint128_t x42 = x23 + x27; + uint128_t x43 = Const 77371252455336267181195262 + x24; + uint128_t x44 = x43 - x28; + uint128_t x45 = Const 77371252455336267181195262 + x25; + uint128_t x46 = x45 - x29; + uint128_t x47 = Const 77371252455336267181195254 + x23; + uint128_t x48 = x47 - x27; + Tbase (Syntax.TWord 8) x49 = x42 * x40; + Tbase (Syntax.TWord 8) x50 = x41 * x41; + Tbase (Syntax.TWord 8) x51 = x40 * x42; + Tbase (Syntax.TWord 8) x52 = x50 + x51; + Tbase (Syntax.TWord 8) x53 = x49 + x52; + Tbase (Syntax.TWord 8) x54 = x42 * x41; + Tbase (Syntax.TWord 8) x55 = x41 * x42; + Tbase (Syntax.TWord 8) x56 = x54 + x55; + Tbase (Syntax.TWord 8) x57 = x40 * x40; + Tbase (Syntax.TWord 8) x58 = Const 5 * x57; + Tbase (Syntax.TWord 8) x59 = x56 + x58; + Tbase (Syntax.TWord 8) x60 = x42 * x42; + Tbase (Syntax.TWord 8) x61 = x41 * x40; + Tbase (Syntax.TWord 8) x62 = x40 * x41; + Tbase (Syntax.TWord 8) x63 = x61 + x62; + Tbase (Syntax.TWord 8) x64 = Const 5 * x63; + Tbase (Syntax.TWord 8) x65 = x60 + x64; + uint128_t x66 = (uint128_t) (x65 >> Const 85); + Tbase (Syntax.TWord 8) x67 = x66 + x59; + uint128_t x68 = (uint128_t) (x67 >> Const 85); + Tbase (Syntax.TWord 8) x69 = x68 + x53; + uint128_t x70 = (uint128_t) x65 & Const 38685626227668133590597631; + uint128_t x71 = (uint128_t) (x69 >> Const 85); + uint128_t x72 = (uint128_t) Const 5 * x71; + uint128_t x73 = x70 + x72; + uint8_t x74 = (uint8_t) (x73 >> Const 85); + uint128_t x75 = (uint128_t) x67 & Const 38685626227668133590597631; + uint128_t x76 = (uint128_t) x74 + x75; + bool x77 = (bool) (x76 >> Const 85); + uint128_t x78 = (uint128_t) x69 & Const 38685626227668133590597631; + uint128_t x79 = (uint128_t) x77 + x78; + uint128_t x80 = x76 & Const 38685626227668133590597631; + uint128_t x81 = x73 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x82 = x48 * x44; + Tbase (Syntax.TWord 8) x83 = x46 * x46; + Tbase (Syntax.TWord 8) x84 = x44 * x48; + Tbase (Syntax.TWord 8) x85 = x83 + x84; + Tbase (Syntax.TWord 8) x86 = x82 + x85; + Tbase (Syntax.TWord 8) x87 = x48 * x46; + Tbase (Syntax.TWord 8) x88 = x46 * x48; + Tbase (Syntax.TWord 8) x89 = x87 + x88; + Tbase (Syntax.TWord 8) x90 = x44 * x44; + Tbase (Syntax.TWord 8) x91 = Const 5 * x90; + Tbase (Syntax.TWord 8) x92 = x89 + x91; + Tbase (Syntax.TWord 8) x93 = x48 * x48; + Tbase (Syntax.TWord 8) x94 = x46 * x44; + Tbase (Syntax.TWord 8) x95 = x44 * x46; + Tbase (Syntax.TWord 8) x96 = x94 + x95; + Tbase (Syntax.TWord 8) x97 = Const 5 * x96; + Tbase (Syntax.TWord 8) x98 = x93 + x97; + uint128_t x99 = (uint128_t) (x98 >> Const 85); + Tbase (Syntax.TWord 8) x100 = x99 + x92; + uint128_t x101 = (uint128_t) (x100 >> Const 85); + Tbase (Syntax.TWord 8) x102 = x101 + x86; + uint128_t x103 = (uint128_t) x98 & Const 38685626227668133590597631; + uint128_t x104 = (uint128_t) (x102 >> Const 85); + uint128_t x105 = (uint128_t) Const 5 * x104; + uint128_t x106 = x103 + x105; + uint8_t x107 = (uint8_t) (x106 >> Const 85); + uint128_t x108 = (uint128_t) x100 & Const 38685626227668133590597631; + uint128_t x109 = (uint128_t) x107 + x108; + bool x110 = (bool) (x109 >> Const 85); + uint128_t x111 = (uint128_t) x102 & Const 38685626227668133590597631; + uint128_t x112 = (uint128_t) x110 + x111; + uint128_t x113 = x109 & Const 38685626227668133590597631; + uint128_t x114 = x106 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x115 = x81 * x112; + Tbase (Syntax.TWord 8) x116 = x80 * x113; + Tbase (Syntax.TWord 8) x117 = x79 * x114; + Tbase (Syntax.TWord 8) x118 = x116 + x117; + Tbase (Syntax.TWord 8) x119 = x115 + x118; + Tbase (Syntax.TWord 8) x120 = x81 * x113; + Tbase (Syntax.TWord 8) x121 = x80 * x114; + Tbase (Syntax.TWord 8) x122 = x120 + x121; + Tbase (Syntax.TWord 8) x123 = x79 * x112; + Tbase (Syntax.TWord 8) x124 = Const 5 * x123; + Tbase (Syntax.TWord 8) x125 = x122 + x124; + Tbase (Syntax.TWord 8) x126 = x81 * x114; + Tbase (Syntax.TWord 8) x127 = x80 * x112; + Tbase (Syntax.TWord 8) x128 = x79 * x113; + Tbase (Syntax.TWord 8) x129 = x127 + x128; + Tbase (Syntax.TWord 8) x130 = Const 5 * x129; + Tbase (Syntax.TWord 8) x131 = x126 + x130; + uint128_t x132 = (uint128_t) (x131 >> Const 85); + Tbase (Syntax.TWord 8) x133 = x132 + x125; + uint128_t x134 = (uint128_t) (x133 >> Const 85); + Tbase (Syntax.TWord 8) x135 = x134 + x119; + uint128_t x136 = (uint128_t) x131 & Const 38685626227668133590597631; + uint128_t x137 = (uint128_t) (x135 >> Const 85); + uint128_t x138 = (uint128_t) Const 5 * x137; + uint128_t x139 = x136 + x138; + uint8_t x140 = (uint8_t) (x139 >> Const 85); + uint128_t x141 = (uint128_t) x133 & Const 38685626227668133590597631; + uint128_t x142 = (uint128_t) x140 + x141; + bool x143 = (bool) (x142 >> Const 85); + uint128_t x144 = (uint128_t) x135 & Const 38685626227668133590597631; + uint128_t x145 = (uint128_t) x143 + x144; + uint128_t x146 = x142 & Const 38685626227668133590597631; + uint128_t x147 = x139 & Const 38685626227668133590597631; + uint128_t x148 = Const 77371252455336267181195262 + x79; + uint128_t x149 = x148 - x112; + uint128_t x150 = Const 77371252455336267181195262 + x80; + uint128_t x151 = x150 - x113; + uint128_t x152 = Const 77371252455336267181195254 + x81; + uint128_t x153 = x152 - x114; + Tbase (Syntax.TWord 8) x154 = x13 * x149; + Tbase (Syntax.TWord 8) x155 = x15 * x151; + Tbase (Syntax.TWord 8) x156 = x14 * x153; + Tbase (Syntax.TWord 8) x157 = x155 + x156; + Tbase (Syntax.TWord 8) x158 = x154 + x157; + Tbase (Syntax.TWord 8) x159 = x13 * x151; + Tbase (Syntax.TWord 8) x160 = x15 * x153; + Tbase (Syntax.TWord 8) x161 = x159 + x160; + Tbase (Syntax.TWord 8) x162 = x14 * x149; + Tbase (Syntax.TWord 8) x163 = Const 5 * x162; + Tbase (Syntax.TWord 8) x164 = x161 + x163; + Tbase (Syntax.TWord 8) x165 = x13 * x153; + Tbase (Syntax.TWord 8) x166 = x15 * x149; + Tbase (Syntax.TWord 8) x167 = x14 * x151; + Tbase (Syntax.TWord 8) x168 = x166 + x167; + Tbase (Syntax.TWord 8) x169 = Const 5 * x168; + Tbase (Syntax.TWord 8) x170 = x165 + x169; + uint128_t x171 = (uint128_t) (x170 >> Const 85); + Tbase (Syntax.TWord 8) x172 = x171 + x164; + uint128_t x173 = (uint128_t) (x172 >> Const 85); + Tbase (Syntax.TWord 8) x174 = x173 + x158; + uint128_t x175 = (uint128_t) x170 & Const 38685626227668133590597631; + uint128_t x176 = (uint128_t) (x174 >> Const 85); + uint128_t x177 = (uint128_t) Const 5 * x176; + uint128_t x178 = x175 + x177; + uint8_t x179 = (uint8_t) (x178 >> Const 85); + uint128_t x180 = (uint128_t) x172 & Const 38685626227668133590597631; + uint128_t x181 = (uint128_t) x179 + x180; + bool x182 = (bool) (x181 >> Const 85); + uint128_t x183 = (uint128_t) x174 & Const 38685626227668133590597631; + uint128_t x184 = (uint128_t) x182 + x183; + uint128_t x185 = x181 & Const 38685626227668133590597631; + uint128_t x186 = x178 & Const 38685626227668133590597631; + uint128_t x187 = x79 + x184; + uint128_t x188 = x80 + x185; + uint128_t x189 = x81 + x186; + Tbase (Syntax.TWord 8) x190 = x153 * x187; + Tbase (Syntax.TWord 8) x191 = x151 * x188; + Tbase (Syntax.TWord 8) x192 = x149 * x189; + Tbase (Syntax.TWord 8) x193 = x191 + x192; + Tbase (Syntax.TWord 8) x194 = x190 + x193; + Tbase (Syntax.TWord 8) x195 = x153 * x188; + Tbase (Syntax.TWord 8) x196 = x151 * x189; + Tbase (Syntax.TWord 8) x197 = x195 + x196; + Tbase (Syntax.TWord 8) x198 = x149 * x187; + Tbase (Syntax.TWord 8) x199 = Const 5 * x198; + Tbase (Syntax.TWord 8) x200 = x197 + x199; + Tbase (Syntax.TWord 8) x201 = x153 * x189; + Tbase (Syntax.TWord 8) x202 = x151 * x187; + Tbase (Syntax.TWord 8) x203 = x149 * x188; + Tbase (Syntax.TWord 8) x204 = x202 + x203; + Tbase (Syntax.TWord 8) x205 = Const 5 * x204; + Tbase (Syntax.TWord 8) x206 = x201 + x205; + uint128_t x207 = (uint128_t) (x206 >> Const 85); + Tbase (Syntax.TWord 8) x208 = x207 + x200; + uint128_t x209 = (uint128_t) (x208 >> Const 85); + Tbase (Syntax.TWord 8) x210 = x209 + x194; + uint128_t x211 = (uint128_t) x206 & Const 38685626227668133590597631; + uint128_t x212 = (uint128_t) (x210 >> Const 85); + uint128_t x213 = (uint128_t) Const 5 * x212; + uint128_t x214 = x211 + x213; + uint8_t x215 = (uint8_t) (x214 >> Const 85); + uint128_t x216 = (uint128_t) x208 & Const 38685626227668133590597631; + uint128_t x217 = (uint128_t) x215 + x216; + bool x218 = (bool) (x217 >> Const 85); + uint128_t x219 = (uint128_t) x210 & Const 38685626227668133590597631; + uint128_t x220 = (uint128_t) x218 + x219; + uint128_t x221 = x217 & Const 38685626227668133590597631; + uint128_t x222 = x214 & Const 38685626227668133590597631; + uint128_t x223 = x34 + x38; + uint128_t x224 = x35 + x39; + uint128_t x225 = x33 + x37; + uint128_t x226 = Const 77371252455336267181195262 + x34; + uint128_t x227 = x226 - x38; + uint128_t x228 = Const 77371252455336267181195262 + x35; + uint128_t x229 = x228 - x39; + uint128_t x230 = Const 77371252455336267181195254 + x33; + uint128_t x231 = x230 - x37; + Tbase (Syntax.TWord 8) x232 = x225 * x44; + Tbase (Syntax.TWord 8) x233 = x224 * x46; + Tbase (Syntax.TWord 8) x234 = x223 * x48; + Tbase (Syntax.TWord 8) x235 = x233 + x234; + Tbase (Syntax.TWord 8) x236 = x232 + x235; + Tbase (Syntax.TWord 8) x237 = x225 * x46; + Tbase (Syntax.TWord 8) x238 = x224 * x48; + Tbase (Syntax.TWord 8) x239 = x237 + x238; + Tbase (Syntax.TWord 8) x240 = x223 * x44; + Tbase (Syntax.TWord 8) x241 = Const 5 * x240; + Tbase (Syntax.TWord 8) x242 = x239 + x241; + Tbase (Syntax.TWord 8) x243 = x225 * x48; + Tbase (Syntax.TWord 8) x244 = x224 * x44; + Tbase (Syntax.TWord 8) x245 = x223 * x46; + Tbase (Syntax.TWord 8) x246 = x244 + x245; + Tbase (Syntax.TWord 8) x247 = Const 5 * x246; + Tbase (Syntax.TWord 8) x248 = x243 + x247; + uint128_t x249 = (uint128_t) (x248 >> Const 85); + Tbase (Syntax.TWord 8) x250 = x249 + x242; + uint128_t x251 = (uint128_t) (x250 >> Const 85); + Tbase (Syntax.TWord 8) x252 = x251 + x236; + uint128_t x253 = (uint128_t) x248 & Const 38685626227668133590597631; + uint128_t x254 = (uint128_t) (x252 >> Const 85); + uint128_t x255 = (uint128_t) Const 5 * x254; + uint128_t x256 = x253 + x255; + uint8_t x257 = (uint8_t) (x256 >> Const 85); + uint128_t x258 = (uint128_t) x250 & Const 38685626227668133590597631; + uint128_t x259 = (uint128_t) x257 + x258; + bool x260 = (bool) (x259 >> Const 85); + uint128_t x261 = (uint128_t) x252 & Const 38685626227668133590597631; + uint128_t x262 = (uint128_t) x260 + x261; + uint128_t x263 = x259 & Const 38685626227668133590597631; + uint128_t x264 = x256 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x265 = x231 * x40; + Tbase (Syntax.TWord 8) x266 = x229 * x41; + Tbase (Syntax.TWord 8) x267 = x227 * x42; + Tbase (Syntax.TWord 8) x268 = x266 + x267; + Tbase (Syntax.TWord 8) x269 = x265 + x268; + Tbase (Syntax.TWord 8) x270 = x231 * x41; + Tbase (Syntax.TWord 8) x271 = x229 * x42; + Tbase (Syntax.TWord 8) x272 = x270 + x271; + Tbase (Syntax.TWord 8) x273 = x227 * x40; + Tbase (Syntax.TWord 8) x274 = Const 5 * x273; + Tbase (Syntax.TWord 8) x275 = x272 + x274; + Tbase (Syntax.TWord 8) x276 = x231 * x42; + Tbase (Syntax.TWord 8) x277 = x229 * x40; + Tbase (Syntax.TWord 8) x278 = x227 * x41; + Tbase (Syntax.TWord 8) x279 = x277 + x278; + Tbase (Syntax.TWord 8) x280 = Const 5 * x279; + Tbase (Syntax.TWord 8) x281 = x276 + x280; + uint128_t x282 = (uint128_t) (x281 >> Const 85); + Tbase (Syntax.TWord 8) x283 = x282 + x275; + uint128_t x284 = (uint128_t) (x283 >> Const 85); + Tbase (Syntax.TWord 8) x285 = x284 + x269; + uint128_t x286 = (uint128_t) x281 & Const 38685626227668133590597631; + uint128_t x287 = (uint128_t) (x285 >> Const 85); + uint128_t x288 = (uint128_t) Const 5 * x287; + uint128_t x289 = x286 + x288; + uint8_t x290 = (uint8_t) (x289 >> Const 85); + uint128_t x291 = (uint128_t) x283 & Const 38685626227668133590597631; + uint128_t x292 = (uint128_t) x290 + x291; + bool x293 = (bool) (x292 >> Const 85); + uint128_t x294 = (uint128_t) x285 & Const 38685626227668133590597631; + uint128_t x295 = (uint128_t) x293 + x294; + uint128_t x296 = x292 & Const 38685626227668133590597631; + uint128_t x297 = x289 & Const 38685626227668133590597631; + uint128_t x298 = x295 + x262; + uint128_t x299 = x296 + x263; + uint128_t x300 = x297 + x264; + uint128_t x301 = x295 + x262; + uint128_t x302 = x296 + x263; + uint128_t x303 = x297 + x264; + Tbase (Syntax.TWord 8) x304 = x300 * x301; + Tbase (Syntax.TWord 8) x305 = x299 * x302; + Tbase (Syntax.TWord 8) x306 = x298 * x303; + Tbase (Syntax.TWord 8) x307 = x305 + x306; + Tbase (Syntax.TWord 8) x308 = x304 + x307; + Tbase (Syntax.TWord 8) x309 = x300 * x302; + Tbase (Syntax.TWord 8) x310 = x299 * x303; + Tbase (Syntax.TWord 8) x311 = x309 + x310; + Tbase (Syntax.TWord 8) x312 = x298 * x301; + Tbase (Syntax.TWord 8) x313 = Const 5 * x312; + Tbase (Syntax.TWord 8) x314 = x311 + x313; + Tbase (Syntax.TWord 8) x315 = x300 * x303; + Tbase (Syntax.TWord 8) x316 = x299 * x301; + Tbase (Syntax.TWord 8) x317 = x298 * x302; + Tbase (Syntax.TWord 8) x318 = x316 + x317; + Tbase (Syntax.TWord 8) x319 = Const 5 * x318; + Tbase (Syntax.TWord 8) x320 = x315 + x319; + uint128_t x321 = (uint128_t) (x320 >> Const 85); + Tbase (Syntax.TWord 8) x322 = x321 + x314; + uint128_t x323 = (uint128_t) (x322 >> Const 85); + Tbase (Syntax.TWord 8) x324 = x323 + x308; + uint128_t x325 = (uint128_t) x320 & Const 38685626227668133590597631; + uint128_t x326 = (uint128_t) (x324 >> Const 85); + uint128_t x327 = (uint128_t) Const 5 * x326; + uint128_t x328 = x325 + x327; + uint8_t x329 = (uint8_t) (x328 >> Const 85); + uint128_t x330 = (uint128_t) x322 & Const 38685626227668133590597631; + uint128_t x331 = (uint128_t) x329 + x330; + bool x332 = (bool) (x331 >> Const 85); + uint128_t x333 = (uint128_t) x324 & Const 38685626227668133590597631; + uint128_t x334 = (uint128_t) x332 + x333; + uint128_t x335 = x331 & Const 38685626227668133590597631; + uint128_t x336 = x328 & Const 38685626227668133590597631; + uint128_t x337 = Const 77371252455336267181195262 + x295; + uint128_t x338 = x337 - x262; + uint128_t x339 = Const 77371252455336267181195262 + x296; + uint128_t x340 = x339 - x263; + uint128_t x341 = Const 77371252455336267181195254 + x297; + uint128_t x342 = x341 - x264; + uint128_t x343 = Const 77371252455336267181195262 + x295; + uint128_t x344 = x343 - x262; + uint128_t x345 = Const 77371252455336267181195262 + x296; + uint128_t x346 = x345 - x263; + uint128_t x347 = Const 77371252455336267181195254 + x297; + uint128_t x348 = x347 - x264; + Tbase (Syntax.TWord 8) x349 = x342 * x344; + Tbase (Syntax.TWord 8) x350 = x340 * x346; + Tbase (Syntax.TWord 8) x351 = x338 * x348; + Tbase (Syntax.TWord 8) x352 = x350 + x351; + Tbase (Syntax.TWord 8) x353 = x349 + x352; + Tbase (Syntax.TWord 8) x354 = x342 * x346; + Tbase (Syntax.TWord 8) x355 = x340 * x348; + Tbase (Syntax.TWord 8) x356 = x354 + x355; + Tbase (Syntax.TWord 8) x357 = x338 * x344; + Tbase (Syntax.TWord 8) x358 = Const 5 * x357; + Tbase (Syntax.TWord 8) x359 = x356 + x358; + Tbase (Syntax.TWord 8) x360 = x342 * x348; + Tbase (Syntax.TWord 8) x361 = x340 * x344; + Tbase (Syntax.TWord 8) x362 = x338 * x346; + Tbase (Syntax.TWord 8) x363 = x361 + x362; + Tbase (Syntax.TWord 8) x364 = Const 5 * x363; + Tbase (Syntax.TWord 8) x365 = x360 + x364; + uint128_t x366 = (uint128_t) (x365 >> Const 85); + Tbase (Syntax.TWord 8) x367 = x366 + x359; + uint128_t x368 = (uint128_t) (x367 >> Const 85); + Tbase (Syntax.TWord 8) x369 = x368 + x353; + uint128_t x370 = (uint128_t) x365 & Const 38685626227668133590597631; + uint128_t x371 = (uint128_t) (x369 >> Const 85); + uint128_t x372 = (uint128_t) Const 5 * x371; + uint128_t x373 = x370 + x372; + uint8_t x374 = (uint8_t) (x373 >> Const 85); + uint128_t x375 = (uint128_t) x367 & Const 38685626227668133590597631; + uint128_t x376 = (uint128_t) x374 + x375; + bool x377 = (bool) (x376 >> Const 85); + uint128_t x378 = (uint128_t) x369 & Const 38685626227668133590597631; + uint128_t x379 = (uint128_t) x377 + x378; + uint128_t x380 = x376 & Const 38685626227668133590597631; + uint128_t x381 = x373 & Const 38685626227668133590597631; + Tbase (Syntax.TWord 8) x382 = x17 * x379; + Tbase (Syntax.TWord 8) x383 = x19 * x380; + Tbase (Syntax.TWord 8) x384 = x18 * x381; + Tbase (Syntax.TWord 8) x385 = x383 + x384; + Tbase (Syntax.TWord 8) x386 = x382 + x385; + Tbase (Syntax.TWord 8) x387 = x17 * x380; + Tbase (Syntax.TWord 8) x388 = x19 * x381; + Tbase (Syntax.TWord 8) x389 = x387 + x388; + Tbase (Syntax.TWord 8) x390 = x18 * x379; + Tbase (Syntax.TWord 8) x391 = Const 5 * x390; + Tbase (Syntax.TWord 8) x392 = x389 + x391; + Tbase (Syntax.TWord 8) x393 = x17 * x381; + Tbase (Syntax.TWord 8) x394 = x19 * x379; + Tbase (Syntax.TWord 8) x395 = x18 * x380; + Tbase (Syntax.TWord 8) x396 = x394 + x395; + Tbase (Syntax.TWord 8) x397 = Const 5 * x396; + Tbase (Syntax.TWord 8) x398 = x393 + x397; + uint128_t x399 = (uint128_t) (x398 >> Const 85); + Tbase (Syntax.TWord 8) x400 = x399 + x392; + uint128_t x401 = (uint128_t) (x400 >> Const 85); + Tbase (Syntax.TWord 8) x402 = x401 + x386; + uint128_t x403 = (uint128_t) x398 & Const 38685626227668133590597631; + uint128_t x404 = (uint128_t) (x402 >> Const 85); + uint128_t x405 = (uint128_t) Const 5 * x404; + uint128_t x406 = x403 + x405; + uint8_t x407 = (uint8_t) (x406 >> Const 85); + uint128_t x408 = (uint128_t) x400 & Const 38685626227668133590597631; + uint128_t x409 = (uint128_t) x407 + x408; + bool x410 = (bool) (x409 >> Const 85); + uint128_t x411 = (uint128_t) x402 & Const 38685626227668133590597631; + uint128_t x412 = (uint128_t) x410 + x411; + uint128_t x413 = x409 & Const 38685626227668133590597631; + uint128_t x414 = x406 & Const 38685626227668133590597631; + (Return x145, Return x146, Return x147, + (Return x220, Return x221, Return x222), + (Return x334, Return x335, Return x336, + (Return x412, Return x413, Return x414)))) + (x, x0, (x1, x2), (x3, x4)) in + y in +y))%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 * (word128 * word128 * word128)) -- cgit v1.2.3