cranelift-codegen 0.134.0

;; GENERATED BY `isaspec`. DO NOT EDIT!!!

(attr MInst.VecMisc (tag isaspec_generated))

(spec
    (MInst.VecMisc op rd rn size)
    (provide
        (match
            size
            ((Size8x16)
                (match
                    op
                    ((Cnt)
                        (with
                            (t0
                                t10
                                t100
                                t101
                                t102
                                t103
                                t104
                                t105
                                t106
                                t107
                                t108
                                t109
                                t11
                                t110
                                t111
                                t112
                                t113
                                t114
                                t115
                                t116
                                t117
                                t118
                                t119
                                t12
                                t120
                                t121
                                t122
                                t123
                                t124
                                t125
                                t126
                                t127
                                t128
                                t129
                                t13
                                t130
                                t131
                                t132
                                t133
                                t134
                                t135
                                t136
                                t137
                                t138
                                t139
                                t14
                                t140
                                t141
                                t142
                                t143
                                t144
                                t145
                                t146
                                t147
                                t148
                                t149
                                t15
                                t150
                                t151
                                t152
                                t153
                                t154
                                t155
                                t156
                                t157
                                t158
                                t159
                                t16
                                t160
                                t161
                                t162
                                t163
                                t164
                                t165
                                t166
                                t167
                                t168
                                t169
                                t17
                                t170
                                t171
                                t172
                                t173
                                t174
                                t175
                                t176
                                t177
                                t178
                                t179
                                t18
                                t180
                                t181
                                t182
                                t183
                                t184
                                t185
                                t186
                                t187
                                t188
                                t189
                                t19
                                t190
                                t191
                                t192
                                t193
                                t194
                                t195
                                t196
                                t197
                                t198
                                t199
                                t2
                                t20
                                t200
                                t201
                                t202
                                t203
                                t204
                                t205
                                t206
                                t207
                                t208
                                t209
                                t21
                                t210
                                t211
                                t212
                                t213
                                t214
                                t215
                                t216
                                t217
                                t218
                                t219
                                t22
                                t220
                                t221
                                t222
                                t223
                                t224
                                t225
                                t226
                                t227
                                t228
                                t229
                                t23
                                t230
                                t231
                                t232
                                t233
                                t234
                                t235
                                t236
                                t237
                                t238
                                t239
                                t24
                                t240
                                t241
                                t242
                                t243
                                t244
                                t245
                                t246
                                t247
                                t248
                                t249
                                t25
                                t250
                                t251
                                t252
                                t253
                                t254
                                t255
                                t256
                                t257
                                t258
                                t259
                                t26
                                t260
                                t261
                                t262
                                t263
                                t264
                                t265
                                t266
                                t267
                                t268
                                t269
                                t27
                                t270
                                t271
                                t272
                                t273
                                t274
                                t275
                                t276
                                t277
                                t278
                                t279
                                t28
                                t280
                                t281
                                t282
                                t283
                                t284
                                t285
                                t286
                                t287
                                t288
                                t289
                                t29
                                t290
                                t291
                                t292
                                t293
                                t294
                                t295
                                t296
                                t297
                                t298
                                t299
                                t3
                                t30
                                t300
                                t301
                                t302
                                t303
                                t304
                                t305
                                t306
                                t307
                                t308
                                t309
                                t31
                                t310
                                t311
                                t312
                                t313
                                t314
                                t315
                                t316
                                t317
                                t318
                                t319
                                t32
                                t320
                                t321
                                t322
                                t323
                                t324
                                t325
                                t326
                                t327
                                t328
                                t329
                                t33
                                t330
                                t331
                                t332
                                t333
                                t334
                                t335
                                t336
                                t337
                                t338
                                t339
                                t34
                                t340
                                t341
                                t342
                                t343
                                t344
                                t345
                                t346
                                t347
                                t348
                                t349
                                t35
                                t350
                                t351
                                t352
                                t353
                                t354
                                t355
                                t356
                                t357
                                t358
                                t359
                                t36
                                t360
                                t361
                                t362
                                t363
                                t364
                                t365
                                t366
                                t367
                                t368
                                t369
                                t37
                                t370
                                t371
                                t372
                                t373
                                t374
                                t375
                                t376
                                t377
                                t378
                                t379
                                t38
                                t380
                                t381
                                t382
                                t383
                                t384
                                t385
                                t386
                                t387
                                t388
                                t389
                                t39
                                t390
                                t391
                                t392
                                t393
                                t394
                                t395
                                t396
                                t397
                                t398
                                t399
                                t4
                                t40
                                t400
                                t41
                                t42
                                t43
                                t44
                                t45
                                t46
                                t47
                                t48
                                t49
                                t5
                                t50
                                t51
                                t52
                                t53
                                t54
                                t55
                                t56
                                t57
                                t58
                                t59
                                t6
                                t60
                                t61
                                t62
                                t63
                                t64
                                t65
                                t66
                                t67
                                t68
                                t69
                                t7
                                t70
                                t71
                                t72
                                t73
                                t74
                                t75
                                t76
                                t77
                                t78
                                t79
                                t8
                                t80
                                t81
                                t82
                                t83
                                t84
                                t85
                                t86
                                t87
                                t88
                                t89
                                t9
                                t90
                                t91
                                t92
                                t93
                                t94
                                t95
                                t96
                                t97
                                t98
                                t99
                            )
                            (and
                                (= t0 #x0)
                                (= t2 (= (extract 0 0 rn) #b1))
                                (if t2 (= t3 #x1) true)
                                (= t4 (if t2 t3 t0))
                                (= t5 (= (extract 1 1 rn) #b1))
                                (if t5 (= t6 (bvadd t4 #x1)) true)
                                (= t7 (if t5 t6 t4))
                                (= t8 (= (extract 2 2 rn) #b1))
                                (if t8 (= t9 (bvadd t7 #x1)) true)
                                (= t10 (if t8 t9 t7))
                                (= t11 (= (extract 3 3 rn) #b1))
                                (if t11 (= t12 (bvadd t10 #x1)) true)
                                (= t13 (if t11 t12 t10))
                                (= t14 (= (extract 4 4 rn) #b1))
                                (if t14 (= t15 (bvadd t13 #x1)) true)
                                (= t16 (if t14 t15 t13))
                                (= t17 (= (extract 5 5 rn) #b1))
                                (if t17 (= t18 (bvadd t16 #x1)) true)
                                (= t19 (if t17 t18 t16))
                                (= t20 (= (extract 6 6 rn) #b1))
                                (if t20 (= t21 (bvadd t19 #x1)) true)
                                (= t22 (if t20 t21 t19))
                                (= t23 (= (extract 7 7 rn) #b1))
                                (if t23 (= t24 (bvadd t22 #x1)) true)
                                (= t25 (if t23 t24 t22))
                                (= t26 #x0)
                                (= t27 (= (extract 8 8 rn) #b1))
                                (if t27 (= t28 #x1) true)
                                (= t29 (if t27 t28 t26))
                                (= t30 (= (extract 9 9 rn) #b1))
                                (if t30 (= t31 (bvadd t29 #x1)) true)
                                (= t32 (if t30 t31 t29))
                                (= t33 (= (extract 10 10 rn) #b1))
                                (if t33 (= t34 (bvadd t32 #x1)) true)
                                (= t35 (if t33 t34 t32))
                                (= t36 (= (extract 11 11 rn) #b1))
                                (if t36 (= t37 (bvadd t35 #x1)) true)
                                (= t38 (if t36 t37 t35))
                                (= t39 (= (extract 12 12 rn) #b1))
                                (if t39 (= t40 (bvadd t38 #x1)) true)
                                (= t41 (if t39 t40 t38))
                                (= t42 (= (extract 13 13 rn) #b1))
                                (if t42 (= t43 (bvadd t41 #x1)) true)
                                (= t44 (if t42 t43 t41))
                                (= t45 (= (extract 14 14 rn) #b1))
                                (if t45 (= t46 (bvadd t44 #x1)) true)
                                (= t47 (if t45 t46 t44))
                                (= t48 (= (extract 15 15 rn) #b1))
                                (if t48 (= t49 (bvadd t47 #x1)) true)
                                (= t50 (if t48 t49 t47))
                                (= t51 #x0)
                                (= t52 (= (extract 16 16 rn) #b1))
                                (if t52 (= t53 #x1) true)
                                (= t54 (if t52 t53 t51))
                                (= t55 (= (extract 17 17 rn) #b1))
                                (if t55 (= t56 (bvadd t54 #x1)) true)
                                (= t57 (if t55 t56 t54))
                                (= t58 (= (extract 18 18 rn) #b1))
                                (if t58 (= t59 (bvadd t57 #x1)) true)
                                (= t60 (if t58 t59 t57))
                                (= t61 (= (extract 19 19 rn) #b1))
                                (if t61 (= t62 (bvadd t60 #x1)) true)
                                (= t63 (if t61 t62 t60))
                                (= t64 (= (extract 20 20 rn) #b1))
                                (if t64 (= t65 (bvadd t63 #x1)) true)
                                (= t66 (if t64 t65 t63))
                                (= t67 (= (extract 21 21 rn) #b1))
                                (if t67 (= t68 (bvadd t66 #x1)) true)
                                (= t69 (if t67 t68 t66))
                                (= t70 (= (extract 22 22 rn) #b1))
                                (if t70 (= t71 (bvadd t69 #x1)) true)
                                (= t72 (if t70 t71 t69))
                                (= t73 (= (extract 23 23 rn) #b1))
                                (if t73 (= t74 (bvadd t72 #x1)) true)
                                (= t75 (if t73 t74 t72))
                                (= t76 #x0)
                                (= t77 (= (extract 24 24 rn) #b1))
                                (if t77 (= t78 #x1) true)
                                (= t79 (if t77 t78 t76))
                                (= t80 (= (extract 25 25 rn) #b1))
                                (if t80 (= t81 (bvadd t79 #x1)) true)
                                (= t82 (if t80 t81 t79))
                                (= t83 (= (extract 26 26 rn) #b1))
                                (if t83 (= t84 (bvadd t82 #x1)) true)
                                (= t85 (if t83 t84 t82))
                                (= t86 (= (extract 27 27 rn) #b1))
                                (if t86 (= t87 (bvadd t85 #x1)) true)
                                (= t88 (if t86 t87 t85))
                                (= t89 (= (extract 28 28 rn) #b1))
                                (if t89 (= t90 (bvadd t88 #x1)) true)
                                (= t91 (if t89 t90 t88))
                                (= t92 (= (extract 29 29 rn) #b1))
                                (if t92 (= t93 (bvadd t91 #x1)) true)
                                (= t94 (if t92 t93 t91))
                                (= t95 (= (extract 30 30 rn) #b1))
                                (if t95 (= t96 (bvadd t94 #x1)) true)
                                (= t97 (if t95 t96 t94))
                                (= t98 (= (extract 31 31 rn) #b1))
                                (if t98 (= t99 (bvadd t97 #x1)) true)
                                (= t100 (if t98 t99 t97))
                                (= t101 #x0)
                                (= t102 (= (extract 32 32 rn) #b1))
                                (if t102 (= t103 #x1) true)
                                (= t104 (if t102 t103 t101))
                                (= t105 (= (extract 33 33 rn) #b1))
                                (if t105 (= t106 (bvadd t104 #x1)) true)
                                (= t107 (if t105 t106 t104))
                                (= t108 (= (extract 34 34 rn) #b1))
                                (if t108 (= t109 (bvadd t107 #x1)) true)
                                (= t110 (if t108 t109 t107))
                                (= t111 (= (extract 35 35 rn) #b1))
                                (if t111 (= t112 (bvadd t110 #x1)) true)
                                (= t113 (if t111 t112 t110))
                                (= t114 (= (extract 36 36 rn) #b1))
                                (if t114 (= t115 (bvadd t113 #x1)) true)
                                (= t116 (if t114 t115 t113))
                                (= t117 (= (extract 37 37 rn) #b1))
                                (if t117 (= t118 (bvadd t116 #x1)) true)
                                (= t119 (if t117 t118 t116))
                                (= t120 (= (extract 38 38 rn) #b1))
                                (if t120 (= t121 (bvadd t119 #x1)) true)
                                (= t122 (if t120 t121 t119))
                                (= t123 (= (extract 39 39 rn) #b1))
                                (if t123 (= t124 (bvadd t122 #x1)) true)
                                (= t125 (if t123 t124 t122))
                                (= t126 #x0)
                                (= t127 (= (extract 40 40 rn) #b1))
                                (if t127 (= t128 #x1) true)
                                (= t129 (if t127 t128 t126))
                                (= t130 (= (extract 41 41 rn) #b1))
                                (if t130 (= t131 (bvadd t129 #x1)) true)
                                (= t132 (if t130 t131 t129))
                                (= t133 (= (extract 42 42 rn) #b1))
                                (if t133 (= t134 (bvadd t132 #x1)) true)
                                (= t135 (if t133 t134 t132))
                                (= t136 (= (extract 43 43 rn) #b1))
                                (if t136 (= t137 (bvadd t135 #x1)) true)
                                (= t138 (if t136 t137 t135))
                                (= t139 (= (extract 44 44 rn) #b1))
                                (if t139 (= t140 (bvadd t138 #x1)) true)
                                (= t141 (if t139 t140 t138))
                                (= t142 (= (extract 45 45 rn) #b1))
                                (if t142 (= t143 (bvadd t141 #x1)) true)
                                (= t144 (if t142 t143 t141))
                                (= t145 (= (extract 46 46 rn) #b1))
                                (if t145 (= t146 (bvadd t144 #x1)) true)
                                (= t147 (if t145 t146 t144))
                                (= t148 (= (extract 47 47 rn) #b1))
                                (if t148 (= t149 (bvadd t147 #x1)) true)
                                (= t150 (if t148 t149 t147))
                                (= t151 #x0)
                                (= t152 (= (extract 48 48 rn) #b1))
                                (if t152 (= t153 #x1) true)
                                (= t154 (if t152 t153 t151))
                                (= t155 (= (extract 49 49 rn) #b1))
                                (if t155 (= t156 (bvadd t154 #x1)) true)
                                (= t157 (if t155 t156 t154))
                                (= t158 (= (extract 50 50 rn) #b1))
                                (if t158 (= t159 (bvadd t157 #x1)) true)
                                (= t160 (if t158 t159 t157))
                                (= t161 (= (extract 51 51 rn) #b1))
                                (if t161 (= t162 (bvadd t160 #x1)) true)
                                (= t163 (if t161 t162 t160))
                                (= t164 (= (extract 52 52 rn) #b1))
                                (if t164 (= t165 (bvadd t163 #x1)) true)
                                (= t166 (if t164 t165 t163))
                                (= t167 (= (extract 53 53 rn) #b1))
                                (if t167 (= t168 (bvadd t166 #x1)) true)
                                (= t169 (if t167 t168 t166))
                                (= t170 (= (extract 54 54 rn) #b1))
                                (if t170 (= t171 (bvadd t169 #x1)) true)
                                (= t172 (if t170 t171 t169))
                                (= t173 (= (extract 55 55 rn) #b1))
                                (if t173 (= t174 (bvadd t172 #x1)) true)
                                (= t175 (if t173 t174 t172))
                                (= t176 #x0)
                                (= t177 (= (extract 56 56 rn) #b1))
                                (if t177 (= t178 #x1) true)
                                (= t179 (if t177 t178 t176))
                                (= t180 (= (extract 57 57 rn) #b1))
                                (if t180 (= t181 (bvadd t179 #x1)) true)
                                (= t182 (if t180 t181 t179))
                                (= t183 (= (extract 58 58 rn) #b1))
                                (if t183 (= t184 (bvadd t182 #x1)) true)
                                (= t185 (if t183 t184 t182))
                                (= t186 (= (extract 59 59 rn) #b1))
                                (if t186 (= t187 (bvadd t185 #x1)) true)
                                (= t188 (if t186 t187 t185))
                                (= t189 (= (extract 60 60 rn) #b1))
                                (if t189 (= t190 (bvadd t188 #x1)) true)
                                (= t191 (if t189 t190 t188))
                                (= t192 (= (extract 61 61 rn) #b1))
                                (if t192 (= t193 (bvadd t191 #x1)) true)
                                (= t194 (if t192 t193 t191))
                                (= t195 (= (extract 62 62 rn) #b1))
                                (if t195 (= t196 (bvadd t194 #x1)) true)
                                (= t197 (if t195 t196 t194))
                                (= t198 (= (extract 63 63 rn) #b1))
                                (if t198 (= t199 (bvadd t197 #x1)) true)
                                (= t200 (if t198 t199 t197))
                                (= t201 #x0)
                                (= t202 (= (extract 64 64 rn) #b1))
                                (if t202 (= t203 #x1) true)
                                (= t204 (if t202 t203 t201))
                                (= t205 (= (extract 65 65 rn) #b1))
                                (if t205 (= t206 (bvadd t204 #x1)) true)
                                (= t207 (if t205 t206 t204))
                                (= t208 (= (extract 66 66 rn) #b1))
                                (if t208 (= t209 (bvadd t207 #x1)) true)
                                (= t210 (if t208 t209 t207))
                                (= t211 (= (extract 67 67 rn) #b1))
                                (if t211 (= t212 (bvadd t210 #x1)) true)
                                (= t213 (if t211 t212 t210))
                                (= t214 (= (extract 68 68 rn) #b1))
                                (if t214 (= t215 (bvadd t213 #x1)) true)
                                (= t216 (if t214 t215 t213))
                                (= t217 (= (extract 69 69 rn) #b1))
                                (if t217 (= t218 (bvadd t216 #x1)) true)
                                (= t219 (if t217 t218 t216))
                                (= t220 (= (extract 70 70 rn) #b1))
                                (if t220 (= t221 (bvadd t219 #x1)) true)
                                (= t222 (if t220 t221 t219))
                                (= t223 (= (extract 71 71 rn) #b1))
                                (if t223 (= t224 (bvadd t222 #x1)) true)
                                (= t225 (if t223 t224 t222))
                                (= t226 #x0)
                                (= t227 (= (extract 72 72 rn) #b1))
                                (if t227 (= t228 #x1) true)
                                (= t229 (if t227 t228 t226))
                                (= t230 (= (extract 73 73 rn) #b1))
                                (if t230 (= t231 (bvadd t229 #x1)) true)
                                (= t232 (if t230 t231 t229))
                                (= t233 (= (extract 74 74 rn) #b1))
                                (if t233 (= t234 (bvadd t232 #x1)) true)
                                (= t235 (if t233 t234 t232))
                                (= t236 (= (extract 75 75 rn) #b1))
                                (if t236 (= t237 (bvadd t235 #x1)) true)
                                (= t238 (if t236 t237 t235))
                                (= t239 (= (extract 76 76 rn) #b1))
                                (if t239 (= t240 (bvadd t238 #x1)) true)
                                (= t241 (if t239 t240 t238))
                                (= t242 (= (extract 77 77 rn) #b1))
                                (if t242 (= t243 (bvadd t241 #x1)) true)
                                (= t244 (if t242 t243 t241))
                                (= t245 (= (extract 78 78 rn) #b1))
                                (if t245 (= t246 (bvadd t244 #x1)) true)
                                (= t247 (if t245 t246 t244))
                                (= t248 (= (extract 79 79 rn) #b1))
                                (if t248 (= t249 (bvadd t247 #x1)) true)
                                (= t250 (if t248 t249 t247))
                                (= t251 #x0)
                                (= t252 (= (extract 80 80 rn) #b1))
                                (if t252 (= t253 #x1) true)
                                (= t254 (if t252 t253 t251))
                                (= t255 (= (extract 81 81 rn) #b1))
                                (if t255 (= t256 (bvadd t254 #x1)) true)
                                (= t257 (if t255 t256 t254))
                                (= t258 (= (extract 82 82 rn) #b1))
                                (if t258 (= t259 (bvadd t257 #x1)) true)
                                (= t260 (if t258 t259 t257))
                                (= t261 (= (extract 83 83 rn) #b1))
                                (if t261 (= t262 (bvadd t260 #x1)) true)
                                (= t263 (if t261 t262 t260))
                                (= t264 (= (extract 84 84 rn) #b1))
                                (if t264 (= t265 (bvadd t263 #x1)) true)
                                (= t266 (if t264 t265 t263))
                                (= t267 (= (extract 85 85 rn) #b1))
                                (if t267 (= t268 (bvadd t266 #x1)) true)
                                (= t269 (if t267 t268 t266))
                                (= t270 (= (extract 86 86 rn) #b1))
                                (if t270 (= t271 (bvadd t269 #x1)) true)
                                (= t272 (if t270 t271 t269))
                                (= t273 (= (extract 87 87 rn) #b1))
                                (if t273 (= t274 (bvadd t272 #x1)) true)
                                (= t275 (if t273 t274 t272))
                                (= t276 #x0)
                                (= t277 (= (extract 88 88 rn) #b1))
                                (if t277 (= t278 #x1) true)
                                (= t279 (if t277 t278 t276))
                                (= t280 (= (extract 89 89 rn) #b1))
                                (if t280 (= t281 (bvadd t279 #x1)) true)
                                (= t282 (if t280 t281 t279))
                                (= t283 (= (extract 90 90 rn) #b1))
                                (if t283 (= t284 (bvadd t282 #x1)) true)
                                (= t285 (if t283 t284 t282))
                                (= t286 (= (extract 91 91 rn) #b1))
                                (if t286 (= t287 (bvadd t285 #x1)) true)
                                (= t288 (if t286 t287 t285))
                                (= t289 (= (extract 92 92 rn) #b1))
                                (if t289 (= t290 (bvadd t288 #x1)) true)
                                (= t291 (if t289 t290 t288))
                                (= t292 (= (extract 93 93 rn) #b1))
                                (if t292 (= t293 (bvadd t291 #x1)) true)
                                (= t294 (if t292 t293 t291))
                                (= t295 (= (extract 94 94 rn) #b1))
                                (if t295 (= t296 (bvadd t294 #x1)) true)
                                (= t297 (if t295 t296 t294))
                                (= t298 (= (extract 95 95 rn) #b1))
                                (if t298 (= t299 (bvadd t297 #x1)) true)
                                (= t300 (if t298 t299 t297))
                                (= t301 #x0)
                                (= t302 (= (extract 96 96 rn) #b1))
                                (if t302 (= t303 #x1) true)
                                (= t304 (if t302 t303 t301))
                                (= t305 (= (extract 97 97 rn) #b1))
                                (if t305 (= t306 (bvadd t304 #x1)) true)
                                (= t307 (if t305 t306 t304))
                                (= t308 (= (extract 98 98 rn) #b1))
                                (if t308 (= t309 (bvadd t307 #x1)) true)
                                (= t310 (if t308 t309 t307))
                                (= t311 (= (extract 99 99 rn) #b1))
                                (if t311 (= t312 (bvadd t310 #x1)) true)
                                (= t313 (if t311 t312 t310))
                                (= t314 (= (extract 100 100 rn) #b1))
                                (if t314 (= t315 (bvadd t313 #x1)) true)
                                (= t316 (if t314 t315 t313))
                                (= t317 (= (extract 101 101 rn) #b1))
                                (if t317 (= t318 (bvadd t316 #x1)) true)
                                (= t319 (if t317 t318 t316))
                                (= t320 (= (extract 102 102 rn) #b1))
                                (if t320 (= t321 (bvadd t319 #x1)) true)
                                (= t322 (if t320 t321 t319))
                                (= t323 (= (extract 103 103 rn) #b1))
                                (if t323 (= t324 (bvadd t322 #x1)) true)
                                (= t325 (if t323 t324 t322))
                                (= t326 #x0)
                                (= t327 (= (extract 104 104 rn) #b1))
                                (if t327 (= t328 #x1) true)
                                (= t329 (if t327 t328 t326))
                                (= t330 (= (extract 105 105 rn) #b1))
                                (if t330 (= t331 (bvadd t329 #x1)) true)
                                (= t332 (if t330 t331 t329))
                                (= t333 (= (extract 106 106 rn) #b1))
                                (if t333 (= t334 (bvadd t332 #x1)) true)
                                (= t335 (if t333 t334 t332))
                                (= t336 (= (extract 107 107 rn) #b1))
                                (if t336 (= t337 (bvadd t335 #x1)) true)
                                (= t338 (if t336 t337 t335))
                                (= t339 (= (extract 108 108 rn) #b1))
                                (if t339 (= t340 (bvadd t338 #x1)) true)
                                (= t341 (if t339 t340 t338))
                                (= t342 (= (extract 109 109 rn) #b1))
                                (if t342 (= t343 (bvadd t341 #x1)) true)
                                (= t344 (if t342 t343 t341))
                                (= t345 (= (extract 110 110 rn) #b1))
                                (if t345 (= t346 (bvadd t344 #x1)) true)
                                (= t347 (if t345 t346 t344))
                                (= t348 (= (extract 111 111 rn) #b1))
                                (if t348 (= t349 (bvadd t347 #x1)) true)
                                (= t350 (if t348 t349 t347))
                                (= t351 #x0)
                                (= t352 (= (extract 112 112 rn) #b1))
                                (if t352 (= t353 #x1) true)
                                (= t354 (if t352 t353 t351))
                                (= t355 (= (extract 113 113 rn) #b1))
                                (if t355 (= t356 (bvadd t354 #x1)) true)
                                (= t357 (if t355 t356 t354))
                                (= t358 (= (extract 114 114 rn) #b1))
                                (if t358 (= t359 (bvadd t357 #x1)) true)
                                (= t360 (if t358 t359 t357))
                                (= t361 (= (extract 115 115 rn) #b1))
                                (if t361 (= t362 (bvadd t360 #x1)) true)
                                (= t363 (if t361 t362 t360))
                                (= t364 (= (extract 116 116 rn) #b1))
                                (if t364 (= t365 (bvadd t363 #x1)) true)
                                (= t366 (if t364 t365 t363))
                                (= t367 (= (extract 117 117 rn) #b1))
                                (if t367 (= t368 (bvadd t366 #x1)) true)
                                (= t369 (if t367 t368 t366))
                                (= t370 (= (extract 118 118 rn) #b1))
                                (if t370 (= t371 (bvadd t369 #x1)) true)
                                (= t372 (if t370 t371 t369))
                                (= t373 (= (extract 119 119 rn) #b1))
                                (if t373 (= t374 (bvadd t372 #x1)) true)
                                (= t375 (if t373 t374 t372))
                                (= t376 #x0)
                                (= t377 (= (extract 120 120 rn) #b1))
                                (if t377 (= t378 #x1) true)
                                (= t379 (if t377 t378 t376))
                                (= t380 (= (extract 121 121 rn) #b1))
                                (if t380 (= t381 (bvadd t379 #x1)) true)
                                (= t382 (if t380 t381 t379))
                                (= t383 (= (extract 122 122 rn) #b1))
                                (if t383 (= t384 (bvadd t382 #x1)) true)
                                (= t385 (if t383 t384 t382))
                                (= t386 (= (extract 123 123 rn) #b1))
                                (if t386 (= t387 (bvadd t385 #x1)) true)
                                (= t388 (if t386 t387 t385))
                                (= t389 (= (extract 124 124 rn) #b1))
                                (if t389 (= t390 (bvadd t388 #x1)) true)
                                (= t391 (if t389 t390 t388))
                                (= t392 (= (extract 125 125 rn) #b1))
                                (if t392 (= t393 (bvadd t391 #x1)) true)
                                (= t394 (if t392 t393 t391))
                                (= t395 (= (extract 126 126 rn) #b1))
                                (if t395 (= t396 (bvadd t394 #x1)) true)
                                (= t397 (if t395 t396 t394))
                                (= t398 (= (extract 127 127 rn) #b1))
                                (if t398 (= t399 (bvadd t397 #x1)) true)
                                (= t400 (if t398 t399 t397))
                                (=
                                    rd
                                    (concat
                                        (zero_ext 8 t400)
                                        (concat
                                            (zero_ext 8 t375)
                                            (concat
                                                (zero_ext 8 t350)
                                                (concat
                                                    (zero_ext 8 t325)
                                                    (concat
                                                        (zero_ext 8 t300)
                                                        (concat
                                                            (zero_ext 8 t275)
                                                            (concat
                                                                (zero_ext 8 t250)
                                                                (concat
                                                                    (zero_ext 8 t225)
                                                                    (concat
                                                                        (zero_ext 8 t200)
                                                                        (concat
                                                                            (zero_ext 8 t175)
                                                                            (concat
                                                                                (zero_ext 8 t150)
                                                                                (concat
                                                                                    (zero_ext 8 t125)
                                                                                    (concat (zero_ext 8 t100) (concat (zero_ext 8 t75) (concat (zero_ext 8 t50) (zero_ext 8 t25))))
                                                                                )
                                                                            )
                                                                        )
                                                                    )
                                                                )
                                                            )
                                                        )
                                                    )
                                                )
                                            )
                                        )
                                    )
                                )
                            )
                        )
                    )
                )
            )
            ((Size8x8)
                (match
                    op
                    ((Cnt)
                        (with
                            (t0
                                t10
                                t100
                                t101
                                t102
                                t103
                                t104
                                t105
                                t106
                                t107
                                t108
                                t109
                                t11
                                t110
                                t111
                                t112
                                t113
                                t114
                                t115
                                t116
                                t117
                                t118
                                t119
                                t12
                                t120
                                t121
                                t122
                                t123
                                t124
                                t125
                                t126
                                t127
                                t128
                                t129
                                t13
                                t130
                                t131
                                t132
                                t133
                                t134
                                t135
                                t136
                                t137
                                t138
                                t139
                                t14
                                t140
                                t141
                                t142
                                t143
                                t144
                                t145
                                t146
                                t147
                                t148
                                t149
                                t15
                                t150
                                t151
                                t152
                                t153
                                t154
                                t155
                                t156
                                t157
                                t158
                                t159
                                t16
                                t160
                                t161
                                t162
                                t163
                                t164
                                t165
                                t166
                                t167
                                t168
                                t169
                                t17
                                t170
                                t171
                                t172
                                t173
                                t174
                                t175
                                t176
                                t177
                                t178
                                t179
                                t18
                                t180
                                t181
                                t182
                                t183
                                t184
                                t185
                                t186
                                t187
                                t188
                                t189
                                t19
                                t190
                                t191
                                t192
                                t193
                                t194
                                t195
                                t196
                                t197
                                t198
                                t199
                                t2
                                t20
                                t200
                                t21
                                t22
                                t23
                                t24
                                t25
                                t26
                                t27
                                t28
                                t29
                                t3
                                t30
                                t31
                                t32
                                t33
                                t34
                                t35
                                t36
                                t37
                                t38
                                t39
                                t4
                                t40
                                t41
                                t42
                                t43
                                t44
                                t45
                                t46
                                t47
                                t48
                                t49
                                t5
                                t50
                                t51
                                t52
                                t53
                                t54
                                t55
                                t56
                                t57
                                t58
                                t59
                                t6
                                t60
                                t61
                                t62
                                t63
                                t64
                                t65
                                t66
                                t67
                                t68
                                t69
                                t7
                                t70
                                t71
                                t72
                                t73
                                t74
                                t75
                                t76
                                t77
                                t78
                                t79
                                t8
                                t80
                                t81
                                t82
                                t83
                                t84
                                t85
                                t86
                                t87
                                t88
                                t89
                                t9
                                t90
                                t91
                                t92
                                t93
                                t94
                                t95
                                t96
                                t97
                                t98
                                t99
                            )
                            (and
                                (= t0 #x0)
                                (= t2 (= (extract 0 0 rn) #b1))
                                (if t2 (= t3 #x1) true)
                                (= t4 (if t2 t3 t0))
                                (= t5 (= (extract 1 1 rn) #b1))
                                (if t5 (= t6 (bvadd t4 #x1)) true)
                                (= t7 (if t5 t6 t4))
                                (= t8 (= (extract 2 2 rn) #b1))
                                (if t8 (= t9 (bvadd t7 #x1)) true)
                                (= t10 (if t8 t9 t7))
                                (= t11 (= (extract 3 3 rn) #b1))
                                (if t11 (= t12 (bvadd t10 #x1)) true)
                                (= t13 (if t11 t12 t10))
                                (= t14 (= (extract 4 4 rn) #b1))
                                (if t14 (= t15 (bvadd t13 #x1)) true)
                                (= t16 (if t14 t15 t13))
                                (= t17 (= (extract 5 5 rn) #b1))
                                (if t17 (= t18 (bvadd t16 #x1)) true)
                                (= t19 (if t17 t18 t16))
                                (= t20 (= (extract 6 6 rn) #b1))
                                (if t20 (= t21 (bvadd t19 #x1)) true)
                                (= t22 (if t20 t21 t19))
                                (= t23 (= (extract 7 7 rn) #b1))
                                (if t23 (= t24 (bvadd t22 #x1)) true)
                                (= t25 (if t23 t24 t22))
                                (= t26 #x0)
                                (= t27 (= (extract 8 8 rn) #b1))
                                (if t27 (= t28 #x1) true)
                                (= t29 (if t27 t28 t26))
                                (= t30 (= (extract 9 9 rn) #b1))
                                (if t30 (= t31 (bvadd t29 #x1)) true)
                                (= t32 (if t30 t31 t29))
                                (= t33 (= (extract 10 10 rn) #b1))
                                (if t33 (= t34 (bvadd t32 #x1)) true)
                                (= t35 (if t33 t34 t32))
                                (= t36 (= (extract 11 11 rn) #b1))
                                (if t36 (= t37 (bvadd t35 #x1)) true)
                                (= t38 (if t36 t37 t35))
                                (= t39 (= (extract 12 12 rn) #b1))
                                (if t39 (= t40 (bvadd t38 #x1)) true)
                                (= t41 (if t39 t40 t38))
                                (= t42 (= (extract 13 13 rn) #b1))
                                (if t42 (= t43 (bvadd t41 #x1)) true)
                                (= t44 (if t42 t43 t41))
                                (= t45 (= (extract 14 14 rn) #b1))
                                (if t45 (= t46 (bvadd t44 #x1)) true)
                                (= t47 (if t45 t46 t44))
                                (= t48 (= (extract 15 15 rn) #b1))
                                (if t48 (= t49 (bvadd t47 #x1)) true)
                                (= t50 (if t48 t49 t47))
                                (= t51 #x0)
                                (= t52 (= (extract 16 16 rn) #b1))
                                (if t52 (= t53 #x1) true)
                                (= t54 (if t52 t53 t51))
                                (= t55 (= (extract 17 17 rn) #b1))
                                (if t55 (= t56 (bvadd t54 #x1)) true)
                                (= t57 (if t55 t56 t54))
                                (= t58 (= (extract 18 18 rn) #b1))
                                (if t58 (= t59 (bvadd t57 #x1)) true)
                                (= t60 (if t58 t59 t57))
                                (= t61 (= (extract 19 19 rn) #b1))
                                (if t61 (= t62 (bvadd t60 #x1)) true)
                                (= t63 (if t61 t62 t60))
                                (= t64 (= (extract 20 20 rn) #b1))
                                (if t64 (= t65 (bvadd t63 #x1)) true)
                                (= t66 (if t64 t65 t63))
                                (= t67 (= (extract 21 21 rn) #b1))
                                (if t67 (= t68 (bvadd t66 #x1)) true)
                                (= t69 (if t67 t68 t66))
                                (= t70 (= (extract 22 22 rn) #b1))
                                (if t70 (= t71 (bvadd t69 #x1)) true)
                                (= t72 (if t70 t71 t69))
                                (= t73 (= (extract 23 23 rn) #b1))
                                (if t73 (= t74 (bvadd t72 #x1)) true)
                                (= t75 (if t73 t74 t72))
                                (= t76 #x0)
                                (= t77 (= (extract 24 24 rn) #b1))
                                (if t77 (= t78 #x1) true)
                                (= t79 (if t77 t78 t76))
                                (= t80 (= (extract 25 25 rn) #b1))
                                (if t80 (= t81 (bvadd t79 #x1)) true)
                                (= t82 (if t80 t81 t79))
                                (= t83 (= (extract 26 26 rn) #b1))
                                (if t83 (= t84 (bvadd t82 #x1)) true)
                                (= t85 (if t83 t84 t82))
                                (= t86 (= (extract 27 27 rn) #b1))
                                (if t86 (= t87 (bvadd t85 #x1)) true)
                                (= t88 (if t86 t87 t85))
                                (= t89 (= (extract 28 28 rn) #b1))
                                (if t89 (= t90 (bvadd t88 #x1)) true)
                                (= t91 (if t89 t90 t88))
                                (= t92 (= (extract 29 29 rn) #b1))
                                (if t92 (= t93 (bvadd t91 #x1)) true)
                                (= t94 (if t92 t93 t91))
                                (= t95 (= (extract 30 30 rn) #b1))
                                (if t95 (= t96 (bvadd t94 #x1)) true)
                                (= t97 (if t95 t96 t94))
                                (= t98 (= (extract 31 31 rn) #b1))
                                (if t98 (= t99 (bvadd t97 #x1)) true)
                                (= t100 (if t98 t99 t97))
                                (= t101 #x0)
                                (= t102 (= (extract 32 32 rn) #b1))
                                (if t102 (= t103 #x1) true)
                                (= t104 (if t102 t103 t101))
                                (= t105 (= (extract 33 33 rn) #b1))
                                (if t105 (= t106 (bvadd t104 #x1)) true)
                                (= t107 (if t105 t106 t104))
                                (= t108 (= (extract 34 34 rn) #b1))
                                (if t108 (= t109 (bvadd t107 #x1)) true)
                                (= t110 (if t108 t109 t107))
                                (= t111 (= (extract 35 35 rn) #b1))
                                (if t111 (= t112 (bvadd t110 #x1)) true)
                                (= t113 (if t111 t112 t110))
                                (= t114 (= (extract 36 36 rn) #b1))
                                (if t114 (= t115 (bvadd t113 #x1)) true)
                                (= t116 (if t114 t115 t113))
                                (= t117 (= (extract 37 37 rn) #b1))
                                (if t117 (= t118 (bvadd t116 #x1)) true)
                                (= t119 (if t117 t118 t116))
                                (= t120 (= (extract 38 38 rn) #b1))
                                (if t120 (= t121 (bvadd t119 #x1)) true)
                                (= t122 (if t120 t121 t119))
                                (= t123 (= (extract 39 39 rn) #b1))
                                (if t123 (= t124 (bvadd t122 #x1)) true)
                                (= t125 (if t123 t124 t122))
                                (= t126 #x0)
                                (= t127 (= (extract 40 40 rn) #b1))
                                (if t127 (= t128 #x1) true)
                                (= t129 (if t127 t128 t126))
                                (= t130 (= (extract 41 41 rn) #b1))
                                (if t130 (= t131 (bvadd t129 #x1)) true)
                                (= t132 (if t130 t131 t129))
                                (= t133 (= (extract 42 42 rn) #b1))
                                (if t133 (= t134 (bvadd t132 #x1)) true)
                                (= t135 (if t133 t134 t132))
                                (= t136 (= (extract 43 43 rn) #b1))
                                (if t136 (= t137 (bvadd t135 #x1)) true)
                                (= t138 (if t136 t137 t135))
                                (= t139 (= (extract 44 44 rn) #b1))
                                (if t139 (= t140 (bvadd t138 #x1)) true)
                                (= t141 (if t139 t140 t138))
                                (= t142 (= (extract 45 45 rn) #b1))
                                (if t142 (= t143 (bvadd t141 #x1)) true)
                                (= t144 (if t142 t143 t141))
                                (= t145 (= (extract 46 46 rn) #b1))
                                (if t145 (= t146 (bvadd t144 #x1)) true)
                                (= t147 (if t145 t146 t144))
                                (= t148 (= (extract 47 47 rn) #b1))
                                (if t148 (= t149 (bvadd t147 #x1)) true)
                                (= t150 (if t148 t149 t147))
                                (= t151 #x0)
                                (= t152 (= (extract 48 48 rn) #b1))
                                (if t152 (= t153 #x1) true)
                                (= t154 (if t152 t153 t151))
                                (= t155 (= (extract 49 49 rn) #b1))
                                (if t155 (= t156 (bvadd t154 #x1)) true)
                                (= t157 (if t155 t156 t154))
                                (= t158 (= (extract 50 50 rn) #b1))
                                (if t158 (= t159 (bvadd t157 #x1)) true)
                                (= t160 (if t158 t159 t157))
                                (= t161 (= (extract 51 51 rn) #b1))
                                (if t161 (= t162 (bvadd t160 #x1)) true)
                                (= t163 (if t161 t162 t160))
                                (= t164 (= (extract 52 52 rn) #b1))
                                (if t164 (= t165 (bvadd t163 #x1)) true)
                                (= t166 (if t164 t165 t163))
                                (= t167 (= (extract 53 53 rn) #b1))
                                (if t167 (= t168 (bvadd t166 #x1)) true)
                                (= t169 (if t167 t168 t166))
                                (= t170 (= (extract 54 54 rn) #b1))
                                (if t170 (= t171 (bvadd t169 #x1)) true)
                                (= t172 (if t170 t171 t169))
                                (= t173 (= (extract 55 55 rn) #b1))
                                (if t173 (= t174 (bvadd t172 #x1)) true)
                                (= t175 (if t173 t174 t172))
                                (= t176 #x0)
                                (= t177 (= (extract 56 56 rn) #b1))
                                (if t177 (= t178 #x1) true)
                                (= t179 (if t177 t178 t176))
                                (= t180 (= (extract 57 57 rn) #b1))
                                (if t180 (= t181 (bvadd t179 #x1)) true)
                                (= t182 (if t180 t181 t179))
                                (= t183 (= (extract 58 58 rn) #b1))
                                (if t183 (= t184 (bvadd t182 #x1)) true)
                                (= t185 (if t183 t184 t182))
                                (= t186 (= (extract 59 59 rn) #b1))
                                (if t186 (= t187 (bvadd t185 #x1)) true)
                                (= t188 (if t186 t187 t185))
                                (= t189 (= (extract 60 60 rn) #b1))
                                (if t189 (= t190 (bvadd t188 #x1)) true)
                                (= t191 (if t189 t190 t188))
                                (= t192 (= (extract 61 61 rn) #b1))
                                (if t192 (= t193 (bvadd t191 #x1)) true)
                                (= t194 (if t192 t193 t191))
                                (= t195 (= (extract 62 62 rn) #b1))
                                (if t195 (= t196 (bvadd t194 #x1)) true)
                                (= t197 (if t195 t196 t194))
                                (= t198 (= (extract 63 63 rn) #b1))
                                (if t198 (= t199 (bvadd t197 #x1)) true)
                                (= t200 (if t198 t199 t197))
                                (=
                                    rd
                                    (zero_ext
                                        128
                                        (concat
                                            (zero_ext 8 t200)
                                            (concat
                                                (zero_ext 8 t175)
                                                (concat
                                                    (zero_ext 8 t150)
                                                    (concat
                                                        (zero_ext 8 t125)
                                                        (concat (zero_ext 8 t100) (concat (zero_ext 8 t75) (concat (zero_ext 8 t50) (zero_ext 8 t25))))
                                                    )
                                                )
                                            )
                                        )
                                    )
                                )
                            )
                        )
                    )
                )
            )
        )
    )
    (require (match size ((Size8x16) (match op ((Cnt) true))) ((Size8x8) (match op ((Cnt) true)))))
)