def aria_sb31
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
13# BEGIN GENERATED by gen/proof.py: aria
14# each S-box and its inverse undo each other on every byte
15def aria_sb31(w0: Word(8n)) -> {w0 == A.aria.sb3(A.aria.sb1(w0)) : Word(8n)}:
16 match w0:
17 case WCon{False{}, w1}:
18 match w1:
19 case WCon{False{}, w2}:
20 match w2:
21 case WCon{False{}, w3}:
22 match w3:
23 case WCon{False{}, w4}:
24 match w4:
25 case WCon{False{}, w5}:
26 match w5:
27 case WCon{False{}, w6}:
28 match w6:
29 case WCon{False{}, w7}:
30 match w7:
31 case WCon{False{}, w8}:
32 match w8:
33 case WNil{}:
34 {==}
35 case WCon{True{}, w8}:
36 match w8:
37 case WNil{}:
38 {==}
39 case WCon{True{}, w7}:
40 match w7:
41 case WCon{False{}, w8}:
42 match w8:
43 case WNil{}:
44 {==}
45 case WCon{True{}, w8}:
46 match w8:
47 case WNil{}:
48 {==}
49 case WCon{True{}, w6}:
50 match w6:
51 case WCon{False{}, w7}:
52 match w7:
53 case WCon{False{}, w8}:
54 match w8:
55 case WNil{}:
56 {==}
57 case WCon{True{}, w8}:
58 match w8:
59 case WNil{}:
60 {==}
61 case WCon{True{}, w7}:
62 match w7:
63 case WCon{False{}, w8}:
64 match w8:
65 case WNil{}:
66 {==}
67 case WCon{True{}, w8}:
68 match w8:
69 case WNil{}:
70 {==}
71 case WCon{True{}, w5}:
72 match w5:
73 case WCon{False{}, w6}:
74 match w6:
75 case WCon{False{}, w7}:
76 match w7:
77 case WCon{False{}, w8}:
78 match w8:
79 case WNil{}:
80 {==}
81 case WCon{True{}, w8}:
82 match w8:
83 case WNil{}:
84 {==}
85 case WCon{True{}, w7}:
86 match w7:
87 case WCon{False{}, w8}:
88 match w8:
89 case WNil{}:
90 {==}
91 case WCon{True{}, w8}:
92 match w8:
93 case WNil{}:
94 {==}
95 case WCon{True{}, w6}:
96 match w6:
97 case WCon{False{}, w7}:
98 match w7:
99 case WCon{False{}, w8}:
100 match w8:
101 case WNil{}:
102 {==}
103 case WCon{True{}, w8}:
104 match w8:
105 case WNil{}:
106 {==}
107 case WCon{True{}, w7}:
108 match w7:
109 case WCon{False{}, w8}:
110 match w8:
111 case WNil{}:
112 {==}
113 case WCon{True{}, w8}:
114 match w8:
115 case WNil{}:
116 {==}
117 case WCon{True{}, w4}:
118 match w4:
119 case WCon{False{}, w5}:
120 match w5:
121 case WCon{False{}, w6}:
122 match w6:
123 case WCon{False{}, w7}:
124 match w7:
125 case WCon{False{}, w8}:
126 match w8:
127 case WNil{}:
128 {==}
129 case WCon{True{}, w8}:
130 match w8:
131 case WNil{}:
132 {==}
133 case WCon{True{}, w7}:
134 match w7:
135 case WCon{False{}, w8}:
136 match w8:
137 case WNil{}:
138 {==}
139 case WCon{True{}, w8}:
140 match w8:
141 case WNil{}:
142 {==}
143 case WCon{True{}, w6}:
144 match w6:
145 case WCon{False{}, w7}:
146 match w7:
147 case WCon{False{}, w8}:
148 match w8:
149 case WNil{}:
150 {==}
151 case WCon{True{}, w8}:
152 match w8:
153 case WNil{}:
154 {==}
155 case WCon{True{}, w7}:
156 match w7:
157 case WCon{False{}, w8}:
158 match w8:
159 case WNil{}:
160 {==}
161 case WCon{True{}, w8}:
162 match w8:
163 case WNil{}:
164 {==}
165 case WCon{True{}, w5}:
166 match w5:
167 case WCon{False{}, w6}:
168 match w6:
169 case WCon{False{}, w7}:
170 match w7:
171 case WCon{False{}, w8}:
172 match w8:
173 case WNil{}:
174 {==}
175 case WCon{True{}, w8}:
176 match w8:
177 case WNil{}:
178 {==}
179 case WCon{True{}, w7}:
180 match w7:
181 case WCon{False{}, w8}:
182 match w8:
183 case WNil{}:
184 {==}
185 case WCon{True{}, w8}:
186 match w8:
187 case WNil{}:
188 {==}
189 case WCon{True{}, w6}:
190 match w6:
191 case WCon{False{}, w7}:
192 match w7:
193 case WCon{False{}, w8}:
194 match w8:
195 case WNil{}:
196 {==}
197 case WCon{True{}, w8}:
198 match w8:
199 case WNil{}:
200 {==}
201 case WCon{True{}, w7}:
202 match w7:
203 case WCon{False{}, w8}:
204 match w8:
205 case WNil{}:
206 {==}
207 case WCon{True{}, w8}:
208 match w8:
209 case WNil{}:
210 {==}
211 case WCon{True{}, w3}:
212 match w3:
213 case WCon{False{}, w4}:
214 match w4:
215 case WCon{False{}, w5}:
216 match w5:
217 case WCon{False{}, w6}:
218 match w6:
219 case WCon{False{}, w7}:
220 match w7:
221 case WCon{False{}, w8}:
222 match w8:
223 case WNil{}:
224 {==}
225 case WCon{True{}, w8}:
226 match w8:
227 case WNil{}:
228 {==}
229 case WCon{True{}, w7}:
230 match w7:
231 case WCon{False{}, w8}:
232 match w8:
233 case WNil{}:
234 {==}
235 case WCon{True{}, w8}:
236 match w8:
237 case WNil{}:
238 {==}
239 case WCon{True{}, w6}:
240 match w6:
241 case WCon{False{}, w7}:
242 match w7:
243 case WCon{False{}, w8}:
244 match w8:
245 case WNil{}:
246 {==}
247 case WCon{True{}, w8}:
248 match w8:
249 case WNil{}:
250 {==}
251 case WCon{True{}, w7}:
252 match w7:
253 case WCon{False{}, w8}:
254 match w8:
255 case WNil{}:
256 {==}
257 case WCon{True{}, w8}:
258 match w8:
259 case WNil{}:
260 {==}
261 case WCon{True{}, w5}:
262 match w5:
263 case WCon{False{}, w6}:
264 match w6:
265 case WCon{False{}, w7}:
266 match w7:
267 case WCon{False{}, w8}:
268 match w8:
269 case WNil{}:
270 {==}
271 case WCon{True{}, w8}:
272 match w8:
273 case WNil{}:
274 {==}
275 case WCon{True{}, w7}:
276 match w7:
277 case WCon{False{}, w8}:
278 match w8:
279 case WNil{}:
280 {==}
281 case WCon{True{}, w8}:
282 match w8:
283 case WNil{}:
284 {==}
285 case WCon{True{}, w6}:
286 match w6:
287 case WCon{False{}, w7}:
288 match w7:
289 case WCon{False{}, w8}:
290 match w8:
291 case WNil{}:
292 {==}
293 case WCon{True{}, w8}:
294 match w8:
295 case WNil{}:
296 {==}
297 case WCon{True{}, w7}:
298 match w7:
299 case WCon{False{}, w8}:
300 match w8:
301 case WNil{}:
302 {==}
303 case WCon{True{}, w8}:
304 match w8:
305 case WNil{}:
306 {==}
307 case WCon{True{}, w4}:
308 match w4:
309 case WCon{False{}, w5}:
310 match w5:
311 case WCon{False{}, w6}:
312 match w6:
313 case WCon{False{}, w7}:
314 match w7:
315 case WCon{False{}, w8}:
316 match w8:
317 case WNil{}:
318 {==}
319 case WCon{True{}, w8}:
320 match w8:
321 case WNil{}:
322 {==}
323 case WCon{True{}, w7}:
324 match w7:
325 case WCon{False{}, w8}:
326 match w8:
327 case WNil{}:
328 {==}
329 case WCon{True{}, w8}:
330 match w8:
331 case WNil{}:
332 {==}
333 case WCon{True{}, w6}:
334 match w6:
335 case WCon{False{}, w7}:
336 match w7:
337 case WCon{False{}, w8}:
338 match w8:
339 case WNil{}:
340 {==}
341 case WCon{True{}, w8}:
342 match w8:
343 case WNil{}:
344 {==}
345 case WCon{True{}, w7}:
346 match w7:
347 case WCon{False{}, w8}:
348 match w8:
349 case WNil{}:
350 {==}
351 case WCon{True{}, w8}:
352 match w8:
353 case WNil{}:
354 {==}
355 case WCon{True{}, w5}:
356 match w5:
357 case WCon{False{}, w6}:
358 match w6:
359 case WCon{False{}, w7}:
360 match w7:
361 case WCon{False{}, w8}:
362 match w8:
363 case WNil{}:
364 {==}
365 case WCon{True{}, w8}:
366 match w8:
367 case WNil{}:
368 {==}
369 case WCon{True{}, w7}:
370 match w7:
371 case WCon{False{}, w8}:
372 match w8:
373 case WNil{}:
374 {==}
375 case WCon{True{}, w8}:
376 match w8:
377 case WNil{}:
378 {==}
379 case WCon{True{}, w6}:
380 match w6:
381 case WCon{False{}, w7}:
382 match w7:
383 case WCon{False{}, w8}:
384 match w8:
385 case WNil{}:
386 {==}
387 case WCon{True{}, w8}:
388 match w8:
389 case WNil{}:
390 {==}
391 case WCon{True{}, w7}:
392 match w7:
393 case WCon{False{}, w8}:
394 match w8:
395 case WNil{}:
396 {==}
397 case WCon{True{}, w8}:
398 match w8:
399 case WNil{}:
400 {==}
401 case WCon{True{}, w2}:
402 match w2:
403 case WCon{False{}, w3}:
404 match w3:
405 case WCon{False{}, w4}:
406 match w4:
407 case WCon{False{}, w5}:
408 match w5:
409 case WCon{False{}, w6}:
410 match w6:
411 case WCon{False{}, w7}:
412 match w7:
413 case WCon{False{}, w8}:
414 match w8:
415 case WNil{}:
416 {==}
417 case WCon{True{}, w8}:
418 match w8:
419 case WNil{}:
420 {==}
421 case WCon{True{}, w7}:
422 match w7:
423 case WCon{False{}, w8}:
424 match w8:
425 case WNil{}:
426 {==}
427 case WCon{True{}, w8}:
428 match w8:
429 case WNil{}:
430 {==}
431 case WCon{True{}, w6}:
432 match w6:
433 case WCon{False{}, w7}:
434 match w7:
435 case WCon{False{}, w8}:
436 match w8:
437 case WNil{}:
438 {==}
439 case WCon{True{}, w8}:
440 match w8:
441 case WNil{}:
442 {==}
443 case WCon{True{}, w7}:
444 match w7:
445 case WCon{False{}, w8}:
446 match w8:
447 case WNil{}:
448 {==}
449 case WCon{True{}, w8}:
450 match w8:
451 case WNil{}:
452 {==}
453 case WCon{True{}, w5}:
454 match w5:
455 case WCon{False{}, w6}:
456 match w6:
457 case WCon{False{}, w7}:
458 match w7:
459 case WCon{False{}, w8}:
460 match w8:
461 case WNil{}:
462 {==}
463 case WCon{True{}, w8}:
464 match w8:
465 case WNil{}:
466 {==}
467 case WCon{True{}, w7}:
468 match w7:
469 case WCon{False{}, w8}:
470 match w8:
471 case WNil{}:
472 {==}
473 case WCon{True{}, w8}:
474 match w8:
475 case WNil{}:
476 {==}
477 case WCon{True{}, w6}:
478 match w6:
479 case WCon{False{}, w7}:
480 match w7:
481 case WCon{False{}, w8}:
482 match w8:
483 case WNil{}:
484 {==}
485 case WCon{True{}, w8}:
486 match w8:
487 case WNil{}:
488 {==}
489 case WCon{True{}, w7}:
490 match w7:
491 case WCon{False{}, w8}:
492 match w8:
493 case WNil{}:
494 {==}
495 case WCon{True{}, w8}:
496 match w8:
497 case WNil{}:
498 {==}
499 case WCon{True{}, w4}:
500 match w4:
501 case WCon{False{}, w5}:
502 match w5:
503 case WCon{False{}, w6}:
504 match w6:
505 case WCon{False{}, w7}:
506 match w7:
507 case WCon{False{}, w8}:
508 match w8:
509 case WNil{}:
510 {==}
511 case WCon{True{}, w8}:
512 match w8:
513 case WNil{}:
514 {==}
515 case WCon{True{}, w7}:
516 match w7:
517 case WCon{False{}, w8}:
518 match w8:
519 case WNil{}:
520 {==}
521 case WCon{True{}, w8}:
522 match w8:
523 case WNil{}:
524 {==}
525 case WCon{True{}, w6}:
526 match w6:
527 case WCon{False{}, w7}:
528 match w7:
529 case WCon{False{}, w8}:
530 match w8:
531 case WNil{}:
532 {==}
533 case WCon{True{}, w8}:
534 match w8:
535 case WNil{}:
536 {==}
537 case WCon{True{}, w7}:
538 match w7:
539 case WCon{False{}, w8}:
540 match w8:
541 case WNil{}:
542 {==}
543 case WCon{True{}, w8}:
544 match w8:
545 case WNil{}:
546 {==}
547 case WCon{True{}, w5}:
548 match w5:
549 case WCon{False{}, w6}:
550 match w6:
551 case WCon{False{}, w7}:
552 match w7:
553 case WCon{False{}, w8}:
554 match w8:
555 case WNil{}:
556 {==}
557 case WCon{True{}, w8}:
558 match w8:
559 case WNil{}:
560 {==}
561 case WCon{True{}, w7}:
562 match w7:
563 case WCon{False{}, w8}:
564 match w8:
565 case WNil{}:
566 {==}
567 case WCon{True{}, w8}:
568 match w8:
569 case WNil{}:
570 {==}
571 case WCon{True{}, w6}:
572 match w6:
573 case WCon{False{}, w7}:
574 match w7:
575 case WCon{False{}, w8}:
576 match w8:
577 case WNil{}:
578 {==}
579 case WCon{True{}, w8}:
580 match w8:
581 case WNil{}:
582 {==}
583 case WCon{True{}, w7}:
584 match w7:
585 case WCon{False{}, w8}:
586 match w8:
587 case WNil{}:
588 {==}
589 case WCon{True{}, w8}:
590 match w8:
591 case WNil{}:
592 {==}
593 case WCon{True{}, w3}:
594 match w3:
595 case WCon{False{}, w4}:
596 match w4:
597 case WCon{False{}, w5}:
598 match w5:
599 case WCon{False{}, w6}:
600 match w6:
601 case WCon{False{}, w7}:
602 match w7:
603 case WCon{False{}, w8}:
604 match w8:
605 case WNil{}:
606 {==}
607 case WCon{True{}, w8}:
608 match w8:
609 case WNil{}:
610 {==}
611 case WCon{True{}, w7}:
612 match w7:
613 case WCon{False{}, w8}:
614 match w8:
615 case WNil{}:
616 {==}
617 case WCon{True{}, w8}:
618 match w8:
619 case WNil{}:
620 {==}
621 case WCon{True{}, w6}:
622 match w6:
623 case WCon{False{}, w7}:
624 match w7:
625 case WCon{False{}, w8}:
626 match w8:
627 case WNil{}:
628 {==}
629 case WCon{True{}, w8}:
630 match w8:
631 case WNil{}:
632 {==}
633 case WCon{True{}, w7}:
634 match w7:
635 case WCon{False{}, w8}:
636 match w8:
637 case WNil{}:
638 {==}
639 case WCon{True{}, w8}:
640 match w8:
641 case WNil{}:
642 {==}
643 case WCon{True{}, w5}:
644 match w5:
645 case WCon{False{}, w6}:
646 match w6:
647 case WCon{False{}, w7}:
648 match w7:
649 case WCon{False{}, w8}:
650 match w8:
651 case WNil{}:
652 {==}
653 case WCon{True{}, w8}:
654 match w8:
655 case WNil{}:
656 {==}
657 case WCon{True{}, w7}:
658 match w7:
659 case WCon{False{}, w8}:
660 match w8:
661 case WNil{}:
662 {==}
663 case WCon{True{}, w8}:
664 match w8:
665 case WNil{}:
666 {==}
667 case WCon{True{}, w6}:
668 match w6:
669 case WCon{False{}, w7}:
670 match w7:
671 case WCon{False{}, w8}:
672 match w8:
673 case WNil{}:
674 {==}
675 case WCon{True{}, w8}:
676 match w8:
677 case WNil{}:
678 {==}
679 case WCon{True{}, w7}:
680 match w7:
681 case WCon{False{}, w8}:
682 match w8:
683 case WNil{}:
684 {==}
685 case WCon{True{}, w8}:
686 match w8:
687 case WNil{}:
688 {==}
689 case WCon{True{}, w4}:
690 match w4:
691 case WCon{False{}, w5}:
692 match w5:
693 case WCon{False{}, w6}:
694 match w6:
695 case WCon{False{}, w7}:
696 match w7:
697 case WCon{False{}, w8}:
698 match w8:
699 case WNil{}:
700 {==}
701 case WCon{True{}, w8}:
702 match w8:
703 case WNil{}:
704 {==}
705 case WCon{True{}, w7}:
706 match w7:
707 case WCon{False{}, w8}:
708 match w8:
709 case WNil{}:
710 {==}
711 case WCon{True{}, w8}:
712 match w8:
713 case WNil{}:
714 {==}
715 case WCon{True{}, w6}:
716 match w6:
717 case WCon{False{}, w7}:
718 match w7:
719 case WCon{False{}, w8}:
720 match w8:
721 case WNil{}:
722 {==}
723 case WCon{True{}, w8}:
724 match w8:
725 case WNil{}:
726 {==}
727 case WCon{True{}, w7}:
728 match w7:
729 case WCon{False{}, w8}:
730 match w8:
731 case WNil{}:
732 {==}
733 case WCon{True{}, w8}:
734 match w8:
735 case WNil{}:
736 {==}
737 case WCon{True{}, w5}:
738 match w5:
739 case WCon{False{}, w6}:
740 match w6:
741 case WCon{False{}, w7}:
742 match w7:
743 case WCon{False{}, w8}:
744 match w8:
745 case WNil{}:
746 {==}
747 case WCon{True{}, w8}:
748 match w8:
749 case WNil{}:
750 {==}
751 case WCon{True{}, w7}:
752 match w7:
753 case WCon{False{}, w8}:
754 match w8:
755 case WNil{}:
756 {==}
757 case WCon{True{}, w8}:
758 match w8:
759 case WNil{}:
760 {==}
761 case WCon{True{}, w6}:
762 match w6:
763 case WCon{False{}, w7}:
764 match w7:
765 case WCon{False{}, w8}:
766 match w8:
767 case WNil{}:
768 {==}
769 case WCon{True{}, w8}:
770 match w8:
771 case WNil{}:
772 {==}
773 case WCon{True{}, w7}:
774 match w7:
775 case WCon{False{}, w8}:
776 match w8:
777 case WNil{}:
778 {==}
779 case WCon{True{}, w8}:
780 match w8:
781 case WNil{}:
782 {==}
783 case WCon{True{}, w1}:
784 match w1:
785 case WCon{False{}, w2}:
786 match w2:
787 case WCon{False{}, w3}:
788 match w3:
789 case WCon{False{}, w4}:
790 match w4:
791 case WCon{False{}, w5}:
792 match w5:
793 case WCon{False{}, w6}:
794 match w6:
795 case WCon{False{}, w7}:
796 match w7:
797 case WCon{False{}, w8}:
798 match w8:
799 case WNil{}:
800 {==}
801 case WCon{True{}, w8}:
802 match w8:
803 case WNil{}:
804 {==}
805 case WCon{True{}, w7}:
806 match w7:
807 case WCon{False{}, w8}:
808 match w8:
809 case WNil{}:
810 {==}
811 case WCon{True{}, w8}:
812 match w8:
813 case WNil{}:
814 {==}
815 case WCon{True{}, w6}:
816 match w6:
817 case WCon{False{}, w7}:
818 match w7:
819 case WCon{False{}, w8}:
820 match w8:
821 case WNil{}:
822 {==}
823 case WCon{True{}, w8}:
824 match w8:
825 case WNil{}:
826 {==}
827 case WCon{True{}, w7}:
828 match w7:
829 case WCon{False{}, w8}:
830 match w8:
831 case WNil{}:
832 {==}
833 case WCon{True{}, w8}:
834 match w8:
835 case WNil{}:
836 {==}
837 case WCon{True{}, w5}:
838 match w5:
839 case WCon{False{}, w6}:
840 match w6:
841 case WCon{False{}, w7}:
842 match w7:
843 case WCon{False{}, w8}:
844 match w8:
845 case WNil{}:
846 {==}
847 case WCon{True{}, w8}:
848 match w8:
849 case WNil{}:
850 {==}
851 case WCon{True{}, w7}:
852 match w7:
853 case WCon{False{}, w8}:
854 match w8:
855 case WNil{}:
856 {==}
857 case WCon{True{}, w8}:
858 match w8:
859 case WNil{}:
860 {==}
861 case WCon{True{}, w6}:
862 match w6:
863 case WCon{False{}, w7}:
864 match w7:
865 case WCon{False{}, w8}:
866 match w8:
867 case WNil{}:
868 {==}
869 case WCon{True{}, w8}:
870 match w8:
871 case WNil{}:
872 {==}
873 case WCon{True{}, w7}:
874 match w7:
875 case WCon{False{}, w8}:
876 match w8:
877 case WNil{}:
878 {==}
879 case WCon{True{}, w8}:
880 match w8:
881 case WNil{}:
882 {==}
883 case WCon{True{}, w4}:
884 match w4:
885 case WCon{False{}, w5}:
886 match w5:
887 case WCon{False{}, w6}:
888 match w6:
889 case WCon{False{}, w7}:
890 match w7:
891 case WCon{False{}, w8}:
892 match w8:
893 case WNil{}:
894 {==}
895 case WCon{True{}, w8}:
896 match w8:
897 case WNil{}:
898 {==}
899 case WCon{True{}, w7}:
900 match w7:
901 case WCon{False{}, w8}:
902 match w8:
903 case WNil{}:
904 {==}
905 case WCon{True{}, w8}:
906 match w8:
907 case WNil{}:
908 {==}
909 case WCon{True{}, w6}:
910 match w6:
911 case WCon{False{}, w7}:
912 match w7:
913 case WCon{False{}, w8}:
914 match w8:
915 case WNil{}:
916 {==}
917 case WCon{True{}, w8}:
918 match w8:
919 case WNil{}:
920 {==}
921 case WCon{True{}, w7}:
922 match w7:
923 case WCon{False{}, w8}:
924 match w8:
925 case WNil{}:
926 {==}
927 case WCon{True{}, w8}:
928 match w8:
929 case WNil{}:
930 {==}
931 case WCon{True{}, w5}:
932 match w5:
933 case WCon{False{}, w6}:
934 match w6:
935 case WCon{False{}, w7}:
936 match w7:
937 case WCon{False{}, w8}:
938 match w8:
939 case WNil{}:
940 {==}
941 case WCon{True{}, w8}:
942 match w8:
943 case WNil{}:
944 {==}
945 case WCon{True{}, w7}:
946 match w7:
947 case WCon{False{}, w8}:
948 match w8:
949 case WNil{}:
950 {==}
951 case WCon{True{}, w8}:
952 match w8:
953 case WNil{}:
954 {==}
955 case WCon{True{}, w6}:
956 match w6:
957 case WCon{False{}, w7}:
958 match w7:
959 case WCon{False{}, w8}:
960 match w8:
961 case WNil{}:
962 {==}
963 case WCon{True{}, w8}:
964 match w8:
965 case WNil{}:
966 {==}
967 case WCon{True{}, w7}:
968 match w7:
969 case WCon{False{}, w8}:
970 match w8:
971 case WNil{}:
972 {==}
973 case WCon{True{}, w8}:
974 match w8:
975 case WNil{}:
976 {==}
977 case WCon{True{}, w3}:
978 match w3:
979 case WCon{False{}, w4}:
980 match w4:
981 case WCon{False{}, w5}:
982 match w5:
983 case WCon{False{}, w6}:
984 match w6:
985 case WCon{False{}, w7}:
986 match w7:
987 case WCon{False{}, w8}:
988 match w8:
989 case WNil{}:
990 {==}
991 case WCon{True{}, w8}:
992 match w8:
993 case WNil{}:
994 {==}
995 case WCon{True{}, w7}:
996 match w7:
997 case WCon{False{}, w8}:
998 match w8:
999 case WNil{}:
1000 {==}
1001 case WCon{True{}, w8}:
1002 match w8:
1003 case WNil{}:
1004 {==}
1005 case WCon{True{}, w6}:
1006 match w6:
1007 case WCon{False{}, w7}:
1008 match w7:
1009 case WCon{False{}, w8}:
1010 match w8:
1011 case WNil{}:
1012 {==}
1013 case WCon{True{}, w8}:
1014 match w8:
1015 case WNil{}:
1016 {==}
1017 case WCon{True{}, w7}:
1018 match w7:
1019 case WCon{False{}, w8}:
1020 match w8:
1021 case WNil{}:
1022 {==}
1023 case WCon{True{}, w8}:
1024 match w8:
1025 case WNil{}:
1026 {==}
1027 case WCon{True{}, w5}:
1028 match w5:
1029 case WCon{False{}, w6}:
1030 match w6:
1031 case WCon{False{}, w7}:
1032 match w7:
1033 case WCon{False{}, w8}:
1034 match w8:
1035 case WNil{}:
1036 {==}
1037 case WCon{True{}, w8}:
1038 match w8:
1039 case WNil{}:
1040 {==}
1041 case WCon{True{}, w7}:
1042 match w7:
1043 case WCon{False{}, w8}:
1044 match w8:
1045 case WNil{}:
1046 {==}
1047 case WCon{True{}, w8}:
1048 match w8:
1049 case WNil{}:
1050 {==}
1051 case WCon{True{}, w6}:
1052 match w6:
1053 case WCon{False{}, w7}:
1054 match w7:
1055 case WCon{False{}, w8}:
1056 match w8:
1057 case WNil{}:
1058 {==}
1059 case WCon{True{}, w8}:
1060 match w8:
1061 case WNil{}:
1062 {==}
1063 case WCon{True{}, w7}:
1064 match w7:
1065 case WCon{False{}, w8}:
1066 match w8:
1067 case WNil{}:
1068 {==}
1069 case WCon{True{}, w8}:
1070 match w8:
1071 case WNil{}:
1072 {==}
1073 case WCon{True{}, w4}:
1074 match w4:
1075 case WCon{False{}, w5}:
1076 match w5:
1077 case WCon{False{}, w6}:
1078 match w6:
1079 case WCon{False{}, w7}:
1080 match w7:
1081 case WCon{False{}, w8}:
1082 match w8:
1083 case WNil{}:
1084 {==}
1085 case WCon{True{}, w8}:
1086 match w8:
1087 case WNil{}:
1088 {==}
1089 case WCon{True{}, w7}:
1090 match w7:
1091 case WCon{False{}, w8}:
1092 match w8:
1093 case WNil{}:
1094 {==}
1095 case WCon{True{}, w8}:
1096 match w8:
1097 case WNil{}:
1098 {==}
1099 case WCon{True{}, w6}:
1100 match w6:
1101 case WCon{False{}, w7}:
1102 match w7:
1103 case WCon{False{}, w8}:
1104 match w8:
1105 case WNil{}:
1106 {==}
1107 case WCon{True{}, w8}:
1108 match w8:
1109 case WNil{}:
1110 {==}
1111 case WCon{True{}, w7}:
1112 match w7:
1113 case WCon{False{}, w8}:
1114 match w8:
1115 case WNil{}:
1116 {==}
1117 case WCon{True{}, w8}:
1118 match w8:
1119 case WNil{}:
1120 {==}
1121 case WCon{True{}, w5}:
1122 match w5:
1123 case WCon{False{}, w6}:
1124 match w6:
1125 case WCon{False{}, w7}:
1126 match w7:
1127 case WCon{False{}, w8}:
1128 match w8:
1129 case WNil{}:
1130 {==}
1131 case WCon{True{}, w8}:
1132 match w8:
1133 case WNil{}:
1134 {==}
1135 case WCon{True{}, w7}:
1136 match w7:
1137 case WCon{False{}, w8}:
1138 match w8:
1139 case WNil{}:
1140 {==}
1141 case WCon{True{}, w8}:
1142 match w8:
1143 case WNil{}:
1144 {==}
1145 case WCon{True{}, w6}:
1146 match w6:
1147 case WCon{False{}, w7}:
1148 match w7:
1149 case WCon{False{}, w8}:
1150 match w8:
1151 case WNil{}:
1152 {==}
1153 case WCon{True{}, w8}:
1154 match w8:
1155 case WNil{}:
1156 {==}
1157 case WCon{True{}, w7}:
1158 match w7:
1159 case WCon{False{}, w8}:
1160 match w8:
1161 case WNil{}:
1162 {==}
1163 case WCon{True{}, w8}:
1164 match w8:
1165 case WNil{}:
1166 {==}
1167 case WCon{True{}, w2}:
1168 match w2:
1169 case WCon{False{}, w3}:
1170 match w3:
1171 case WCon{False{}, w4}:
1172 match w4:
1173 case WCon{False{}, w5}:
1174 match w5:
1175 case WCon{False{}, w6}:
1176 match w6:
1177 case WCon{False{}, w7}:
1178 match w7:
1179 case WCon{False{}, w8}:
1180 match w8:
1181 case WNil{}:
1182 {==}
1183 case WCon{True{}, w8}:
1184 match w8:
1185 case WNil{}:
1186 {==}
1187 case WCon{True{}, w7}:
1188 match w7:
1189 case WCon{False{}, w8}:
1190 match w8:
1191 case WNil{}:
1192 {==}
1193 case WCon{True{}, w8}:
1194 match w8:
1195 case WNil{}:
1196 {==}
1197 case WCon{True{}, w6}:
1198 match w6:
1199 case WCon{False{}, w7}:
1200 match w7:
1201 case WCon{False{}, w8}:
1202 match w8:
1203 case WNil{}:
1204 {==}
1205 case WCon{True{}, w8}:
1206 match w8:
1207 case WNil{}:
1208 {==}
1209 case WCon{True{}, w7}:
1210 match w7:
1211 case WCon{False{}, w8}:
1212 match w8:
1213 case WNil{}:
1214 {==}
1215 case WCon{True{}, w8}:
1216 match w8:
1217 case WNil{}:
1218 {==}
1219 case WCon{True{}, w5}:
1220 match w5:
1221 case WCon{False{}, w6}:
1222 match w6:
1223 case WCon{False{}, w7}:
1224 match w7:
1225 case WCon{False{}, w8}:
1226 match w8:
1227 case WNil{}:
1228 {==}
1229 case WCon{True{}, w8}:
1230 match w8:
1231 case WNil{}:
1232 {==}
1233 case WCon{True{}, w7}:
1234 match w7:
1235 case WCon{False{}, w8}:
1236 match w8:
1237 case WNil{}:
1238 {==}
1239 case WCon{True{}, w8}:
1240 match w8:
1241 case WNil{}:
1242 {==}
1243 case WCon{True{}, w6}:
1244 match w6:
1245 case WCon{False{}, w7}:
1246 match w7:
1247 case WCon{False{}, w8}:
1248 match w8:
1249 case WNil{}:
1250 {==}
1251 case WCon{True{}, w8}:
1252 match w8:
1253 case WNil{}:
1254 {==}
1255 case WCon{True{}, w7}:
1256 match w7:
1257 case WCon{False{}, w8}:
1258 match w8:
1259 case WNil{}:
1260 {==}
1261 case WCon{True{}, w8}:
1262 match w8:
1263 case WNil{}:
1264 {==}
1265 case WCon{True{}, w4}:
1266 match w4:
1267 case WCon{False{}, w5}:
1268 match w5:
1269 case WCon{False{}, w6}:
1270 match w6:
1271 case WCon{False{}, w7}:
1272 match w7:
1273 case WCon{False{}, w8}:
1274 match w8:
1275 case WNil{}:
1276 {==}
1277 case WCon{True{}, w8}:
1278 match w8:
1279 case WNil{}:
1280 {==}
1281 case WCon{True{}, w7}:
1282 match w7:
1283 case WCon{False{}, w8}:
1284 match w8:
1285 case WNil{}:
1286 {==}
1287 case WCon{True{}, w8}:
1288 match w8:
1289 case WNil{}:
1290 {==}
1291 case WCon{True{}, w6}:
1292 match w6:
1293 case WCon{False{}, w7}:
1294 match w7:
1295 case WCon{False{}, w8}:
1296 match w8:
1297 case WNil{}:
1298 {==}
1299 case WCon{True{}, w8}:
1300 match w8:
1301 case WNil{}:
1302 {==}
1303 case WCon{True{}, w7}:
1304 match w7:
1305 case WCon{False{}, w8}:
1306 match w8:
1307 case WNil{}:
1308 {==}
1309 case WCon{True{}, w8}:
1310 match w8:
1311 case WNil{}:
1312 {==}
1313 case WCon{True{}, w5}:
1314 match w5:
1315 case WCon{False{}, w6}:
1316 match w6:
1317 case WCon{False{}, w7}:
1318 match w7:
1319 case WCon{False{}, w8}:
1320 match w8:
1321 case WNil{}:
1322 {==}
1323 case WCon{True{}, w8}:
1324 match w8:
1325 case WNil{}:
1326 {==}
1327 case WCon{True{}, w7}:
1328 match w7:
1329 case WCon{False{}, w8}:
1330 match w8:
1331 case WNil{}:
1332 {==}
1333 case WCon{True{}, w8}:
1334 match w8:
1335 case WNil{}:
1336 {==}
1337 case WCon{True{}, w6}:
1338 match w6:
1339 case WCon{False{}, w7}:
1340 match w7:
1341 case WCon{False{}, w8}:
1342 match w8:
1343 case WNil{}:
1344 {==}
1345 case WCon{True{}, w8}:
1346 match w8:
1347 case WNil{}:
1348 {==}
1349 case WCon{True{}, w7}:
1350 match w7:
1351 case WCon{False{}, w8}:
1352 match w8:
1353 case WNil{}:
1354 {==}
1355 case WCon{True{}, w8}:
1356 match w8:
1357 case WNil{}:
1358 {==}
1359 case WCon{True{}, w3}:
1360 match w3:
1361 case WCon{False{}, w4}:
1362 match w4:
1363 case WCon{False{}, w5}:
1364 match w5:
1365 case WCon{False{}, w6}:
1366 match w6:
1367 case WCon{False{}, w7}:
1368 match w7:
1369 case WCon{False{}, w8}:
1370 match w8:
1371 case WNil{}:
1372 {==}
1373 case WCon{True{}, w8}:
1374 match w8:
1375 case WNil{}:
1376 {==}
1377 case WCon{True{}, w7}:
1378 match w7:
1379 case WCon{False{}, w8}:
1380 match w8:
1381 case WNil{}:
1382 {==}
1383 case WCon{True{}, w8}:
1384 match w8:
1385 case WNil{}:
1386 {==}
1387 case WCon{True{}, w6}:
1388 match w6:
1389 case WCon{False{}, w7}:
1390 match w7:
1391 case WCon{False{}, w8}:
1392 match w8:
1393 case WNil{}:
1394 {==}
1395 case WCon{True{}, w8}:
1396 match w8:
1397 case WNil{}:
1398 {==}
1399 case WCon{True{}, w7}:
1400 match w7:
1401 case WCon{False{}, w8}:
1402 match w8:
1403 case WNil{}:
1404 {==}
1405 case WCon{True{}, w8}:
1406 match w8:
1407 case WNil{}:
1408 {==}
1409 case WCon{True{}, w5}:
1410 match w5:
1411 case WCon{False{}, w6}:
1412 match w6:
1413 case WCon{False{}, w7}:
1414 match w7:
1415 case WCon{False{}, w8}:
1416 match w8:
1417 case WNil{}:
1418 {==}
1419 case WCon{True{}, w8}:
1420 match w8:
1421 case WNil{}:
1422 {==}
1423 case WCon{True{}, w7}:
1424 match w7:
1425 case WCon{False{}, w8}:
1426 match w8:
1427 case WNil{}:
1428 {==}
1429 case WCon{True{}, w8}:
1430 match w8:
1431 case WNil{}:
1432 {==}
1433 case WCon{True{}, w6}:
1434 match w6:
1435 case WCon{False{}, w7}:
1436 match w7:
1437 case WCon{False{}, w8}:
1438 match w8:
1439 case WNil{}:
1440 {==}
1441 case WCon{True{}, w8}:
1442 match w8:
1443 case WNil{}:
1444 {==}
1445 case WCon{True{}, w7}:
1446 match w7:
1447 case WCon{False{}, w8}:
1448 match w8:
1449 case WNil{}:
1450 {==}
1451 case WCon{True{}, w8}:
1452 match w8:
1453 case WNil{}:
1454 {==}
1455 case WCon{True{}, w4}:
1456 match w4:
1457 case WCon{False{}, w5}:
1458 match w5:
1459 case WCon{False{}, w6}:
1460 match w6:
1461 case WCon{False{}, w7}:
1462 match w7:
1463 case WCon{False{}, w8}:
1464 match w8:
1465 case WNil{}:
1466 {==}
1467 case WCon{True{}, w8}:
1468 match w8:
1469 case WNil{}:
1470 {==}
1471 case WCon{True{}, w7}:
1472 match w7:
1473 case WCon{False{}, w8}:
1474 match w8:
1475 case WNil{}:
1476 {==}
1477 case WCon{True{}, w8}:
1478 match w8:
1479 case WNil{}:
1480 {==}
1481 case WCon{True{}, w6}:
1482 match w6:
1483 case WCon{False{}, w7}:
1484 match w7:
1485 case WCon{False{}, w8}:
1486 match w8:
1487 case WNil{}:
1488 {==}
1489 case WCon{True{}, w8}:
1490 match w8:
1491 case WNil{}:
1492 {==}
1493 case WCon{True{}, w7}:
1494 match w7:
1495 case WCon{False{}, w8}:
1496 match w8:
1497 case WNil{}:
1498 {==}
1499 case WCon{True{}, w8}:
1500 match w8:
1501 case WNil{}:
1502 {==}
1503 case WCon{True{}, w5}:
1504 match w5:
1505 case WCon{False{}, w6}:
1506 match w6:
1507 case WCon{False{}, w7}:
1508 match w7:
1509 case WCon{False{}, w8}:
1510 match w8:
1511 case WNil{}:
1512 {==}
1513 case WCon{True{}, w8}:
1514 match w8:
1515 case WNil{}:
1516 {==}
1517 case WCon{True{}, w7}:
1518 match w7:
1519 case WCon{False{}, w8}:
1520 match w8:
1521 case WNil{}:
1522 {==}
1523 case WCon{True{}, w8}:
1524 match w8:
1525 case WNil{}:
1526 {==}
1527 case WCon{True{}, w6}:
1528 match w6:
1529 case WCon{False{}, w7}:
1530 match w7:
1531 case WCon{False{}, w8}:
1532 match w8:
1533 case WNil{}:
1534 {==}
1535 case WCon{True{}, w8}:
1536 match w8:
1537 case WNil{}:
1538 {==}
1539 case WCon{True{}, w7}:
1540 match w7:
1541 case WCon{False{}, w8}:
1542 match w8:
1543 case WNil{}:
1544 {==}
1545 case WCon{True{}, w8}:
1546 match w8:
1547 case WNil{}:
1548 {==}