def aria_sb42
import bend-osdev-aria@0.1.0.0/PROOF.bend as PROOFimport Base
import bend-osdev-aria@0.1.0.0/aria.bend as A
3085def aria_sb42(w0: Word(8n)) -> {w0 == A.aria.sb4(A.aria.sb2(w0)) : Word(8n)}:
3086 match w0:
3087 case WCon{False{}, w1}:
3088 match w1:
3089 case WCon{False{}, w2}:
3090 match w2:
3091 case WCon{False{}, w3}:
3092 match w3:
3093 case WCon{False{}, w4}:
3094 match w4:
3095 case WCon{False{}, w5}:
3096 match w5:
3097 case WCon{False{}, w6}:
3098 match w6:
3099 case WCon{False{}, w7}:
3100 match w7:
3101 case WCon{False{}, w8}:
3102 match w8:
3103 case WNil{}:
3104 {==}
3105 case WCon{True{}, w8}:
3106 match w8:
3107 case WNil{}:
3108 {==}
3109 case WCon{True{}, w7}:
3110 match w7:
3111 case WCon{False{}, w8}:
3112 match w8:
3113 case WNil{}:
3114 {==}
3115 case WCon{True{}, w8}:
3116 match w8:
3117 case WNil{}:
3118 {==}
3119 case WCon{True{}, w6}:
3120 match w6:
3121 case WCon{False{}, w7}:
3122 match w7:
3123 case WCon{False{}, w8}:
3124 match w8:
3125 case WNil{}:
3126 {==}
3127 case WCon{True{}, w8}:
3128 match w8:
3129 case WNil{}:
3130 {==}
3131 case WCon{True{}, w7}:
3132 match w7:
3133 case WCon{False{}, w8}:
3134 match w8:
3135 case WNil{}:
3136 {==}
3137 case WCon{True{}, w8}:
3138 match w8:
3139 case WNil{}:
3140 {==}
3141 case WCon{True{}, w5}:
3142 match w5:
3143 case WCon{False{}, w6}:
3144 match w6:
3145 case WCon{False{}, w7}:
3146 match w7:
3147 case WCon{False{}, w8}:
3148 match w8:
3149 case WNil{}:
3150 {==}
3151 case WCon{True{}, w8}:
3152 match w8:
3153 case WNil{}:
3154 {==}
3155 case WCon{True{}, w7}:
3156 match w7:
3157 case WCon{False{}, w8}:
3158 match w8:
3159 case WNil{}:
3160 {==}
3161 case WCon{True{}, w8}:
3162 match w8:
3163 case WNil{}:
3164 {==}
3165 case WCon{True{}, w6}:
3166 match w6:
3167 case WCon{False{}, w7}:
3168 match w7:
3169 case WCon{False{}, w8}:
3170 match w8:
3171 case WNil{}:
3172 {==}
3173 case WCon{True{}, w8}:
3174 match w8:
3175 case WNil{}:
3176 {==}
3177 case WCon{True{}, w7}:
3178 match w7:
3179 case WCon{False{}, w8}:
3180 match w8:
3181 case WNil{}:
3182 {==}
3183 case WCon{True{}, w8}:
3184 match w8:
3185 case WNil{}:
3186 {==}
3187 case WCon{True{}, w4}:
3188 match w4:
3189 case WCon{False{}, w5}:
3190 match w5:
3191 case WCon{False{}, w6}:
3192 match w6:
3193 case WCon{False{}, w7}:
3194 match w7:
3195 case WCon{False{}, w8}:
3196 match w8:
3197 case WNil{}:
3198 {==}
3199 case WCon{True{}, w8}:
3200 match w8:
3201 case WNil{}:
3202 {==}
3203 case WCon{True{}, w7}:
3204 match w7:
3205 case WCon{False{}, w8}:
3206 match w8:
3207 case WNil{}:
3208 {==}
3209 case WCon{True{}, w8}:
3210 match w8:
3211 case WNil{}:
3212 {==}
3213 case WCon{True{}, w6}:
3214 match w6:
3215 case WCon{False{}, w7}:
3216 match w7:
3217 case WCon{False{}, w8}:
3218 match w8:
3219 case WNil{}:
3220 {==}
3221 case WCon{True{}, w8}:
3222 match w8:
3223 case WNil{}:
3224 {==}
3225 case WCon{True{}, w7}:
3226 match w7:
3227 case WCon{False{}, w8}:
3228 match w8:
3229 case WNil{}:
3230 {==}
3231 case WCon{True{}, w8}:
3232 match w8:
3233 case WNil{}:
3234 {==}
3235 case WCon{True{}, w5}:
3236 match w5:
3237 case WCon{False{}, w6}:
3238 match w6:
3239 case WCon{False{}, w7}:
3240 match w7:
3241 case WCon{False{}, w8}:
3242 match w8:
3243 case WNil{}:
3244 {==}
3245 case WCon{True{}, w8}:
3246 match w8:
3247 case WNil{}:
3248 {==}
3249 case WCon{True{}, w7}:
3250 match w7:
3251 case WCon{False{}, w8}:
3252 match w8:
3253 case WNil{}:
3254 {==}
3255 case WCon{True{}, w8}:
3256 match w8:
3257 case WNil{}:
3258 {==}
3259 case WCon{True{}, w6}:
3260 match w6:
3261 case WCon{False{}, w7}:
3262 match w7:
3263 case WCon{False{}, w8}:
3264 match w8:
3265 case WNil{}:
3266 {==}
3267 case WCon{True{}, w8}:
3268 match w8:
3269 case WNil{}:
3270 {==}
3271 case WCon{True{}, w7}:
3272 match w7:
3273 case WCon{False{}, w8}:
3274 match w8:
3275 case WNil{}:
3276 {==}
3277 case WCon{True{}, w8}:
3278 match w8:
3279 case WNil{}:
3280 {==}
3281 case WCon{True{}, w3}:
3282 match w3:
3283 case WCon{False{}, w4}:
3284 match w4:
3285 case WCon{False{}, w5}:
3286 match w5:
3287 case WCon{False{}, w6}:
3288 match w6:
3289 case WCon{False{}, w7}:
3290 match w7:
3291 case WCon{False{}, w8}:
3292 match w8:
3293 case WNil{}:
3294 {==}
3295 case WCon{True{}, w8}:
3296 match w8:
3297 case WNil{}:
3298 {==}
3299 case WCon{True{}, w7}:
3300 match w7:
3301 case WCon{False{}, w8}:
3302 match w8:
3303 case WNil{}:
3304 {==}
3305 case WCon{True{}, w8}:
3306 match w8:
3307 case WNil{}:
3308 {==}
3309 case WCon{True{}, w6}:
3310 match w6:
3311 case WCon{False{}, w7}:
3312 match w7:
3313 case WCon{False{}, w8}:
3314 match w8:
3315 case WNil{}:
3316 {==}
3317 case WCon{True{}, w8}:
3318 match w8:
3319 case WNil{}:
3320 {==}
3321 case WCon{True{}, w7}:
3322 match w7:
3323 case WCon{False{}, w8}:
3324 match w8:
3325 case WNil{}:
3326 {==}
3327 case WCon{True{}, w8}:
3328 match w8:
3329 case WNil{}:
3330 {==}
3331 case WCon{True{}, w5}:
3332 match w5:
3333 case WCon{False{}, w6}:
3334 match w6:
3335 case WCon{False{}, w7}:
3336 match w7:
3337 case WCon{False{}, w8}:
3338 match w8:
3339 case WNil{}:
3340 {==}
3341 case WCon{True{}, w8}:
3342 match w8:
3343 case WNil{}:
3344 {==}
3345 case WCon{True{}, w7}:
3346 match w7:
3347 case WCon{False{}, w8}:
3348 match w8:
3349 case WNil{}:
3350 {==}
3351 case WCon{True{}, w8}:
3352 match w8:
3353 case WNil{}:
3354 {==}
3355 case WCon{True{}, w6}:
3356 match w6:
3357 case WCon{False{}, w7}:
3358 match w7:
3359 case WCon{False{}, w8}:
3360 match w8:
3361 case WNil{}:
3362 {==}
3363 case WCon{True{}, w8}:
3364 match w8:
3365 case WNil{}:
3366 {==}
3367 case WCon{True{}, w7}:
3368 match w7:
3369 case WCon{False{}, w8}:
3370 match w8:
3371 case WNil{}:
3372 {==}
3373 case WCon{True{}, w8}:
3374 match w8:
3375 case WNil{}:
3376 {==}
3377 case WCon{True{}, w4}:
3378 match w4:
3379 case WCon{False{}, w5}:
3380 match w5:
3381 case WCon{False{}, w6}:
3382 match w6:
3383 case WCon{False{}, w7}:
3384 match w7:
3385 case WCon{False{}, w8}:
3386 match w8:
3387 case WNil{}:
3388 {==}
3389 case WCon{True{}, w8}:
3390 match w8:
3391 case WNil{}:
3392 {==}
3393 case WCon{True{}, w7}:
3394 match w7:
3395 case WCon{False{}, w8}:
3396 match w8:
3397 case WNil{}:
3398 {==}
3399 case WCon{True{}, w8}:
3400 match w8:
3401 case WNil{}:
3402 {==}
3403 case WCon{True{}, w6}:
3404 match w6:
3405 case WCon{False{}, w7}:
3406 match w7:
3407 case WCon{False{}, w8}:
3408 match w8:
3409 case WNil{}:
3410 {==}
3411 case WCon{True{}, w8}:
3412 match w8:
3413 case WNil{}:
3414 {==}
3415 case WCon{True{}, w7}:
3416 match w7:
3417 case WCon{False{}, w8}:
3418 match w8:
3419 case WNil{}:
3420 {==}
3421 case WCon{True{}, w8}:
3422 match w8:
3423 case WNil{}:
3424 {==}
3425 case WCon{True{}, w5}:
3426 match w5:
3427 case WCon{False{}, w6}:
3428 match w6:
3429 case WCon{False{}, w7}:
3430 match w7:
3431 case WCon{False{}, w8}:
3432 match w8:
3433 case WNil{}:
3434 {==}
3435 case WCon{True{}, w8}:
3436 match w8:
3437 case WNil{}:
3438 {==}
3439 case WCon{True{}, w7}:
3440 match w7:
3441 case WCon{False{}, w8}:
3442 match w8:
3443 case WNil{}:
3444 {==}
3445 case WCon{True{}, w8}:
3446 match w8:
3447 case WNil{}:
3448 {==}
3449 case WCon{True{}, w6}:
3450 match w6:
3451 case WCon{False{}, w7}:
3452 match w7:
3453 case WCon{False{}, w8}:
3454 match w8:
3455 case WNil{}:
3456 {==}
3457 case WCon{True{}, w8}:
3458 match w8:
3459 case WNil{}:
3460 {==}
3461 case WCon{True{}, w7}:
3462 match w7:
3463 case WCon{False{}, w8}:
3464 match w8:
3465 case WNil{}:
3466 {==}
3467 case WCon{True{}, w8}:
3468 match w8:
3469 case WNil{}:
3470 {==}
3471 case WCon{True{}, w2}:
3472 match w2:
3473 case WCon{False{}, w3}:
3474 match w3:
3475 case WCon{False{}, w4}:
3476 match w4:
3477 case WCon{False{}, w5}:
3478 match w5:
3479 case WCon{False{}, w6}:
3480 match w6:
3481 case WCon{False{}, w7}:
3482 match w7:
3483 case WCon{False{}, w8}:
3484 match w8:
3485 case WNil{}:
3486 {==}
3487 case WCon{True{}, w8}:
3488 match w8:
3489 case WNil{}:
3490 {==}
3491 case WCon{True{}, w7}:
3492 match w7:
3493 case WCon{False{}, w8}:
3494 match w8:
3495 case WNil{}:
3496 {==}
3497 case WCon{True{}, w8}:
3498 match w8:
3499 case WNil{}:
3500 {==}
3501 case WCon{True{}, w6}:
3502 match w6:
3503 case WCon{False{}, w7}:
3504 match w7:
3505 case WCon{False{}, w8}:
3506 match w8:
3507 case WNil{}:
3508 {==}
3509 case WCon{True{}, w8}:
3510 match w8:
3511 case WNil{}:
3512 {==}
3513 case WCon{True{}, w7}:
3514 match w7:
3515 case WCon{False{}, w8}:
3516 match w8:
3517 case WNil{}:
3518 {==}
3519 case WCon{True{}, w8}:
3520 match w8:
3521 case WNil{}:
3522 {==}
3523 case WCon{True{}, w5}:
3524 match w5:
3525 case WCon{False{}, w6}:
3526 match w6:
3527 case WCon{False{}, w7}:
3528 match w7:
3529 case WCon{False{}, w8}:
3530 match w8:
3531 case WNil{}:
3532 {==}
3533 case WCon{True{}, w8}:
3534 match w8:
3535 case WNil{}:
3536 {==}
3537 case WCon{True{}, w7}:
3538 match w7:
3539 case WCon{False{}, w8}:
3540 match w8:
3541 case WNil{}:
3542 {==}
3543 case WCon{True{}, w8}:
3544 match w8:
3545 case WNil{}:
3546 {==}
3547 case WCon{True{}, w6}:
3548 match w6:
3549 case WCon{False{}, w7}:
3550 match w7:
3551 case WCon{False{}, w8}:
3552 match w8:
3553 case WNil{}:
3554 {==}
3555 case WCon{True{}, w8}:
3556 match w8:
3557 case WNil{}:
3558 {==}
3559 case WCon{True{}, w7}:
3560 match w7:
3561 case WCon{False{}, w8}:
3562 match w8:
3563 case WNil{}:
3564 {==}
3565 case WCon{True{}, w8}:
3566 match w8:
3567 case WNil{}:
3568 {==}
3569 case WCon{True{}, w4}:
3570 match w4:
3571 case WCon{False{}, w5}:
3572 match w5:
3573 case WCon{False{}, w6}:
3574 match w6:
3575 case WCon{False{}, w7}:
3576 match w7:
3577 case WCon{False{}, w8}:
3578 match w8:
3579 case WNil{}:
3580 {==}
3581 case WCon{True{}, w8}:
3582 match w8:
3583 case WNil{}:
3584 {==}
3585 case WCon{True{}, w7}:
3586 match w7:
3587 case WCon{False{}, w8}:
3588 match w8:
3589 case WNil{}:
3590 {==}
3591 case WCon{True{}, w8}:
3592 match w8:
3593 case WNil{}:
3594 {==}
3595 case WCon{True{}, w6}:
3596 match w6:
3597 case WCon{False{}, w7}:
3598 match w7:
3599 case WCon{False{}, w8}:
3600 match w8:
3601 case WNil{}:
3602 {==}
3603 case WCon{True{}, w8}:
3604 match w8:
3605 case WNil{}:
3606 {==}
3607 case WCon{True{}, w7}:
3608 match w7:
3609 case WCon{False{}, w8}:
3610 match w8:
3611 case WNil{}:
3612 {==}
3613 case WCon{True{}, w8}:
3614 match w8:
3615 case WNil{}:
3616 {==}
3617 case WCon{True{}, w5}:
3618 match w5:
3619 case WCon{False{}, w6}:
3620 match w6:
3621 case WCon{False{}, w7}:
3622 match w7:
3623 case WCon{False{}, w8}:
3624 match w8:
3625 case WNil{}:
3626 {==}
3627 case WCon{True{}, w8}:
3628 match w8:
3629 case WNil{}:
3630 {==}
3631 case WCon{True{}, w7}:
3632 match w7:
3633 case WCon{False{}, w8}:
3634 match w8:
3635 case WNil{}:
3636 {==}
3637 case WCon{True{}, w8}:
3638 match w8:
3639 case WNil{}:
3640 {==}
3641 case WCon{True{}, w6}:
3642 match w6:
3643 case WCon{False{}, w7}:
3644 match w7:
3645 case WCon{False{}, w8}:
3646 match w8:
3647 case WNil{}:
3648 {==}
3649 case WCon{True{}, w8}:
3650 match w8:
3651 case WNil{}:
3652 {==}
3653 case WCon{True{}, w7}:
3654 match w7:
3655 case WCon{False{}, w8}:
3656 match w8:
3657 case WNil{}:
3658 {==}
3659 case WCon{True{}, w8}:
3660 match w8:
3661 case WNil{}:
3662 {==}
3663 case WCon{True{}, w3}:
3664 match w3:
3665 case WCon{False{}, w4}:
3666 match w4:
3667 case WCon{False{}, w5}:
3668 match w5:
3669 case WCon{False{}, w6}:
3670 match w6:
3671 case WCon{False{}, w7}:
3672 match w7:
3673 case WCon{False{}, w8}:
3674 match w8:
3675 case WNil{}:
3676 {==}
3677 case WCon{True{}, w8}:
3678 match w8:
3679 case WNil{}:
3680 {==}
3681 case WCon{True{}, w7}:
3682 match w7:
3683 case WCon{False{}, w8}:
3684 match w8:
3685 case WNil{}:
3686 {==}
3687 case WCon{True{}, w8}:
3688 match w8:
3689 case WNil{}:
3690 {==}
3691 case WCon{True{}, w6}:
3692 match w6:
3693 case WCon{False{}, w7}:
3694 match w7:
3695 case WCon{False{}, w8}:
3696 match w8:
3697 case WNil{}:
3698 {==}
3699 case WCon{True{}, w8}:
3700 match w8:
3701 case WNil{}:
3702 {==}
3703 case WCon{True{}, w7}:
3704 match w7:
3705 case WCon{False{}, w8}:
3706 match w8:
3707 case WNil{}:
3708 {==}
3709 case WCon{True{}, w8}:
3710 match w8:
3711 case WNil{}:
3712 {==}
3713 case WCon{True{}, w5}:
3714 match w5:
3715 case WCon{False{}, w6}:
3716 match w6:
3717 case WCon{False{}, w7}:
3718 match w7:
3719 case WCon{False{}, w8}:
3720 match w8:
3721 case WNil{}:
3722 {==}
3723 case WCon{True{}, w8}:
3724 match w8:
3725 case WNil{}:
3726 {==}
3727 case WCon{True{}, w7}:
3728 match w7:
3729 case WCon{False{}, w8}:
3730 match w8:
3731 case WNil{}:
3732 {==}
3733 case WCon{True{}, w8}:
3734 match w8:
3735 case WNil{}:
3736 {==}
3737 case WCon{True{}, w6}:
3738 match w6:
3739 case WCon{False{}, w7}:
3740 match w7:
3741 case WCon{False{}, w8}:
3742 match w8:
3743 case WNil{}:
3744 {==}
3745 case WCon{True{}, w8}:
3746 match w8:
3747 case WNil{}:
3748 {==}
3749 case WCon{True{}, w7}:
3750 match w7:
3751 case WCon{False{}, w8}:
3752 match w8:
3753 case WNil{}:
3754 {==}
3755 case WCon{True{}, w8}:
3756 match w8:
3757 case WNil{}:
3758 {==}
3759 case WCon{True{}, w4}:
3760 match w4:
3761 case WCon{False{}, w5}:
3762 match w5:
3763 case WCon{False{}, w6}:
3764 match w6:
3765 case WCon{False{}, w7}:
3766 match w7:
3767 case WCon{False{}, w8}:
3768 match w8:
3769 case WNil{}:
3770 {==}
3771 case WCon{True{}, w8}:
3772 match w8:
3773 case WNil{}:
3774 {==}
3775 case WCon{True{}, w7}:
3776 match w7:
3777 case WCon{False{}, w8}:
3778 match w8:
3779 case WNil{}:
3780 {==}
3781 case WCon{True{}, w8}:
3782 match w8:
3783 case WNil{}:
3784 {==}
3785 case WCon{True{}, w6}:
3786 match w6:
3787 case WCon{False{}, w7}:
3788 match w7:
3789 case WCon{False{}, w8}:
3790 match w8:
3791 case WNil{}:
3792 {==}
3793 case WCon{True{}, w8}:
3794 match w8:
3795 case WNil{}:
3796 {==}
3797 case WCon{True{}, w7}:
3798 match w7:
3799 case WCon{False{}, w8}:
3800 match w8:
3801 case WNil{}:
3802 {==}
3803 case WCon{True{}, w8}:
3804 match w8:
3805 case WNil{}:
3806 {==}
3807 case WCon{True{}, w5}:
3808 match w5:
3809 case WCon{False{}, w6}:
3810 match w6:
3811 case WCon{False{}, w7}:
3812 match w7:
3813 case WCon{False{}, w8}:
3814 match w8:
3815 case WNil{}:
3816 {==}
3817 case WCon{True{}, w8}:
3818 match w8:
3819 case WNil{}:
3820 {==}
3821 case WCon{True{}, w7}:
3822 match w7:
3823 case WCon{False{}, w8}:
3824 match w8:
3825 case WNil{}:
3826 {==}
3827 case WCon{True{}, w8}:
3828 match w8:
3829 case WNil{}:
3830 {==}
3831 case WCon{True{}, w6}:
3832 match w6:
3833 case WCon{False{}, w7}:
3834 match w7:
3835 case WCon{False{}, w8}:
3836 match w8:
3837 case WNil{}:
3838 {==}
3839 case WCon{True{}, w8}:
3840 match w8:
3841 case WNil{}:
3842 {==}
3843 case WCon{True{}, w7}:
3844 match w7:
3845 case WCon{False{}, w8}:
3846 match w8:
3847 case WNil{}:
3848 {==}
3849 case WCon{True{}, w8}:
3850 match w8:
3851 case WNil{}:
3852 {==}
3853 case WCon{True{}, w1}:
3854 match w1:
3855 case WCon{False{}, w2}:
3856 match w2:
3857 case WCon{False{}, w3}:
3858 match w3:
3859 case WCon{False{}, w4}:
3860 match w4:
3861 case WCon{False{}, w5}:
3862 match w5:
3863 case WCon{False{}, w6}:
3864 match w6:
3865 case WCon{False{}, w7}:
3866 match w7:
3867 case WCon{False{}, w8}:
3868 match w8:
3869 case WNil{}:
3870 {==}
3871 case WCon{True{}, w8}:
3872 match w8:
3873 case WNil{}:
3874 {==}
3875 case WCon{True{}, w7}:
3876 match w7:
3877 case WCon{False{}, w8}:
3878 match w8:
3879 case WNil{}:
3880 {==}
3881 case WCon{True{}, w8}:
3882 match w8:
3883 case WNil{}:
3884 {==}
3885 case WCon{True{}, w6}:
3886 match w6:
3887 case WCon{False{}, w7}:
3888 match w7:
3889 case WCon{False{}, w8}:
3890 match w8:
3891 case WNil{}:
3892 {==}
3893 case WCon{True{}, w8}:
3894 match w8:
3895 case WNil{}:
3896 {==}
3897 case WCon{True{}, w7}:
3898 match w7:
3899 case WCon{False{}, w8}:
3900 match w8:
3901 case WNil{}:
3902 {==}
3903 case WCon{True{}, w8}:
3904 match w8:
3905 case WNil{}:
3906 {==}
3907 case WCon{True{}, w5}:
3908 match w5:
3909 case WCon{False{}, w6}:
3910 match w6:
3911 case WCon{False{}, w7}:
3912 match w7:
3913 case WCon{False{}, w8}:
3914 match w8:
3915 case WNil{}:
3916 {==}
3917 case WCon{True{}, w8}:
3918 match w8:
3919 case WNil{}:
3920 {==}
3921 case WCon{True{}, w7}:
3922 match w7:
3923 case WCon{False{}, w8}:
3924 match w8:
3925 case WNil{}:
3926 {==}
3927 case WCon{True{}, w8}:
3928 match w8:
3929 case WNil{}:
3930 {==}
3931 case WCon{True{}, w6}:
3932 match w6:
3933 case WCon{False{}, w7}:
3934 match w7:
3935 case WCon{False{}, w8}:
3936 match w8:
3937 case WNil{}:
3938 {==}
3939 case WCon{True{}, w8}:
3940 match w8:
3941 case WNil{}:
3942 {==}
3943 case WCon{True{}, w7}:
3944 match w7:
3945 case WCon{False{}, w8}:
3946 match w8:
3947 case WNil{}:
3948 {==}
3949 case WCon{True{}, w8}:
3950 match w8:
3951 case WNil{}:
3952 {==}
3953 case WCon{True{}, w4}:
3954 match w4:
3955 case WCon{False{}, w5}:
3956 match w5:
3957 case WCon{False{}, w6}:
3958 match w6:
3959 case WCon{False{}, w7}:
3960 match w7:
3961 case WCon{False{}, w8}:
3962 match w8:
3963 case WNil{}:
3964 {==}
3965 case WCon{True{}, w8}:
3966 match w8:
3967 case WNil{}:
3968 {==}
3969 case WCon{True{}, w7}:
3970 match w7:
3971 case WCon{False{}, w8}:
3972 match w8:
3973 case WNil{}:
3974 {==}
3975 case WCon{True{}, w8}:
3976 match w8:
3977 case WNil{}:
3978 {==}
3979 case WCon{True{}, w6}:
3980 match w6:
3981 case WCon{False{}, w7}:
3982 match w7:
3983 case WCon{False{}, w8}:
3984 match w8:
3985 case WNil{}:
3986 {==}
3987 case WCon{True{}, w8}:
3988 match w8:
3989 case WNil{}:
3990 {==}
3991 case WCon{True{}, w7}:
3992 match w7:
3993 case WCon{False{}, w8}:
3994 match w8:
3995 case WNil{}:
3996 {==}
3997 case WCon{True{}, w8}:
3998 match w8:
3999 case WNil{}:
4000 {==}
4001 case WCon{True{}, w5}:
4002 match w5:
4003 case WCon{False{}, w6}:
4004 match w6:
4005 case WCon{False{}, w7}:
4006 match w7:
4007 case WCon{False{}, w8}:
4008 match w8:
4009 case WNil{}:
4010 {==}
4011 case WCon{True{}, w8}:
4012 match w8:
4013 case WNil{}:
4014 {==}
4015 case WCon{True{}, w7}:
4016 match w7:
4017 case WCon{False{}, w8}:
4018 match w8:
4019 case WNil{}:
4020 {==}
4021 case WCon{True{}, w8}:
4022 match w8:
4023 case WNil{}:
4024 {==}
4025 case WCon{True{}, w6}:
4026 match w6:
4027 case WCon{False{}, w7}:
4028 match w7:
4029 case WCon{False{}, w8}:
4030 match w8:
4031 case WNil{}:
4032 {==}
4033 case WCon{True{}, w8}:
4034 match w8:
4035 case WNil{}:
4036 {==}
4037 case WCon{True{}, w7}:
4038 match w7:
4039 case WCon{False{}, w8}:
4040 match w8:
4041 case WNil{}:
4042 {==}
4043 case WCon{True{}, w8}:
4044 match w8:
4045 case WNil{}:
4046 {==}
4047 case WCon{True{}, w3}:
4048 match w3:
4049 case WCon{False{}, w4}:
4050 match w4:
4051 case WCon{False{}, w5}:
4052 match w5:
4053 case WCon{False{}, w6}:
4054 match w6:
4055 case WCon{False{}, w7}:
4056 match w7:
4057 case WCon{False{}, w8}:
4058 match w8:
4059 case WNil{}:
4060 {==}
4061 case WCon{True{}, w8}:
4062 match w8:
4063 case WNil{}:
4064 {==}
4065 case WCon{True{}, w7}:
4066 match w7:
4067 case WCon{False{}, w8}:
4068 match w8:
4069 case WNil{}:
4070 {==}
4071 case WCon{True{}, w8}:
4072 match w8:
4073 case WNil{}:
4074 {==}
4075 case WCon{True{}, w6}:
4076 match w6:
4077 case WCon{False{}, w7}:
4078 match w7:
4079 case WCon{False{}, w8}:
4080 match w8:
4081 case WNil{}:
4082 {==}
4083 case WCon{True{}, w8}:
4084 match w8:
4085 case WNil{}:
4086 {==}
4087 case WCon{True{}, w7}:
4088 match w7:
4089 case WCon{False{}, w8}:
4090 match w8:
4091 case WNil{}:
4092 {==}
4093 case WCon{True{}, w8}:
4094 match w8:
4095 case WNil{}:
4096 {==}
4097 case WCon{True{}, w5}:
4098 match w5:
4099 case WCon{False{}, w6}:
4100 match w6:
4101 case WCon{False{}, w7}:
4102 match w7:
4103 case WCon{False{}, w8}:
4104 match w8:
4105 case WNil{}:
4106 {==}
4107 case WCon{True{}, w8}:
4108 match w8:
4109 case WNil{}:
4110 {==}
4111 case WCon{True{}, w7}:
4112 match w7:
4113 case WCon{False{}, w8}:
4114 match w8:
4115 case WNil{}:
4116 {==}
4117 case WCon{True{}, w8}:
4118 match w8:
4119 case WNil{}:
4120 {==}
4121 case WCon{True{}, w6}:
4122 match w6:
4123 case WCon{False{}, w7}:
4124 match w7:
4125 case WCon{False{}, w8}:
4126 match w8:
4127 case WNil{}:
4128 {==}
4129 case WCon{True{}, w8}:
4130 match w8:
4131 case WNil{}:
4132 {==}
4133 case WCon{True{}, w7}:
4134 match w7:
4135 case WCon{False{}, w8}:
4136 match w8:
4137 case WNil{}:
4138 {==}
4139 case WCon{True{}, w8}:
4140 match w8:
4141 case WNil{}:
4142 {==}
4143 case WCon{True{}, w4}:
4144 match w4:
4145 case WCon{False{}, w5}:
4146 match w5:
4147 case WCon{False{}, w6}:
4148 match w6:
4149 case WCon{False{}, w7}:
4150 match w7:
4151 case WCon{False{}, w8}:
4152 match w8:
4153 case WNil{}:
4154 {==}
4155 case WCon{True{}, w8}:
4156 match w8:
4157 case WNil{}:
4158 {==}
4159 case WCon{True{}, w7}:
4160 match w7:
4161 case WCon{False{}, w8}:
4162 match w8:
4163 case WNil{}:
4164 {==}
4165 case WCon{True{}, w8}:
4166 match w8:
4167 case WNil{}:
4168 {==}
4169 case WCon{True{}, w6}:
4170 match w6:
4171 case WCon{False{}, w7}:
4172 match w7:
4173 case WCon{False{}, w8}:
4174 match w8:
4175 case WNil{}:
4176 {==}
4177 case WCon{True{}, w8}:
4178 match w8:
4179 case WNil{}:
4180 {==}
4181 case WCon{True{}, w7}:
4182 match w7:
4183 case WCon{False{}, w8}:
4184 match w8:
4185 case WNil{}:
4186 {==}
4187 case WCon{True{}, w8}:
4188 match w8:
4189 case WNil{}:
4190 {==}
4191 case WCon{True{}, w5}:
4192 match w5:
4193 case WCon{False{}, w6}:
4194 match w6:
4195 case WCon{False{}, w7}:
4196 match w7:
4197 case WCon{False{}, w8}:
4198 match w8:
4199 case WNil{}:
4200 {==}
4201 case WCon{True{}, w8}:
4202 match w8:
4203 case WNil{}:
4204 {==}
4205 case WCon{True{}, w7}:
4206 match w7:
4207 case WCon{False{}, w8}:
4208 match w8:
4209 case WNil{}:
4210 {==}
4211 case WCon{True{}, w8}:
4212 match w8:
4213 case WNil{}:
4214 {==}
4215 case WCon{True{}, w6}:
4216 match w6:
4217 case WCon{False{}, w7}:
4218 match w7:
4219 case WCon{False{}, w8}:
4220 match w8:
4221 case WNil{}:
4222 {==}
4223 case WCon{True{}, w8}:
4224 match w8:
4225 case WNil{}:
4226 {==}
4227 case WCon{True{}, w7}:
4228 match w7:
4229 case WCon{False{}, w8}:
4230 match w8:
4231 case WNil{}:
4232 {==}
4233 case WCon{True{}, w8}:
4234 match w8:
4235 case WNil{}:
4236 {==}
4237 case WCon{True{}, w2}:
4238 match w2:
4239 case WCon{False{}, w3}:
4240 match w3:
4241 case WCon{False{}, w4}:
4242 match w4:
4243 case WCon{False{}, w5}:
4244 match w5:
4245 case WCon{False{}, w6}:
4246 match w6:
4247 case WCon{False{}, w7}:
4248 match w7:
4249 case WCon{False{}, w8}:
4250 match w8:
4251 case WNil{}:
4252 {==}
4253 case WCon{True{}, w8}:
4254 match w8:
4255 case WNil{}:
4256 {==}
4257 case WCon{True{}, w7}:
4258 match w7:
4259 case WCon{False{}, w8}:
4260 match w8:
4261 case WNil{}:
4262 {==}
4263 case WCon{True{}, w8}:
4264 match w8:
4265 case WNil{}:
4266 {==}
4267 case WCon{True{}, w6}:
4268 match w6:
4269 case WCon{False{}, w7}:
4270 match w7:
4271 case WCon{False{}, w8}:
4272 match w8:
4273 case WNil{}:
4274 {==}
4275 case WCon{True{}, w8}:
4276 match w8:
4277 case WNil{}:
4278 {==}
4279 case WCon{True{}, w7}:
4280 match w7:
4281 case WCon{False{}, w8}:
4282 match w8:
4283 case WNil{}:
4284 {==}
4285 case WCon{True{}, w8}:
4286 match w8:
4287 case WNil{}:
4288 {==}
4289 case WCon{True{}, w5}:
4290 match w5:
4291 case WCon{False{}, w6}:
4292 match w6:
4293 case WCon{False{}, w7}:
4294 match w7:
4295 case WCon{False{}, w8}:
4296 match w8:
4297 case WNil{}:
4298 {==}
4299 case WCon{True{}, w8}:
4300 match w8:
4301 case WNil{}:
4302 {==}
4303 case WCon{True{}, w7}:
4304 match w7:
4305 case WCon{False{}, w8}:
4306 match w8:
4307 case WNil{}:
4308 {==}
4309 case WCon{True{}, w8}:
4310 match w8:
4311 case WNil{}:
4312 {==}
4313 case WCon{True{}, w6}:
4314 match w6:
4315 case WCon{False{}, w7}:
4316 match w7:
4317 case WCon{False{}, w8}:
4318 match w8:
4319 case WNil{}:
4320 {==}
4321 case WCon{True{}, w8}:
4322 match w8:
4323 case WNil{}:
4324 {==}
4325 case WCon{True{}, w7}:
4326 match w7:
4327 case WCon{False{}, w8}:
4328 match w8:
4329 case WNil{}:
4330 {==}
4331 case WCon{True{}, w8}:
4332 match w8:
4333 case WNil{}:
4334 {==}
4335 case WCon{True{}, w4}:
4336 match w4:
4337 case WCon{False{}, w5}:
4338 match w5:
4339 case WCon{False{}, w6}:
4340 match w6:
4341 case WCon{False{}, w7}:
4342 match w7:
4343 case WCon{False{}, w8}:
4344 match w8:
4345 case WNil{}:
4346 {==}
4347 case WCon{True{}, w8}:
4348 match w8:
4349 case WNil{}:
4350 {==}
4351 case WCon{True{}, w7}:
4352 match w7:
4353 case WCon{False{}, w8}:
4354 match w8:
4355 case WNil{}:
4356 {==}
4357 case WCon{True{}, w8}:
4358 match w8:
4359 case WNil{}:
4360 {==}
4361 case WCon{True{}, w6}:
4362 match w6:
4363 case WCon{False{}, w7}:
4364 match w7:
4365 case WCon{False{}, w8}:
4366 match w8:
4367 case WNil{}:
4368 {==}
4369 case WCon{True{}, w8}:
4370 match w8:
4371 case WNil{}:
4372 {==}
4373 case WCon{True{}, w7}:
4374 match w7:
4375 case WCon{False{}, w8}:
4376 match w8:
4377 case WNil{}:
4378 {==}
4379 case WCon{True{}, w8}:
4380 match w8:
4381 case WNil{}:
4382 {==}
4383 case WCon{True{}, w5}:
4384 match w5:
4385 case WCon{False{}, w6}:
4386 match w6:
4387 case WCon{False{}, w7}:
4388 match w7:
4389 case WCon{False{}, w8}:
4390 match w8:
4391 case WNil{}:
4392 {==}
4393 case WCon{True{}, w8}:
4394 match w8:
4395 case WNil{}:
4396 {==}
4397 case WCon{True{}, w7}:
4398 match w7:
4399 case WCon{False{}, w8}:
4400 match w8:
4401 case WNil{}:
4402 {==}
4403 case WCon{True{}, w8}:
4404 match w8:
4405 case WNil{}:
4406 {==}
4407 case WCon{True{}, w6}:
4408 match w6:
4409 case WCon{False{}, w7}:
4410 match w7:
4411 case WCon{False{}, w8}:
4412 match w8:
4413 case WNil{}:
4414 {==}
4415 case WCon{True{}, w8}:
4416 match w8:
4417 case WNil{}:
4418 {==}
4419 case WCon{True{}, w7}:
4420 match w7:
4421 case WCon{False{}, w8}:
4422 match w8:
4423 case WNil{}:
4424 {==}
4425 case WCon{True{}, w8}:
4426 match w8:
4427 case WNil{}:
4428 {==}
4429 case WCon{True{}, w3}:
4430 match w3:
4431 case WCon{False{}, w4}:
4432 match w4:
4433 case WCon{False{}, w5}:
4434 match w5:
4435 case WCon{False{}, w6}:
4436 match w6:
4437 case WCon{False{}, w7}:
4438 match w7:
4439 case WCon{False{}, w8}:
4440 match w8:
4441 case WNil{}:
4442 {==}
4443 case WCon{True{}, w8}:
4444 match w8:
4445 case WNil{}:
4446 {==}
4447 case WCon{True{}, w7}:
4448 match w7:
4449 case WCon{False{}, w8}:
4450 match w8:
4451 case WNil{}:
4452 {==}
4453 case WCon{True{}, w8}:
4454 match w8:
4455 case WNil{}:
4456 {==}
4457 case WCon{True{}, w6}:
4458 match w6:
4459 case WCon{False{}, w7}:
4460 match w7:
4461 case WCon{False{}, w8}:
4462 match w8:
4463 case WNil{}:
4464 {==}
4465 case WCon{True{}, w8}:
4466 match w8:
4467 case WNil{}:
4468 {==}
4469 case WCon{True{}, w7}:
4470 match w7:
4471 case WCon{False{}, w8}:
4472 match w8:
4473 case WNil{}:
4474 {==}
4475 case WCon{True{}, w8}:
4476 match w8:
4477 case WNil{}:
4478 {==}
4479 case WCon{True{}, w5}:
4480 match w5:
4481 case WCon{False{}, w6}:
4482 match w6:
4483 case WCon{False{}, w7}:
4484 match w7:
4485 case WCon{False{}, w8}:
4486 match w8:
4487 case WNil{}:
4488 {==}
4489 case WCon{True{}, w8}:
4490 match w8:
4491 case WNil{}:
4492 {==}
4493 case WCon{True{}, w7}:
4494 match w7:
4495 case WCon{False{}, w8}:
4496 match w8:
4497 case WNil{}:
4498 {==}
4499 case WCon{True{}, w8}:
4500 match w8:
4501 case WNil{}:
4502 {==}
4503 case WCon{True{}, w6}:
4504 match w6:
4505 case WCon{False{}, w7}:
4506 match w7:
4507 case WCon{False{}, w8}:
4508 match w8:
4509 case WNil{}:
4510 {==}
4511 case WCon{True{}, w8}:
4512 match w8:
4513 case WNil{}:
4514 {==}
4515 case WCon{True{}, w7}:
4516 match w7:
4517 case WCon{False{}, w8}:
4518 match w8:
4519 case WNil{}:
4520 {==}
4521 case WCon{True{}, w8}:
4522 match w8:
4523 case WNil{}:
4524 {==}
4525 case WCon{True{}, w4}:
4526 match w4:
4527 case WCon{False{}, w5}:
4528 match w5:
4529 case WCon{False{}, w6}:
4530 match w6:
4531 case WCon{False{}, w7}:
4532 match w7:
4533 case WCon{False{}, w8}:
4534 match w8:
4535 case WNil{}:
4536 {==}
4537 case WCon{True{}, w8}:
4538 match w8:
4539 case WNil{}:
4540 {==}
4541 case WCon{True{}, w7}:
4542 match w7:
4543 case WCon{False{}, w8}:
4544 match w8:
4545 case WNil{}:
4546 {==}
4547 case WCon{True{}, w8}:
4548 match w8:
4549 case WNil{}:
4550 {==}
4551 case WCon{True{}, w6}:
4552 match w6:
4553 case WCon{False{}, w7}:
4554 match w7:
4555 case WCon{False{}, w8}:
4556 match w8:
4557 case WNil{}:
4558 {==}
4559 case WCon{True{}, w8}:
4560 match w8:
4561 case WNil{}:
4562 {==}
4563 case WCon{True{}, w7}:
4564 match w7:
4565 case WCon{False{}, w8}:
4566 match w8:
4567 case WNil{}:
4568 {==}
4569 case WCon{True{}, w8}:
4570 match w8:
4571 case WNil{}:
4572 {==}
4573 case WCon{True{}, w5}:
4574 match w5:
4575 case WCon{False{}, w6}:
4576 match w6:
4577 case WCon{False{}, w7}:
4578 match w7:
4579 case WCon{False{}, w8}:
4580 match w8:
4581 case WNil{}:
4582 {==}
4583 case WCon{True{}, w8}:
4584 match w8:
4585 case WNil{}:
4586 {==}
4587 case WCon{True{}, w7}:
4588 match w7:
4589 case WCon{False{}, w8}:
4590 match w8:
4591 case WNil{}:
4592 {==}
4593 case WCon{True{}, w8}:
4594 match w8:
4595 case WNil{}:
4596 {==}
4597 case WCon{True{}, w6}:
4598 match w6:
4599 case WCon{False{}, w7}:
4600 match w7:
4601 case WCon{False{}, w8}:
4602 match w8:
4603 case WNil{}:
4604 {==}
4605 case WCon{True{}, w8}:
4606 match w8:
4607 case WNil{}:
4608 {==}
4609 case WCon{True{}, w7}:
4610 match w7:
4611 case WCon{False{}, w8}:
4612 match w8:
4613 case WNil{}:
4614 {==}
4615 case WCon{True{}, w8}:
4616 match w8:
4617 case WNil{}:
4618 {==}