1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
|
λ 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;
uint128_t x37 = x36 - x21;
uint128_t x38 = 0x3ffffffffffffffffffffeL + x18;
uint128_t x39 = x38 - x22;
uint128_t x40 = 0x3ffffffffffffffffffff6L + x16;
uint128_t x41 = x40 - x20;
uint256_t x42 = (uint256_t) x35 * (uint256_t) x33;
uint256_t x43 = (uint256_t) x34 * (uint256_t) x34;
uint256_t x44 = (uint256_t) x33 * (uint256_t) x35;
uint256_t x45 = x43 + x44;
uint256_t x46 = x42 + x45;
uint256_t x47 = (uint256_t) x35 * (uint256_t) x34;
uint256_t x48 = (uint256_t) x34 * (uint256_t) x35;
uint256_t x49 = x47 + x48;
uint256_t x50 = (uint256_t) x33 * (uint256_t) x33;
uint256_t x51 = (uint256_t) 0x5 * x50;
uint256_t x52 = x49 + x51;
uint256_t x53 = (uint256_t) x35 * (uint256_t) x35;
uint256_t x54 = (uint256_t) x34 * (uint256_t) x33;
uint256_t x55 = (uint256_t) x33 * (uint256_t) x34;
uint256_t x56 = x54 + x55;
uint256_t x57 = (uint256_t) 0x5 * x56;
uint256_t x58 = x53 + x57;
uint128_t x59 = (uint128_t) (x58 >> 0x55);
uint256_t x60 = (uint256_t) x59 + x52;
uint128_t x61 = (uint128_t) (x60 >> 0x55);
uint256_t x62 = (uint256_t) x61 + x46;
uint128_t x63 = (uint128_t) x58 & 0x1fffffffffffffffffffffL;
uint128_t x64 = (uint128_t) (x62 >> 0x55);
uint128_t x65 = 0x5 * x64;
uint128_t x66 = x63 + x65;
uint128_t x67 = (uint128_t) (x66 >> 0x55);
uint128_t x68 = (uint128_t) x60 & 0x1fffffffffffffffffffffL;
uint128_t x69 = x67 + x68;
uint128_t x70 = (uint128_t) (x69 >> 0x55);
uint128_t x71 = (uint128_t) x62 & 0x1fffffffffffffffffffffL;
uint128_t x72 = x70 + x71;
uint128_t x73 = x69 & 0x1fffffffffffffffffffffL;
uint128_t x74 = x66 & 0x1fffffffffffffffffffffL;
uint256_t x75 = (uint256_t) x41 * (uint256_t) x37;
uint256_t x76 = (uint256_t) x39 * (uint256_t) x39;
uint256_t x77 = (uint256_t) x37 * (uint256_t) x41;
uint256_t x78 = x76 + x77;
uint256_t x79 = x75 + x78;
uint256_t x80 = (uint256_t) x41 * (uint256_t) x39;
uint256_t x81 = (uint256_t) x39 * (uint256_t) x41;
uint256_t x82 = x80 + x81;
uint256_t x83 = (uint256_t) x37 * (uint256_t) x37;
uint256_t x84 = (uint256_t) 0x5 * x83;
uint256_t x85 = x82 + x84;
uint256_t x86 = (uint256_t) x41 * (uint256_t) x41;
uint256_t x87 = (uint256_t) x39 * (uint256_t) x37;
uint256_t x88 = (uint256_t) x37 * (uint256_t) x39;
uint256_t x89 = x87 + x88;
uint256_t x90 = (uint256_t) 0x5 * x89;
uint256_t x91 = x86 + x90;
uint128_t x92 = (uint128_t) (x91 >> 0x55);
uint256_t x93 = (uint256_t) x92 + x85;
uint128_t x94 = (uint128_t) (x93 >> 0x55);
uint256_t x95 = (uint256_t) x94 + x79;
uint128_t x96 = (uint128_t) x91 & 0x1fffffffffffffffffffffL;
uint128_t x97 = (uint128_t) (x95 >> 0x55);
uint128_t x98 = 0x5 * x97;
uint128_t x99 = x96 + x98;
uint128_t x100 = (uint128_t) (x99 >> 0x55);
uint128_t x101 = (uint128_t) x93 & 0x1fffffffffffffffffffffL;
uint128_t x102 = x100 + x101;
uint128_t x103 = (uint128_t) (x102 >> 0x55);
uint128_t x104 = (uint128_t) x95 & 0x1fffffffffffffffffffffL;
uint128_t x105 = x103 + x104;
uint128_t x106 = x102 & 0x1fffffffffffffffffffffL;
uint128_t x107 = x99 & 0x1fffffffffffffffffffffL;
uint256_t x108 = (uint256_t) x74 * (uint256_t) x105;
uint256_t x109 = (uint256_t) x73 * (uint256_t) x106;
uint256_t x110 = (uint256_t) x72 * (uint256_t) x107;
uint256_t x111 = x109 + x110;
uint256_t x112 = x108 + x111;
uint256_t x113 = (uint256_t) x74 * (uint256_t) x106;
uint256_t x114 = (uint256_t) x73 * (uint256_t) x107;
uint256_t x115 = x113 + x114;
uint256_t x116 = (uint256_t) x72 * (uint256_t) x105;
uint256_t x117 = (uint256_t) 0x5 * x116;
uint256_t x118 = x115 + x117;
uint256_t x119 = (uint256_t) x74 * (uint256_t) x107;
uint256_t x120 = (uint256_t) x73 * (uint256_t) x105;
uint256_t x121 = (uint256_t) x72 * (uint256_t) x106;
uint256_t x122 = x120 + x121;
uint256_t x123 = (uint256_t) 0x5 * x122;
uint256_t x124 = x119 + x123;
uint128_t x125 = (uint128_t) (x124 >> 0x55);
uint256_t x126 = (uint256_t) x125 + x118;
uint128_t x127 = (uint128_t) (x126 >> 0x55);
uint256_t x128 = (uint256_t) x127 + x112;
uint128_t x129 = (uint128_t) x124 & 0x1fffffffffffffffffffffL;
uint128_t x130 = (uint128_t) (x128 >> 0x55);
uint128_t x131 = 0x5 * x130;
uint128_t x132 = x129 + x131;
uint128_t x133 = (uint128_t) (x132 >> 0x55);
uint128_t x134 = (uint128_t) x126 & 0x1fffffffffffffffffffffL;
uint128_t x135 = x133 + x134;
uint128_t x136 = (uint128_t) (x135 >> 0x55);
uint128_t x137 = (uint128_t) x128 & 0x1fffffffffffffffffffffL;
uint128_t x138 = x136 + x137;
uint128_t x139 = x135 & 0x1fffffffffffffffffffffL;
uint128_t x140 = x132 & 0x1fffffffffffffffffffffL;
uint128_t x141 = 0x3ffffffffffffffffffffeL + x72;
uint128_t x142 = x141 - x105;
uint128_t x143 = 0x3ffffffffffffffffffffeL + x73;
uint128_t x144 = x143 - x106;
uint128_t x145 = 0x3ffffffffffffffffffff6L + x74;
uint128_t x146 = x145 - x107;
uint128_t x147 = 0x1db41 * x142;
uint128_t x148 = 0x1db41 * x144;
uint128_t x149 = 0x1db41 * x146;
uint128_t x150 = (uint128_t) (x149 >> 0x55);
uint128_t x151 = x150 + x148;
uint128_t x152 = (uint128_t) (x151 >> 0x55);
uint128_t x153 = x152 + x147;
uint128_t x154 = x149 & 0x1fffffffffffffffffffffL;
uint128_t x155 = (uint128_t) (x153 >> 0x55);
uint128_t x156 = 0x5 * x155;
uint128_t x157 = x154 + x156;
uint128_t x158 = (uint128_t) (x157 >> 0x55);
uint128_t x159 = x151 & 0x1fffffffffffffffffffffL;
uint128_t x160 = x158 + x159;
uint128_t x161 = (uint128_t) (x160 >> 0x55);
uint128_t x162 = x153 & 0x1fffffffffffffffffffffL;
uint128_t x163 = x161 + x162;
uint128_t x164 = x160 & 0x1fffffffffffffffffffffL;
uint128_t x165 = x157 & 0x1fffffffffffffffffffffL;
uint128_t x166 = x72 + x163;
uint128_t x167 = x73 + x164;
uint128_t x168 = x74 + x165;
uint256_t x169 = (uint256_t) x146 * (uint256_t) x166;
uint256_t x170 = (uint256_t) x144 * (uint256_t) x167;
uint256_t x171 = (uint256_t) x142 * (uint256_t) x168;
uint256_t x172 = x170 + x171;
uint256_t x173 = x169 + x172;
uint256_t x174 = (uint256_t) x146 * (uint256_t) x167;
uint256_t x175 = (uint256_t) x144 * (uint256_t) x168;
uint256_t x176 = x174 + x175;
uint256_t x177 = (uint256_t) x142 * (uint256_t) x166;
uint256_t x178 = (uint256_t) 0x5 * x177;
uint256_t x179 = x176 + x178;
uint256_t x180 = (uint256_t) x146 * (uint256_t) x168;
uint256_t x181 = (uint256_t) x144 * (uint256_t) x166;
uint256_t x182 = (uint256_t) x142 * (uint256_t) x167;
uint256_t x183 = x181 + x182;
uint256_t x184 = (uint256_t) 0x5 * x183;
uint256_t x185 = x180 + x184;
uint128_t x186 = (uint128_t) (x185 >> 0x55);
uint256_t x187 = (uint256_t) x186 + x179;
uint128_t x188 = (uint128_t) (x187 >> 0x55);
uint256_t x189 = (uint256_t) x188 + x173;
uint128_t x190 = (uint128_t) x185 & 0x1fffffffffffffffffffffL;
uint128_t x191 = (uint128_t) (x189 >> 0x55);
uint128_t x192 = 0x5 * x191;
uint128_t x193 = x190 + x192;
uint128_t x194 = (uint128_t) (x193 >> 0x55);
uint128_t x195 = (uint128_t) x187 & 0x1fffffffffffffffffffffL;
uint128_t x196 = x194 + x195;
uint128_t x197 = (uint128_t) (x196 >> 0x55);
uint128_t x198 = (uint128_t) x189 & 0x1fffffffffffffffffffffL;
uint128_t x199 = x197 + x198;
uint128_t x200 = x196 & 0x1fffffffffffffffffffffL;
uint128_t x201 = x193 & 0x1fffffffffffffffffffffL;
uint128_t x202 = x27 + x31;
uint128_t x203 = x28 + x32;
uint128_t x204 = x26 + x30;
uint128_t x205 = 0x3ffffffffffffffffffffeL + x27;
uint128_t x206 = x205 - x31;
uint128_t x207 = 0x3ffffffffffffffffffffeL + x28;
uint128_t x208 = x207 - x32;
uint128_t x209 = 0x3ffffffffffffffffffff6L + x26;
uint128_t x210 = x209 - x30;
uint256_t x211 = (uint256_t) x204 * (uint256_t) x37;
uint256_t x212 = (uint256_t) x203 * (uint256_t) x39;
uint256_t x213 = (uint256_t) x202 * (uint256_t) x41;
uint256_t x214 = x212 + x213;
uint256_t x215 = x211 + x214;
uint256_t x216 = (uint256_t) x204 * (uint256_t) x39;
uint256_t x217 = (uint256_t) x203 * (uint256_t) x41;
uint256_t x218 = x216 + x217;
uint256_t x219 = (uint256_t) x202 * (uint256_t) x37;
uint256_t x220 = (uint256_t) 0x5 * x219;
uint256_t x221 = x218 + x220;
uint256_t x222 = (uint256_t) x204 * (uint256_t) x41;
uint256_t x223 = (uint256_t) x203 * (uint256_t) x37;
uint256_t x224 = (uint256_t) x202 * (uint256_t) x39;
uint256_t x225 = x223 + x224;
uint256_t x226 = (uint256_t) 0x5 * x225;
uint256_t x227 = x222 + x226;
uint128_t x228 = (uint128_t) (x227 >> 0x55);
uint256_t x229 = (uint256_t) x228 + x221;
uint128_t x230 = (uint128_t) (x229 >> 0x55);
uint256_t x231 = (uint256_t) x230 + x215;
uint128_t x232 = (uint128_t) x227 & 0x1fffffffffffffffffffffL;
uint128_t x233 = (uint128_t) (x231 >> 0x55);
uint128_t x234 = 0x5 * x233;
uint128_t x235 = x232 + x234;
uint128_t x236 = (uint128_t) (x235 >> 0x55);
uint128_t x237 = (uint128_t) x229 & 0x1fffffffffffffffffffffL;
uint128_t x238 = x236 + x237;
uint128_t x239 = (uint128_t) (x238 >> 0x55);
uint128_t x240 = (uint128_t) x231 & 0x1fffffffffffffffffffffL;
uint128_t x241 = x239 + x240;
uint128_t x242 = x238 & 0x1fffffffffffffffffffffL;
uint128_t x243 = x235 & 0x1fffffffffffffffffffffL;
uint256_t x244 = (uint256_t) x210 * (uint256_t) x33;
uint256_t x245 = (uint256_t) x208 * (uint256_t) x34;
uint256_t x246 = (uint256_t) x206 * (uint256_t) x35;
uint256_t x247 = x245 + x246;
uint256_t x248 = x244 + x247;
uint256_t x249 = (uint256_t) x210 * (uint256_t) x34;
uint256_t x250 = (uint256_t) x208 * (uint256_t) x35;
uint256_t x251 = x249 + x250;
uint256_t x252 = (uint256_t) x206 * (uint256_t) x33;
uint256_t x253 = (uint256_t) 0x5 * x252;
uint256_t x254 = x251 + x253;
uint256_t x255 = (uint256_t) x210 * (uint256_t) x35;
uint256_t x256 = (uint256_t) x208 * (uint256_t) x33;
uint256_t x257 = (uint256_t) x206 * (uint256_t) x34;
uint256_t x258 = x256 + x257;
uint256_t x259 = (uint256_t) 0x5 * x258;
uint256_t x260 = x255 + x259;
uint128_t x261 = (uint128_t) (x260 >> 0x55);
uint256_t x262 = (uint256_t) x261 + x254;
uint128_t x263 = (uint128_t) (x262 >> 0x55);
uint256_t x264 = (uint256_t) x263 + x248;
uint128_t x265 = (uint128_t) x260 & 0x1fffffffffffffffffffffL;
uint128_t x266 = (uint128_t) (x264 >> 0x55);
uint128_t x267 = 0x5 * x266;
uint128_t x268 = x265 + x267;
uint128_t x269 = (uint128_t) (x268 >> 0x55);
uint128_t x270 = (uint128_t) x262 & 0x1fffffffffffffffffffffL;
uint128_t x271 = x269 + x270;
uint128_t x272 = (uint128_t) (x271 >> 0x55);
uint128_t x273 = (uint128_t) x264 & 0x1fffffffffffffffffffffL;
uint128_t x274 = x272 + x273;
uint128_t x275 = x271 & 0x1fffffffffffffffffffffL;
uint128_t x276 = x268 & 0x1fffffffffffffffffffffL;
uint128_t x277 = x274 + x241;
uint128_t x278 = x275 + x242;
uint128_t x279 = x276 + x243;
uint128_t x280 = x274 + x241;
uint128_t x281 = x275 + x242;
uint128_t x282 = x276 + x243;
uint256_t x283 = (uint256_t) x279 * (uint256_t) x280;
uint256_t x284 = (uint256_t) x278 * (uint256_t) x281;
uint256_t x285 = (uint256_t) x277 * (uint256_t) x282;
uint256_t x286 = x284 + x285;
uint256_t x287 = x283 + x286;
uint256_t x288 = (uint256_t) x279 * (uint256_t) x281;
uint256_t x289 = (uint256_t) x278 * (uint256_t) x282;
uint256_t x290 = x288 + x289;
uint256_t x291 = (uint256_t) x277 * (uint256_t) x280;
uint256_t x292 = (uint256_t) 0x5 * x291;
uint256_t x293 = x290 + x292;
uint256_t x294 = (uint256_t) x279 * (uint256_t) x282;
uint256_t x295 = (uint256_t) x278 * (uint256_t) x280;
uint256_t x296 = (uint256_t) x277 * (uint256_t) x281;
uint256_t x297 = x295 + x296;
uint256_t x298 = (uint256_t) 0x5 * x297;
uint256_t x299 = x294 + x298;
uint128_t x300 = (uint128_t) (x299 >> 0x55);
uint256_t x301 = (uint256_t) x300 + x293;
uint128_t x302 = (uint128_t) (x301 >> 0x55);
uint256_t x303 = (uint256_t) x302 + x287;
uint128_t x304 = (uint128_t) x299 & 0x1fffffffffffffffffffffL;
uint128_t x305 = (uint128_t) (x303 >> 0x55);
uint128_t x306 = 0x5 * x305;
uint128_t x307 = x304 + x306;
uint128_t x308 = (uint128_t) (x307 >> 0x55);
uint128_t x309 = (uint128_t) x301 & 0x1fffffffffffffffffffffL;
uint128_t x310 = x308 + x309;
uint128_t x311 = (uint128_t) (x310 >> 0x55);
uint128_t x312 = (uint128_t) x303 & 0x1fffffffffffffffffffffL;
uint128_t x313 = x311 + x312;
uint128_t x314 = x310 & 0x1fffffffffffffffffffffL;
uint128_t x315 = x307 & 0x1fffffffffffffffffffffL;
uint128_t x316 = 0x3ffffffffffffffffffffeL + x274;
uint128_t x317 = x316 - x241;
uint128_t x318 = 0x3ffffffffffffffffffffeL + x275;
uint128_t x319 = x318 - x242;
uint128_t x320 = 0x3ffffffffffffffffffff6L + x276;
uint128_t x321 = x320 - x243;
uint128_t x322 = 0x3ffffffffffffffffffffeL + x274;
uint128_t x323 = x322 - x241;
uint128_t x324 = 0x3ffffffffffffffffffffeL + x275;
uint128_t x325 = x324 - x242;
uint128_t x326 = 0x3ffffffffffffffffffff6L + x276;
uint128_t x327 = x326 - x243;
uint256_t x328 = (uint256_t) x321 * (uint256_t) x323;
uint256_t x329 = (uint256_t) x319 * (uint256_t) x325;
uint256_t x330 = (uint256_t) x317 * (uint256_t) x327;
uint256_t x331 = x329 + x330;
uint256_t x332 = x328 + x331;
uint256_t x333 = (uint256_t) x321 * (uint256_t) x325;
uint256_t x334 = (uint256_t) x319 * (uint256_t) x327;
uint256_t x335 = x333 + x334;
uint256_t x336 = (uint256_t) x317 * (uint256_t) x323;
uint256_t x337 = (uint256_t) 0x5 * x336;
uint256_t x338 = x335 + x337;
uint256_t x339 = (uint256_t) x321 * (uint256_t) x327;
uint256_t x340 = (uint256_t) x319 * (uint256_t) x323;
uint256_t x341 = (uint256_t) x317 * (uint256_t) x325;
uint256_t x342 = x340 + x341;
uint256_t x343 = (uint256_t) 0x5 * x342;
uint256_t x344 = x339 + x343;
uint128_t x345 = (uint128_t) (x344 >> 0x55);
uint256_t x346 = (uint256_t) x345 + x338;
uint128_t x347 = (uint128_t) (x346 >> 0x55);
uint256_t x348 = (uint256_t) x347 + x332;
uint128_t x349 = (uint128_t) x344 & 0x1fffffffffffffffffffffL;
uint128_t x350 = (uint128_t) (x348 >> 0x55);
uint128_t x351 = 0x5 * x350;
uint128_t x352 = x349 + x351;
uint128_t x353 = (uint128_t) (x352 >> 0x55);
uint128_t x354 = (uint128_t) x346 & 0x1fffffffffffffffffffffL;
uint128_t x355 = x353 + x354;
uint128_t x356 = (uint128_t) (x355 >> 0x55);
uint128_t x357 = (uint128_t) x348 & 0x1fffffffffffffffffffffL;
uint128_t x358 = x356 + x357;
uint128_t x359 = x355 & 0x1fffffffffffffffffffffL;
uint128_t x360 = x352 & 0x1fffffffffffffffffffffL;
uint256_t x361 = (uint256_t) x10 * (uint256_t) x358;
uint256_t x362 = (uint256_t) x12 * (uint256_t) x359;
uint256_t x363 = (uint256_t) x11 * (uint256_t) x360;
uint256_t x364 = x362 + x363;
uint256_t x365 = x361 + x364;
uint256_t x366 = (uint256_t) x10 * (uint256_t) x359;
uint256_t x367 = (uint256_t) x12 * (uint256_t) x360;
uint256_t x368 = x366 + x367;
uint256_t x369 = (uint256_t) x11 * (uint256_t) x358;
uint256_t x370 = (uint256_t) 0x5 * x369;
uint256_t x371 = x368 + x370;
uint256_t x372 = (uint256_t) x10 * (uint256_t) x360;
uint256_t x373 = (uint256_t) x12 * (uint256_t) x358;
uint256_t x374 = (uint256_t) x11 * (uint256_t) x359;
uint256_t x375 = x373 + x374;
uint256_t x376 = (uint256_t) 0x5 * x375;
uint256_t x377 = x372 + x376;
uint128_t x378 = (uint128_t) (x377 >> 0x55);
uint256_t x379 = (uint256_t) x378 + x371;
uint128_t x380 = (uint128_t) (x379 >> 0x55);
uint256_t x381 = (uint256_t) x380 + x365;
uint128_t x382 = (uint128_t) x377 & 0x1fffffffffffffffffffffL;
uint128_t x383 = (uint128_t) (x381 >> 0x55);
uint128_t x384 = 0x5 * x383;
uint128_t x385 = x382 + x384;
uint128_t x386 = (uint128_t) (x385 >> 0x55);
uint128_t x387 = (uint128_t) x379 & 0x1fffffffffffffffffffffL;
uint128_t x388 = x386 + x387;
uint128_t x389 = (uint128_t) (x388 >> 0x55);
uint128_t x390 = (uint128_t) x381 & 0x1fffffffffffffffffffffL;
uint128_t x391 = x389 + x390;
uint128_t x392 = x388 & 0x1fffffffffffffffffffffL;
uint128_t x393 = x385 & 0x1fffffffffffffffffffffL;
(Return x138, Return x139, Return x140, (Return x199, Return x200, Return x201), (Return x313, Return x314, Return x315, (Return x391, Return x392, Return x393))))
(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))
|
