proof_tab_cases.bend
bend-osdev-gf@0.1.1.0 · 4,212 lines · 51 definitions
1
2
3
4
5import Base
6import bend-osdev-array@0.1.0.1/array.bend as A
7import bend-osdev-gf@0.1.1.0/gf.bend as G
8import bend-osdev-gf@0.1.1.0/tables.bend as T
9import bend-osdev-gf@0.1.1.0/proof_tab.bend as GT
10
11
12def gc.elt_bits(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, +b5: Bool, +b6: Bool, +b7: Bool, +r: Word(24n)) -> {G.Gf8.elt(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, r}}}}}}}}}) == G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}) : U32}:
13 {==}
14
15
16def gc.isz.bits.s111(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}) : Bool}:
17 match b0:
18 case True{}:
19 match b1:
20 case True{}:
21 match b2:
22 case True{}:
23 match b3:
24 case True{}:
25 match b4:
26 case True{}:
27 {==}
28 case False{}:
29 {==}
30 case False{}:
31 match b4:
32 case True{}:
33 {==}
34 case False{}:
35 {==}
36 case False{}:
37 match b3:
38 case True{}:
39 match b4:
40 case True{}:
41 {==}
42 case False{}:
43 {==}
44 case False{}:
45 match b4:
46 case True{}:
47 {==}
48 case False{}:
49 {==}
50 case False{}:
51 match b2:
52 case True{}:
53 match b3:
54 case True{}:
55 match b4:
56 case True{}:
57 {==}
58 case False{}:
59 {==}
60 case False{}:
61 match b4:
62 case True{}:
63 {==}
64 case False{}:
65 {==}
66 case False{}:
67 match b3:
68 case True{}:
69 match b4:
70 case True{}:
71 {==}
72 case False{}:
73 {==}
74 case False{}:
75 match b4:
76 case True{}:
77 {==}
78 case False{}:
79 {==}
80 case False{}:
81 match b1:
82 case True{}:
83 match b2:
84 case True{}:
85 match b3:
86 case True{}:
87 match b4:
88 case True{}:
89 {==}
90 case False{}:
91 {==}
92 case False{}:
93 match b4:
94 case True{}:
95 {==}
96 case False{}:
97 {==}
98 case False{}:
99 match b3:
100 case True{}:
101 match b4:
102 case True{}:
103 {==}
104 case False{}:
105 {==}
106 case False{}:
107 match b4:
108 case True{}:
109 {==}
110 case False{}:
111 {==}
112 case False{}:
113 match b2:
114 case True{}:
115 match b3:
116 case True{}:
117 match b4:
118 case True{}:
119 {==}
120 case False{}:
121 {==}
122 case False{}:
123 match b4:
124 case True{}:
125 {==}
126 case False{}:
127 {==}
128 case False{}:
129 match b3:
130 case True{}:
131 match b4:
132 case True{}:
133 {==}
134 case False{}:
135 {==}
136 case False{}:
137 match b4:
138 case True{}:
139 {==}
140 case False{}:
141 {==}
142
143def gc.isz.bits.s011(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}) : Bool}:
144 match b0:
145 case True{}:
146 match b1:
147 case True{}:
148 match b2:
149 case True{}:
150 match b3:
151 case True{}:
152 match b4:
153 case True{}:
154 {==}
155 case False{}:
156 {==}
157 case False{}:
158 match b4:
159 case True{}:
160 {==}
161 case False{}:
162 {==}
163 case False{}:
164 match b3:
165 case True{}:
166 match b4:
167 case True{}:
168 {==}
169 case False{}:
170 {==}
171 case False{}:
172 match b4:
173 case True{}:
174 {==}
175 case False{}:
176 {==}
177 case False{}:
178 match b2:
179 case True{}:
180 match b3:
181 case True{}:
182 match b4:
183 case True{}:
184 {==}
185 case False{}:
186 {==}
187 case False{}:
188 match b4:
189 case True{}:
190 {==}
191 case False{}:
192 {==}
193 case False{}:
194 match b3:
195 case True{}:
196 match b4:
197 case True{}:
198 {==}
199 case False{}:
200 {==}
201 case False{}:
202 match b4:
203 case True{}:
204 {==}
205 case False{}:
206 {==}
207 case False{}:
208 match b1:
209 case True{}:
210 match b2:
211 case True{}:
212 match b3:
213 case True{}:
214 match b4:
215 case True{}:
216 {==}
217 case False{}:
218 {==}
219 case False{}:
220 match b4:
221 case True{}:
222 {==}
223 case False{}:
224 {==}
225 case False{}:
226 match b3:
227 case True{}:
228 match b4:
229 case True{}:
230 {==}
231 case False{}:
232 {==}
233 case False{}:
234 match b4:
235 case True{}:
236 {==}
237 case False{}:
238 {==}
239 case False{}:
240 match b2:
241 case True{}:
242 match b3:
243 case True{}:
244 match b4:
245 case True{}:
246 {==}
247 case False{}:
248 {==}
249 case False{}:
250 match b4:
251 case True{}:
252 {==}
253 case False{}:
254 {==}
255 case False{}:
256 match b3:
257 case True{}:
258 match b4:
259 case True{}:
260 {==}
261 case False{}:
262 {==}
263 case False{}:
264 match b4:
265 case True{}:
266 {==}
267 case False{}:
268 {==}
269
270def gc.isz.bits.s101(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}) : Bool}:
271 match b0:
272 case True{}:
273 match b1:
274 case True{}:
275 match b2:
276 case True{}:
277 match b3:
278 case True{}:
279 match b4:
280 case True{}:
281 {==}
282 case False{}:
283 {==}
284 case False{}:
285 match b4:
286 case True{}:
287 {==}
288 case False{}:
289 {==}
290 case False{}:
291 match b3:
292 case True{}:
293 match b4:
294 case True{}:
295 {==}
296 case False{}:
297 {==}
298 case False{}:
299 match b4:
300 case True{}:
301 {==}
302 case False{}:
303 {==}
304 case False{}:
305 match b2:
306 case True{}:
307 match b3:
308 case True{}:
309 match b4:
310 case True{}:
311 {==}
312 case False{}:
313 {==}
314 case False{}:
315 match b4:
316 case True{}:
317 {==}
318 case False{}:
319 {==}
320 case False{}:
321 match b3:
322 case True{}:
323 match b4:
324 case True{}:
325 {==}
326 case False{}:
327 {==}
328 case False{}:
329 match b4:
330 case True{}:
331 {==}
332 case False{}:
333 {==}
334 case False{}:
335 match b1:
336 case True{}:
337 match b2:
338 case True{}:
339 match b3:
340 case True{}:
341 match b4:
342 case True{}:
343 {==}
344 case False{}:
345 {==}
346 case False{}:
347 match b4:
348 case True{}:
349 {==}
350 case False{}:
351 {==}
352 case False{}:
353 match b3:
354 case True{}:
355 match b4:
356 case True{}:
357 {==}
358 case False{}:
359 {==}
360 case False{}:
361 match b4:
362 case True{}:
363 {==}
364 case False{}:
365 {==}
366 case False{}:
367 match b2:
368 case True{}:
369 match b3:
370 case True{}:
371 match b4:
372 case True{}:
373 {==}
374 case False{}:
375 {==}
376 case False{}:
377 match b4:
378 case True{}:
379 {==}
380 case False{}:
381 {==}
382 case False{}:
383 match b3:
384 case True{}:
385 match b4:
386 case True{}:
387 {==}
388 case False{}:
389 {==}
390 case False{}:
391 match b4:
392 case True{}:
393 {==}
394 case False{}:
395 {==}
396
397def gc.isz.bits.s001(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}) : Bool}:
398 match b0:
399 case True{}:
400 match b1:
401 case True{}:
402 match b2:
403 case True{}:
404 match b3:
405 case True{}:
406 match b4:
407 case True{}:
408 {==}
409 case False{}:
410 {==}
411 case False{}:
412 match b4:
413 case True{}:
414 {==}
415 case False{}:
416 {==}
417 case False{}:
418 match b3:
419 case True{}:
420 match b4:
421 case True{}:
422 {==}
423 case False{}:
424 {==}
425 case False{}:
426 match b4:
427 case True{}:
428 {==}
429 case False{}:
430 {==}
431 case False{}:
432 match b2:
433 case True{}:
434 match b3:
435 case True{}:
436 match b4:
437 case True{}:
438 {==}
439 case False{}:
440 {==}
441 case False{}:
442 match b4:
443 case True{}:
444 {==}
445 case False{}:
446 {==}
447 case False{}:
448 match b3:
449 case True{}:
450 match b4:
451 case True{}:
452 {==}
453 case False{}:
454 {==}
455 case False{}:
456 match b4:
457 case True{}:
458 {==}
459 case False{}:
460 {==}
461 case False{}:
462 match b1:
463 case True{}:
464 match b2:
465 case True{}:
466 match b3:
467 case True{}:
468 match b4:
469 case True{}:
470 {==}
471 case False{}:
472 {==}
473 case False{}:
474 match b4:
475 case True{}:
476 {==}
477 case False{}:
478 {==}
479 case False{}:
480 match b3:
481 case True{}:
482 match b4:
483 case True{}:
484 {==}
485 case False{}:
486 {==}
487 case False{}:
488 match b4:
489 case True{}:
490 {==}
491 case False{}:
492 {==}
493 case False{}:
494 match b2:
495 case True{}:
496 match b3:
497 case True{}:
498 match b4:
499 case True{}:
500 {==}
501 case False{}:
502 {==}
503 case False{}:
504 match b4:
505 case True{}:
506 {==}
507 case False{}:
508 {==}
509 case False{}:
510 match b3:
511 case True{}:
512 match b4:
513 case True{}:
514 {==}
515 case False{}:
516 {==}
517 case False{}:
518 match b4:
519 case True{}:
520 {==}
521 case False{}:
522 {==}
523
524def gc.isz.bits.s110(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}) : Bool}:
525 match b0:
526 case True{}:
527 match b1:
528 case True{}:
529 match b2:
530 case True{}:
531 match b3:
532 case True{}:
533 match b4:
534 case True{}:
535 {==}
536 case False{}:
537 {==}
538 case False{}:
539 match b4:
540 case True{}:
541 {==}
542 case False{}:
543 {==}
544 case False{}:
545 match b3:
546 case True{}:
547 match b4:
548 case True{}:
549 {==}
550 case False{}:
551 {==}
552 case False{}:
553 match b4:
554 case True{}:
555 {==}
556 case False{}:
557 {==}
558 case False{}:
559 match b2:
560 case True{}:
561 match b3:
562 case True{}:
563 match b4:
564 case True{}:
565 {==}
566 case False{}:
567 {==}
568 case False{}:
569 match b4:
570 case True{}:
571 {==}
572 case False{}:
573 {==}
574 case False{}:
575 match b3:
576 case True{}:
577 match b4:
578 case True{}:
579 {==}
580 case False{}:
581 {==}
582 case False{}:
583 match b4:
584 case True{}:
585 {==}
586 case False{}:
587 {==}
588 case False{}:
589 match b1:
590 case True{}:
591 match b2:
592 case True{}:
593 match b3:
594 case True{}:
595 match b4:
596 case True{}:
597 {==}
598 case False{}:
599 {==}
600 case False{}:
601 match b4:
602 case True{}:
603 {==}
604 case False{}:
605 {==}
606 case False{}:
607 match b3:
608 case True{}:
609 match b4:
610 case True{}:
611 {==}
612 case False{}:
613 {==}
614 case False{}:
615 match b4:
616 case True{}:
617 {==}
618 case False{}:
619 {==}
620 case False{}:
621 match b2:
622 case True{}:
623 match b3:
624 case True{}:
625 match b4:
626 case True{}:
627 {==}
628 case False{}:
629 {==}
630 case False{}:
631 match b4:
632 case True{}:
633 {==}
634 case False{}:
635 {==}
636 case False{}:
637 match b3:
638 case True{}:
639 match b4:
640 case True{}:
641 {==}
642 case False{}:
643 {==}
644 case False{}:
645 match b4:
646 case True{}:
647 {==}
648 case False{}:
649 {==}
650
651def gc.isz.bits.s010(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}}) : Bool}:
652 match b0:
653 case True{}:
654 match b1:
655 case True{}:
656 match b2:
657 case True{}:
658 match b3:
659 case True{}:
660 match b4:
661 case True{}:
662 {==}
663 case False{}:
664 {==}
665 case False{}:
666 match b4:
667 case True{}:
668 {==}
669 case False{}:
670 {==}
671 case False{}:
672 match b3:
673 case True{}:
674 match b4:
675 case True{}:
676 {==}
677 case False{}:
678 {==}
679 case False{}:
680 match b4:
681 case True{}:
682 {==}
683 case False{}:
684 {==}
685 case False{}:
686 match b2:
687 case True{}:
688 match b3:
689 case True{}:
690 match b4:
691 case True{}:
692 {==}
693 case False{}:
694 {==}
695 case False{}:
696 match b4:
697 case True{}:
698 {==}
699 case False{}:
700 {==}
701 case False{}:
702 match b3:
703 case True{}:
704 match b4:
705 case True{}:
706 {==}
707 case False{}:
708 {==}
709 case False{}:
710 match b4:
711 case True{}:
712 {==}
713 case False{}:
714 {==}
715 case False{}:
716 match b1:
717 case True{}:
718 match b2:
719 case True{}:
720 match b3:
721 case True{}:
722 match b4:
723 case True{}:
724 {==}
725 case False{}:
726 {==}
727 case False{}:
728 match b4:
729 case True{}:
730 {==}
731 case False{}:
732 {==}
733 case False{}:
734 match b3:
735 case True{}:
736 match b4:
737 case True{}:
738 {==}
739 case False{}:
740 {==}
741 case False{}:
742 match b4:
743 case True{}:
744 {==}
745 case False{}:
746 {==}
747 case False{}:
748 match b2:
749 case True{}:
750 match b3:
751 case True{}:
752 match b4:
753 case True{}:
754 {==}
755 case False{}:
756 {==}
757 case False{}:
758 match b4:
759 case True{}:
760 {==}
761 case False{}:
762 {==}
763 case False{}:
764 match b3:
765 case True{}:
766 match b4:
767 case True{}:
768 {==}
769 case False{}:
770 {==}
771 case False{}:
772 match b4:
773 case True{}:
774 {==}
775 case False{}:
776 {==}
777
778def gc.isz.bits.s100(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}) : Bool}:
779 match b0:
780 case True{}:
781 match b1:
782 case True{}:
783 match b2:
784 case True{}:
785 match b3:
786 case True{}:
787 match b4:
788 case True{}:
789 {==}
790 case False{}:
791 {==}
792 case False{}:
793 match b4:
794 case True{}:
795 {==}
796 case False{}:
797 {==}
798 case False{}:
799 match b3:
800 case True{}:
801 match b4:
802 case True{}:
803 {==}
804 case False{}:
805 {==}
806 case False{}:
807 match b4:
808 case True{}:
809 {==}
810 case False{}:
811 {==}
812 case False{}:
813 match b2:
814 case True{}:
815 match b3:
816 case True{}:
817 match b4:
818 case True{}:
819 {==}
820 case False{}:
821 {==}
822 case False{}:
823 match b4:
824 case True{}:
825 {==}
826 case False{}:
827 {==}
828 case False{}:
829 match b3:
830 case True{}:
831 match b4:
832 case True{}:
833 {==}
834 case False{}:
835 {==}
836 case False{}:
837 match b4:
838 case True{}:
839 {==}
840 case False{}:
841 {==}
842 case False{}:
843 match b1:
844 case True{}:
845 match b2:
846 case True{}:
847 match b3:
848 case True{}:
849 match b4:
850 case True{}:
851 {==}
852 case False{}:
853 {==}
854 case False{}:
855 match b4:
856 case True{}:
857 {==}
858 case False{}:
859 {==}
860 case False{}:
861 match b3:
862 case True{}:
863 match b4:
864 case True{}:
865 {==}
866 case False{}:
867 {==}
868 case False{}:
869 match b4:
870 case True{}:
871 {==}
872 case False{}:
873 {==}
874 case False{}:
875 match b2:
876 case True{}:
877 match b3:
878 case True{}:
879 match b4:
880 case True{}:
881 {==}
882 case False{}:
883 {==}
884 case False{}:
885 match b4:
886 case True{}:
887 {==}
888 case False{}:
889 {==}
890 case False{}:
891 match b3:
892 case True{}:
893 match b4:
894 case True{}:
895 {==}
896 case False{}:
897 {==}
898 case False{}:
899 match b4:
900 case True{}:
901 {==}
902 case False{}:
903 {==}
904
905def gc.isz.bits.s000(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}}) : Bool}:
906 match b0:
907 case True{}:
908 match b1:
909 case True{}:
910 match b2:
911 case True{}:
912 match b3:
913 case True{}:
914 match b4:
915 case True{}:
916 {==}
917 case False{}:
918 {==}
919 case False{}:
920 match b4:
921 case True{}:
922 {==}
923 case False{}:
924 {==}
925 case False{}:
926 match b3:
927 case True{}:
928 match b4:
929 case True{}:
930 {==}
931 case False{}:
932 {==}
933 case False{}:
934 match b4:
935 case True{}:
936 {==}
937 case False{}:
938 {==}
939 case False{}:
940 match b2:
941 case True{}:
942 match b3:
943 case True{}:
944 match b4:
945 case True{}:
946 {==}
947 case False{}:
948 {==}
949 case False{}:
950 match b4:
951 case True{}:
952 {==}
953 case False{}:
954 {==}
955 case False{}:
956 match b3:
957 case True{}:
958 match b4:
959 case True{}:
960 {==}
961 case False{}:
962 {==}
963 case False{}:
964 match b4:
965 case True{}:
966 {==}
967 case False{}:
968 {==}
969 case False{}:
970 match b1:
971 case True{}:
972 match b2:
973 case True{}:
974 match b3:
975 case True{}:
976 match b4:
977 case True{}:
978 {==}
979 case False{}:
980 {==}
981 case False{}:
982 match b4:
983 case True{}:
984 {==}
985 case False{}:
986 {==}
987 case False{}:
988 match b3:
989 case True{}:
990 match b4:
991 case True{}:
992 {==}
993 case False{}:
994 {==}
995 case False{}:
996 match b4:
997 case True{}:
998 {==}
999 case False{}:
1000 {==}
1001 case False{}:
1002 match b2:
1003 case True{}:
1004 match b3:
1005 case True{}:
1006 match b4:
1007 case True{}:
1008 {==}
1009 case False{}:
1010 {==}
1011 case False{}:
1012 match b4:
1013 case True{}:
1014 {==}
1015 case False{}:
1016 {==}
1017 case False{}:
1018 match b3:
1019 case True{}:
1020 match b4:
1021 case True{}:
1022 {==}
1023 case False{}:
1024 {==}
1025 case False{}:
1026 match b4:
1027 case True{}:
1028 {==}
1029 case False{}:
1030 {==}
1031
1032def gc.isz.bits(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, +b5: Bool, +b6: Bool, +b7: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}) : Bool}:
1033 match b5 b6 b7:
1034 case True{} True{} True{}:
1035 gc.isz.bits.s111(b0, b1, b2, b3, b4)
1036 case True{} True{} False{}:
1037 gc.isz.bits.s011(b0, b1, b2, b3, b4)
1038 case True{} False{} True{}:
1039 gc.isz.bits.s101(b0, b1, b2, b3, b4)
1040 case True{} False{} False{}:
1041 gc.isz.bits.s001(b0, b1, b2, b3, b4)
1042 case False{} True{} True{}:
1043 gc.isz.bits.s110(b0, b1, b2, b3, b4)
1044 case False{} True{} False{}:
1045 gc.isz.bits.s010(b0, b1, b2, b3, b4)
1046 case False{} False{} True{}:
1047 gc.isz.bits.s100(b0, b1, b2, b3, b4)
1048 case False{} False{} False{}:
1049 gc.isz.bits.s000(b0, b1, b2, b3, b4)
1050
1051def gc.isz(+a: U32) -> {U32.is_eq(G.Gf8.elt(a), 0) == G.Gf8.is_zero(a) : Bool}:
1052 match a:
1053 case U32{WCon{+b0, WCon{+b1, WCon{+b2, WCon{+b3, WCon{+b4, WCon{+b5, WCon{+b6, WCon{+b7, +r}}}}}}}}}:
1054 %Equal.sym(U32, G.Gf8.elt(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, r}}}}}}}}}), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}), gc.elt_bits(b0, b1, b2, b3, b4, b5, b6, b7, r)) : {U32.is_eq(_, 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}) : Bool}
1055 gc.isz.bits(b0, b1, b2, b3, b4, b5, b6, b7)
1056
1057
1058def gc.elt0.s111(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}) == 0 : U32}:
1059 match b0:
1060 case True{}:
1061 match b1:
1062 case True{}:
1063 match b2:
1064 case True{}:
1065 match b3:
1066 case True{}:
1067 match b4:
1068 case True{}:
1069 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1070 case False{}:
1071 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1072 case False{}:
1073 match b4:
1074 case True{}:
1075 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1076 case False{}:
1077 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1078 case False{}:
1079 match b3:
1080 case True{}:
1081 match b4:
1082 case True{}:
1083 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1084 case False{}:
1085 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1086 case False{}:
1087 match b4:
1088 case True{}:
1089 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1090 case False{}:
1091 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1092 case False{}:
1093 match b2:
1094 case True{}:
1095 match b3:
1096 case True{}:
1097 match b4:
1098 case True{}:
1099 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1100 case False{}:
1101 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1102 case False{}:
1103 match b4:
1104 case True{}:
1105 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1106 case False{}:
1107 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1108 case False{}:
1109 match b3:
1110 case True{}:
1111 match b4:
1112 case True{}:
1113 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1114 case False{}:
1115 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1116 case False{}:
1117 match b4:
1118 case True{}:
1119 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1120 case False{}:
1121 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1122 case False{}:
1123 match b1:
1124 case True{}:
1125 match b2:
1126 case True{}:
1127 match b3:
1128 case True{}:
1129 match b4:
1130 case True{}:
1131 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1132 case False{}:
1133 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1134 case False{}:
1135 match b4:
1136 case True{}:
1137 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1138 case False{}:
1139 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1140 case False{}:
1141 match b3:
1142 case True{}:
1143 match b4:
1144 case True{}:
1145 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1146 case False{}:
1147 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1148 case False{}:
1149 match b4:
1150 case True{}:
1151 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1152 case False{}:
1153 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1154 case False{}:
1155 match b2:
1156 case True{}:
1157 match b3:
1158 case True{}:
1159 match b4:
1160 case True{}:
1161 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1162 case False{}:
1163 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1164 case False{}:
1165 match b4:
1166 case True{}:
1167 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1168 case False{}:
1169 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1170 case False{}:
1171 match b3:
1172 case True{}:
1173 match b4:
1174 case True{}:
1175 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1176 case False{}:
1177 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1178 case False{}:
1179 match b4:
1180 case True{}:
1181 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1182 case False{}:
1183 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1184
1185def gc.elt0.s011(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}) == 0 : U32}:
1186 match b0:
1187 case True{}:
1188 match b1:
1189 case True{}:
1190 match b2:
1191 case True{}:
1192 match b3:
1193 case True{}:
1194 match b4:
1195 case True{}:
1196 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1197 case False{}:
1198 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1199 case False{}:
1200 match b4:
1201 case True{}:
1202 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1203 case False{}:
1204 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1205 case False{}:
1206 match b3:
1207 case True{}:
1208 match b4:
1209 case True{}:
1210 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1211 case False{}:
1212 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1213 case False{}:
1214 match b4:
1215 case True{}:
1216 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1217 case False{}:
1218 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1219 case False{}:
1220 match b2:
1221 case True{}:
1222 match b3:
1223 case True{}:
1224 match b4:
1225 case True{}:
1226 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1227 case False{}:
1228 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1229 case False{}:
1230 match b4:
1231 case True{}:
1232 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1233 case False{}:
1234 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1235 case False{}:
1236 match b3:
1237 case True{}:
1238 match b4:
1239 case True{}:
1240 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1241 case False{}:
1242 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1243 case False{}:
1244 match b4:
1245 case True{}:
1246 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1247 case False{}:
1248 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1249 case False{}:
1250 match b1:
1251 case True{}:
1252 match b2:
1253 case True{}:
1254 match b3:
1255 case True{}:
1256 match b4:
1257 case True{}:
1258 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1259 case False{}:
1260 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1261 case False{}:
1262 match b4:
1263 case True{}:
1264 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1265 case False{}:
1266 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1267 case False{}:
1268 match b3:
1269 case True{}:
1270 match b4:
1271 case True{}:
1272 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1273 case False{}:
1274 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1275 case False{}:
1276 match b4:
1277 case True{}:
1278 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1279 case False{}:
1280 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1281 case False{}:
1282 match b2:
1283 case True{}:
1284 match b3:
1285 case True{}:
1286 match b4:
1287 case True{}:
1288 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1289 case False{}:
1290 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1291 case False{}:
1292 match b4:
1293 case True{}:
1294 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1295 case False{}:
1296 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1297 case False{}:
1298 match b3:
1299 case True{}:
1300 match b4:
1301 case True{}:
1302 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1303 case False{}:
1304 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1305 case False{}:
1306 match b4:
1307 case True{}:
1308 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1309 case False{}:
1310 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1311
1312def gc.elt0.s101(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}) == 0 : U32}:
1313 match b0:
1314 case True{}:
1315 match b1:
1316 case True{}:
1317 match b2:
1318 case True{}:
1319 match b3:
1320 case True{}:
1321 match b4:
1322 case True{}:
1323 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1324 case False{}:
1325 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1326 case False{}:
1327 match b4:
1328 case True{}:
1329 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1330 case False{}:
1331 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1332 case False{}:
1333 match b3:
1334 case True{}:
1335 match b4:
1336 case True{}:
1337 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1338 case False{}:
1339 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1340 case False{}:
1341 match b4:
1342 case True{}:
1343 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1344 case False{}:
1345 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1346 case False{}:
1347 match b2:
1348 case True{}:
1349 match b3:
1350 case True{}:
1351 match b4:
1352 case True{}:
1353 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1354 case False{}:
1355 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1356 case False{}:
1357 match b4:
1358 case True{}:
1359 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1360 case False{}:
1361 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1362 case False{}:
1363 match b3:
1364 case True{}:
1365 match b4:
1366 case True{}:
1367 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1368 case False{}:
1369 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1370 case False{}:
1371 match b4:
1372 case True{}:
1373 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1374 case False{}:
1375 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1376 case False{}:
1377 match b1:
1378 case True{}:
1379 match b2:
1380 case True{}:
1381 match b3:
1382 case True{}:
1383 match b4:
1384 case True{}:
1385 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1386 case False{}:
1387 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1388 case False{}:
1389 match b4:
1390 case True{}:
1391 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1392 case False{}:
1393 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1394 case False{}:
1395 match b3:
1396 case True{}:
1397 match b4:
1398 case True{}:
1399 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1400 case False{}:
1401 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1402 case False{}:
1403 match b4:
1404 case True{}:
1405 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1406 case False{}:
1407 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1408 case False{}:
1409 match b2:
1410 case True{}:
1411 match b3:
1412 case True{}:
1413 match b4:
1414 case True{}:
1415 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1416 case False{}:
1417 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1418 case False{}:
1419 match b4:
1420 case True{}:
1421 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1422 case False{}:
1423 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1424 case False{}:
1425 match b3:
1426 case True{}:
1427 match b4:
1428 case True{}:
1429 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1430 case False{}:
1431 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1432 case False{}:
1433 match b4:
1434 case True{}:
1435 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1436 case False{}:
1437 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1438
1439def gc.elt0.s001(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}) == 0 : U32}:
1440 match b0:
1441 case True{}:
1442 match b1:
1443 case True{}:
1444 match b2:
1445 case True{}:
1446 match b3:
1447 case True{}:
1448 match b4:
1449 case True{}:
1450 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1451 case False{}:
1452 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1453 case False{}:
1454 match b4:
1455 case True{}:
1456 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1457 case False{}:
1458 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1459 case False{}:
1460 match b3:
1461 case True{}:
1462 match b4:
1463 case True{}:
1464 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1465 case False{}:
1466 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1467 case False{}:
1468 match b4:
1469 case True{}:
1470 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1471 case False{}:
1472 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1473 case False{}:
1474 match b2:
1475 case True{}:
1476 match b3:
1477 case True{}:
1478 match b4:
1479 case True{}:
1480 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1481 case False{}:
1482 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1483 case False{}:
1484 match b4:
1485 case True{}:
1486 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1487 case False{}:
1488 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1489 case False{}:
1490 match b3:
1491 case True{}:
1492 match b4:
1493 case True{}:
1494 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1495 case False{}:
1496 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1497 case False{}:
1498 match b4:
1499 case True{}:
1500 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1501 case False{}:
1502 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1503 case False{}:
1504 match b1:
1505 case True{}:
1506 match b2:
1507 case True{}:
1508 match b3:
1509 case True{}:
1510 match b4:
1511 case True{}:
1512 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1513 case False{}:
1514 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1515 case False{}:
1516 match b4:
1517 case True{}:
1518 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1519 case False{}:
1520 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1521 case False{}:
1522 match b3:
1523 case True{}:
1524 match b4:
1525 case True{}:
1526 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1527 case False{}:
1528 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1529 case False{}:
1530 match b4:
1531 case True{}:
1532 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1533 case False{}:
1534 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1535 case False{}:
1536 match b2:
1537 case True{}:
1538 match b3:
1539 case True{}:
1540 match b4:
1541 case True{}:
1542 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1543 case False{}:
1544 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1545 case False{}:
1546 match b4:
1547 case True{}:
1548 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1549 case False{}:
1550 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1551 case False{}:
1552 match b3:
1553 case True{}:
1554 match b4:
1555 case True{}:
1556 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1557 case False{}:
1558 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1559 case False{}:
1560 match b4:
1561 case True{}:
1562 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1563 case False{}:
1564 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1565
1566def gc.elt0.s110(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}) == 0 : U32}:
1567 match b0:
1568 case True{}:
1569 match b1:
1570 case True{}:
1571 match b2:
1572 case True{}:
1573 match b3:
1574 case True{}:
1575 match b4:
1576 case True{}:
1577 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1578 case False{}:
1579 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1580 case False{}:
1581 match b4:
1582 case True{}:
1583 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1584 case False{}:
1585 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1586 case False{}:
1587 match b3:
1588 case True{}:
1589 match b4:
1590 case True{}:
1591 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1592 case False{}:
1593 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1594 case False{}:
1595 match b4:
1596 case True{}:
1597 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1598 case False{}:
1599 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1600 case False{}:
1601 match b2:
1602 case True{}:
1603 match b3:
1604 case True{}:
1605 match b4:
1606 case True{}:
1607 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1608 case False{}:
1609 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1610 case False{}:
1611 match b4:
1612 case True{}:
1613 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1614 case False{}:
1615 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1616 case False{}:
1617 match b3:
1618 case True{}:
1619 match b4:
1620 case True{}:
1621 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1622 case False{}:
1623 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1624 case False{}:
1625 match b4:
1626 case True{}:
1627 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1628 case False{}:
1629 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1630 case False{}:
1631 match b1:
1632 case True{}:
1633 match b2:
1634 case True{}:
1635 match b3:
1636 case True{}:
1637 match b4:
1638 case True{}:
1639 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1640 case False{}:
1641 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1642 case False{}:
1643 match b4:
1644 case True{}:
1645 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1646 case False{}:
1647 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1648 case False{}:
1649 match b3:
1650 case True{}:
1651 match b4:
1652 case True{}:
1653 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1654 case False{}:
1655 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1656 case False{}:
1657 match b4:
1658 case True{}:
1659 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1660 case False{}:
1661 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1662 case False{}:
1663 match b2:
1664 case True{}:
1665 match b3:
1666 case True{}:
1667 match b4:
1668 case True{}:
1669 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1670 case False{}:
1671 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1672 case False{}:
1673 match b4:
1674 case True{}:
1675 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1676 case False{}:
1677 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1678 case False{}:
1679 match b3:
1680 case True{}:
1681 match b4:
1682 case True{}:
1683 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1684 case False{}:
1685 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1686 case False{}:
1687 match b4:
1688 case True{}:
1689 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1690 case False{}:
1691 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1692
1693def gc.elt0.s010(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}}) == 0 : U32}:
1694 match b0:
1695 case True{}:
1696 match b1:
1697 case True{}:
1698 match b2:
1699 case True{}:
1700 match b3:
1701 case True{}:
1702 match b4:
1703 case True{}:
1704 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1705 case False{}:
1706 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1707 case False{}:
1708 match b4:
1709 case True{}:
1710 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1711 case False{}:
1712 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1713 case False{}:
1714 match b3:
1715 case True{}:
1716 match b4:
1717 case True{}:
1718 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1719 case False{}:
1720 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1721 case False{}:
1722 match b4:
1723 case True{}:
1724 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1725 case False{}:
1726 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1727 case False{}:
1728 match b2:
1729 case True{}:
1730 match b3:
1731 case True{}:
1732 match b4:
1733 case True{}:
1734 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1735 case False{}:
1736 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1737 case False{}:
1738 match b4:
1739 case True{}:
1740 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1741 case False{}:
1742 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1743 case False{}:
1744 match b3:
1745 case True{}:
1746 match b4:
1747 case True{}:
1748 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1749 case False{}:
1750 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1751 case False{}:
1752 match b4:
1753 case True{}:
1754 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1755 case False{}:
1756 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1757 case False{}:
1758 match b1:
1759 case True{}:
1760 match b2:
1761 case True{}:
1762 match b3:
1763 case True{}:
1764 match b4:
1765 case True{}:
1766 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1767 case False{}:
1768 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1769 case False{}:
1770 match b4:
1771 case True{}:
1772 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1773 case False{}:
1774 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1775 case False{}:
1776 match b3:
1777 case True{}:
1778 match b4:
1779 case True{}:
1780 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1781 case False{}:
1782 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1783 case False{}:
1784 match b4:
1785 case True{}:
1786 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1787 case False{}:
1788 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1789 case False{}:
1790 match b2:
1791 case True{}:
1792 match b3:
1793 case True{}:
1794 match b4:
1795 case True{}:
1796 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1797 case False{}:
1798 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1799 case False{}:
1800 match b4:
1801 case True{}:
1802 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1803 case False{}:
1804 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1805 case False{}:
1806 match b3:
1807 case True{}:
1808 match b4:
1809 case True{}:
1810 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1811 case False{}:
1812 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1813 case False{}:
1814 match b4:
1815 case True{}:
1816 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1817 case False{}:
1818 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1819
1820def gc.elt0.s100(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}) == 0 : U32}:
1821 match b0:
1822 case True{}:
1823 match b1:
1824 case True{}:
1825 match b2:
1826 case True{}:
1827 match b3:
1828 case True{}:
1829 match b4:
1830 case True{}:
1831 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1832 case False{}:
1833 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1834 case False{}:
1835 match b4:
1836 case True{}:
1837 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1838 case False{}:
1839 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1840 case False{}:
1841 match b3:
1842 case True{}:
1843 match b4:
1844 case True{}:
1845 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1846 case False{}:
1847 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1848 case False{}:
1849 match b4:
1850 case True{}:
1851 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1852 case False{}:
1853 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1854 case False{}:
1855 match b2:
1856 case True{}:
1857 match b3:
1858 case True{}:
1859 match b4:
1860 case True{}:
1861 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1862 case False{}:
1863 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1864 case False{}:
1865 match b4:
1866 case True{}:
1867 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1868 case False{}:
1869 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1870 case False{}:
1871 match b3:
1872 case True{}:
1873 match b4:
1874 case True{}:
1875 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1876 case False{}:
1877 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1878 case False{}:
1879 match b4:
1880 case True{}:
1881 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1882 case False{}:
1883 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1884 case False{}:
1885 match b1:
1886 case True{}:
1887 match b2:
1888 case True{}:
1889 match b3:
1890 case True{}:
1891 match b4:
1892 case True{}:
1893 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1894 case False{}:
1895 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1896 case False{}:
1897 match b4:
1898 case True{}:
1899 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1900 case False{}:
1901 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1902 case False{}:
1903 match b3:
1904 case True{}:
1905 match b4:
1906 case True{}:
1907 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1908 case False{}:
1909 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1910 case False{}:
1911 match b4:
1912 case True{}:
1913 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1914 case False{}:
1915 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1916 case False{}:
1917 match b2:
1918 case True{}:
1919 match b3:
1920 case True{}:
1921 match b4:
1922 case True{}:
1923 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1924 case False{}:
1925 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1926 case False{}:
1927 match b4:
1928 case True{}:
1929 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1930 case False{}:
1931 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1932 case False{}:
1933 match b3:
1934 case True{}:
1935 match b4:
1936 case True{}:
1937 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1938 case False{}:
1939 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1940 case False{}:
1941 match b4:
1942 case True{}:
1943 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1944 case False{}:
1945 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1946
1947def gc.elt0.s000(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}}) == 0 : U32}:
1948 match b0:
1949 case True{}:
1950 match b1:
1951 case True{}:
1952 match b2:
1953 case True{}:
1954 match b3:
1955 case True{}:
1956 match b4:
1957 case True{}:
1958 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1959 case False{}:
1960 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1961 case False{}:
1962 match b4:
1963 case True{}:
1964 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1965 case False{}:
1966 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1967 case False{}:
1968 match b3:
1969 case True{}:
1970 match b4:
1971 case True{}:
1972 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1973 case False{}:
1974 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1975 case False{}:
1976 match b4:
1977 case True{}:
1978 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1979 case False{}:
1980 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1981 case False{}:
1982 match b2:
1983 case True{}:
1984 match b3:
1985 case True{}:
1986 match b4:
1987 case True{}:
1988 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1989 case False{}:
1990 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1991 case False{}:
1992 match b4:
1993 case True{}:
1994 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1995 case False{}:
1996 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1997 case False{}:
1998 match b3:
1999 case True{}:
2000 match b4:
2001 case True{}:
2002 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2003 case False{}:
2004 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2005 case False{}:
2006 match b4:
2007 case True{}:
2008 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2009 case False{}:
2010 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2011 case False{}:
2012 match b1:
2013 case True{}:
2014 match b2:
2015 case True{}:
2016 match b3:
2017 case True{}:
2018 match b4:
2019 case True{}:
2020 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2021 case False{}:
2022 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2023 case False{}:
2024 match b4:
2025 case True{}:
2026 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2027 case False{}:
2028 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2029 case False{}:
2030 match b3:
2031 case True{}:
2032 match b4:
2033 case True{}:
2034 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2035 case False{}:
2036 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2037 case False{}:
2038 match b4:
2039 case True{}:
2040 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2041 case False{}:
2042 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2043 case False{}:
2044 match b2:
2045 case True{}:
2046 match b3:
2047 case True{}:
2048 match b4:
2049 case True{}:
2050 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2051 case False{}:
2052 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2053 case False{}:
2054 match b4:
2055 case True{}:
2056 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2057 case False{}:
2058 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2059 case False{}:
2060 match b3:
2061 case True{}:
2062 match b4:
2063 case True{}:
2064 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2065 case False{}:
2066 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2067 case False{}:
2068 match b4:
2069 case True{}:
2070 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
2071 case False{}:
2072 {==}
2073
2074def gc.elt0.bits(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, +b5: Bool, +b6: Bool, +b7: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}) == 0 : U32}:
2075 match b5 b6 b7:
2076 case True{} True{} True{}:
2077 gc.elt0.s111(b0, b1, b2, b3, b4, h)
2078 case True{} True{} False{}:
2079 gc.elt0.s011(b0, b1, b2, b3, b4, h)
2080 case True{} False{} True{}:
2081 gc.elt0.s101(b0, b1, b2, b3, b4, h)
2082 case True{} False{} False{}:
2083 gc.elt0.s001(b0, b1, b2, b3, b4, h)
2084 case False{} True{} True{}:
2085 gc.elt0.s110(b0, b1, b2, b3, b4, h)
2086 case False{} True{} False{}:
2087 gc.elt0.s010(b0, b1, b2, b3, b4, h)
2088 case False{} False{} True{}:
2089 gc.elt0.s100(b0, b1, b2, b3, b4, h)
2090 case False{} False{} False{}:
2091 gc.elt0.s000(b0, b1, b2, b3, b4, h)
2092
2093def gc.elt0(+a: U32, h: {U32.is_eq(G.Gf8.elt(a), 0) == True{} : Bool}) -> {G.Gf8.elt(a) == 0 : U32}:
2094 match a:
2095 case U32{WCon{+b0, WCon{+b1, WCon{+b2, WCon{+b3, WCon{+b4, WCon{+b5, WCon{+b6, WCon{+b7, +r}}}}}}}}}:
2096 gc.elt0.bits(b0, b1, b2, b3, b4, b5, b6, b7, h)
2097
2098
2099
2100def gc.aes.ex0() -> {T.Gf8Tab.exp_table(G.Gf8.aes()) == T.gf8tab.fill.exp(510n, Array.new(U32, 9n, 0), G.Gf8.aes(), 1, 0) : Array<U32>}:
2101 {==}
2102
2103def gc.aes.el0() -> {T.Gf8Tab.log_table(G.Gf8.aes()) == T.gf8tab.fill.log(255n, Array.new(U32, 8n, 0), G.Gf8.aes(), 1, 0) : Array<U32>}:
2104 {==}
2105
2106def gc.aes.llist() -> List<&2, U32>:
2107 [0, 0, 25, 1, 50, 2, 26, 198, 75, 199, 27, 104, 51, 238, 223, 3, 100, 4, 224, 14, 52, 141, 129, 239, 76, 113, 8, 200, 248, 105, 28, 193, 125, 194, 29, 181, 249, 185, 39, 106, 77, 228, 166, 114, 154, 201, 9, 120, 101, 47, 138, 5, 33, 15, 225, 36, 18, 240, 130, 69, 53, 147, 218, 142, 150, 143, 219, 189, 54, 208, 206, 148, 19, 92, 210, 241, 64, 70, 131, 56, 102, 221, 253, 48, 191, 6, 139, 98, 179, 37, 226, 152, 34, 136, 145, 16, 126, 110, 72, 195, 163, 182, 30, 66, 58, 107, 40, 84, 250, 133, 61, 186, 43, 121, 10, 21, 155, 159, 94, 202, 78, 212, 172, 229, 243, 115, 167, 87, 175, 88, 168, 80, 244, 234, 214, 116, 79, 174, 233, 213, 231, 230, 173, 232, 44, 215, 117, 122, 235, 22, 11, 245, 89, 203, 95, 176, 156, 169, 81, 160, 127, 12, 246, 111, 23, 196, 73, 236, 216, 67, 31, 45, 164, 118, 123, 183, 204, 187, 62, 90, 251, 96, 177, 134, 59, 82, 161, 108, 170, 85, 41, 157, 151, 178, 135, 144, 97, 190, 220, 252, 188, 149, 207, 205, 55, 63, 91, 209, 83, 57, 132, 60, 65, 162, 109, 71, 20, 42, 158, 93, 86, 242, 211, 171, 68, 17, 146, 217, 35, 32, 46, 137, 180, 124, 184, 38, 119, 153, 227, 165, 103, 74, 237, 222, 197, 49, 254, 24, 13, 99, 140, 128, 192, 247, 112, 7]
2108
2109def gc.aes.lmodel() -> {GT.gt.fl(255n, List.replicate(U32, A.Arrays.slots(8n), 0), G.Gf8.aes(), 0n) == gc.aes.llist() : List<&2, U32>}:
2110 {==}
2111
2112def gc.aes.new() -> {GT.gt.tab(G.Gf8.aes(), gc.aes.llist()) == T.Gf8Tab.new(G.Gf8.aes()) : T.Gf8Tab}:
2113 GT.gt.new(G.Gf8.aes(), gc.aes.llist(), gc.aes.ex0(), gc.aes.el0(), gc.aes.lmodel())
2114
2115
2116def gc.aes.log.bits.s111(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}))) : U32}:
2117 match b0:
2118 case True{}:
2119 match b1:
2120 case True{}:
2121 match b2:
2122 case True{}:
2123 match b3:
2124 case True{}:
2125 match b4:
2126 case True{}:
2127 {==}
2128 case False{}:
2129 {==}
2130 case False{}:
2131 match b4:
2132 case True{}:
2133 {==}
2134 case False{}:
2135 {==}
2136 case False{}:
2137 match b3:
2138 case True{}:
2139 match b4:
2140 case True{}:
2141 {==}
2142 case False{}:
2143 {==}
2144 case False{}:
2145 match b4:
2146 case True{}:
2147 {==}
2148 case False{}:
2149 {==}
2150 case False{}:
2151 match b2:
2152 case True{}:
2153 match b3:
2154 case True{}:
2155 match b4:
2156 case True{}:
2157 {==}
2158 case False{}:
2159 {==}
2160 case False{}:
2161 match b4:
2162 case True{}:
2163 {==}
2164 case False{}:
2165 {==}
2166 case False{}:
2167 match b3:
2168 case True{}:
2169 match b4:
2170 case True{}:
2171 {==}
2172 case False{}:
2173 {==}
2174 case False{}:
2175 match b4:
2176 case True{}:
2177 {==}
2178 case False{}:
2179 {==}
2180 case False{}:
2181 match b1:
2182 case True{}:
2183 match b2:
2184 case True{}:
2185 match b3:
2186 case True{}:
2187 match b4:
2188 case True{}:
2189 {==}
2190 case False{}:
2191 {==}
2192 case False{}:
2193 match b4:
2194 case True{}:
2195 {==}
2196 case False{}:
2197 {==}
2198 case False{}:
2199 match b3:
2200 case True{}:
2201 match b4:
2202 case True{}:
2203 {==}
2204 case False{}:
2205 {==}
2206 case False{}:
2207 match b4:
2208 case True{}:
2209 {==}
2210 case False{}:
2211 {==}
2212 case False{}:
2213 match b2:
2214 case True{}:
2215 match b3:
2216 case True{}:
2217 match b4:
2218 case True{}:
2219 {==}
2220 case False{}:
2221 {==}
2222 case False{}:
2223 match b4:
2224 case True{}:
2225 {==}
2226 case False{}:
2227 {==}
2228 case False{}:
2229 match b3:
2230 case True{}:
2231 match b4:
2232 case True{}:
2233 {==}
2234 case False{}:
2235 {==}
2236 case False{}:
2237 match b4:
2238 case True{}:
2239 {==}
2240 case False{}:
2241 {==}
2242
2243def gc.aes.log.bits.s011(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}))) : U32}:
2244 match b0:
2245 case True{}:
2246 match b1:
2247 case True{}:
2248 match b2:
2249 case True{}:
2250 match b3:
2251 case True{}:
2252 match b4:
2253 case True{}:
2254 {==}
2255 case False{}:
2256 {==}
2257 case False{}:
2258 match b4:
2259 case True{}:
2260 {==}
2261 case False{}:
2262 {==}
2263 case False{}:
2264 match b3:
2265 case True{}:
2266 match b4:
2267 case True{}:
2268 {==}
2269 case False{}:
2270 {==}
2271 case False{}:
2272 match b4:
2273 case True{}:
2274 {==}
2275 case False{}:
2276 {==}
2277 case False{}:
2278 match b2:
2279 case True{}:
2280 match b3:
2281 case True{}:
2282 match b4:
2283 case True{}:
2284 {==}
2285 case False{}:
2286 {==}
2287 case False{}:
2288 match b4:
2289 case True{}:
2290 {==}
2291 case False{}:
2292 {==}
2293 case False{}:
2294 match b3:
2295 case True{}:
2296 match b4:
2297 case True{}:
2298 {==}
2299 case False{}:
2300 {==}
2301 case False{}:
2302 match b4:
2303 case True{}:
2304 {==}
2305 case False{}:
2306 {==}
2307 case False{}:
2308 match b1:
2309 case True{}:
2310 match b2:
2311 case True{}:
2312 match b3:
2313 case True{}:
2314 match b4:
2315 case True{}:
2316 {==}
2317 case False{}:
2318 {==}
2319 case False{}:
2320 match b4:
2321 case True{}:
2322 {==}
2323 case False{}:
2324 {==}
2325 case False{}:
2326 match b3:
2327 case True{}:
2328 match b4:
2329 case True{}:
2330 {==}
2331 case False{}:
2332 {==}
2333 case False{}:
2334 match b4:
2335 case True{}:
2336 {==}
2337 case False{}:
2338 {==}
2339 case False{}:
2340 match b2:
2341 case True{}:
2342 match b3:
2343 case True{}:
2344 match b4:
2345 case True{}:
2346 {==}
2347 case False{}:
2348 {==}
2349 case False{}:
2350 match b4:
2351 case True{}:
2352 {==}
2353 case False{}:
2354 {==}
2355 case False{}:
2356 match b3:
2357 case True{}:
2358 match b4:
2359 case True{}:
2360 {==}
2361 case False{}:
2362 {==}
2363 case False{}:
2364 match b4:
2365 case True{}:
2366 {==}
2367 case False{}:
2368 {==}
2369
2370def gc.aes.log.bits.s101(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}))) : U32}:
2371 match b0:
2372 case True{}:
2373 match b1:
2374 case True{}:
2375 match b2:
2376 case True{}:
2377 match b3:
2378 case True{}:
2379 match b4:
2380 case True{}:
2381 {==}
2382 case False{}:
2383 {==}
2384 case False{}:
2385 match b4:
2386 case True{}:
2387 {==}
2388 case False{}:
2389 {==}
2390 case False{}:
2391 match b3:
2392 case True{}:
2393 match b4:
2394 case True{}:
2395 {==}
2396 case False{}:
2397 {==}
2398 case False{}:
2399 match b4:
2400 case True{}:
2401 {==}
2402 case False{}:
2403 {==}
2404 case False{}:
2405 match b2:
2406 case True{}:
2407 match b3:
2408 case True{}:
2409 match b4:
2410 case True{}:
2411 {==}
2412 case False{}:
2413 {==}
2414 case False{}:
2415 match b4:
2416 case True{}:
2417 {==}
2418 case False{}:
2419 {==}
2420 case False{}:
2421 match b3:
2422 case True{}:
2423 match b4:
2424 case True{}:
2425 {==}
2426 case False{}:
2427 {==}
2428 case False{}:
2429 match b4:
2430 case True{}:
2431 {==}
2432 case False{}:
2433 {==}
2434 case False{}:
2435 match b1:
2436 case True{}:
2437 match b2:
2438 case True{}:
2439 match b3:
2440 case True{}:
2441 match b4:
2442 case True{}:
2443 {==}
2444 case False{}:
2445 {==}
2446 case False{}:
2447 match b4:
2448 case True{}:
2449 {==}
2450 case False{}:
2451 {==}
2452 case False{}:
2453 match b3:
2454 case True{}:
2455 match b4:
2456 case True{}:
2457 {==}
2458 case False{}:
2459 {==}
2460 case False{}:
2461 match b4:
2462 case True{}:
2463 {==}
2464 case False{}:
2465 {==}
2466 case False{}:
2467 match b2:
2468 case True{}:
2469 match b3:
2470 case True{}:
2471 match b4:
2472 case True{}:
2473 {==}
2474 case False{}:
2475 {==}
2476 case False{}:
2477 match b4:
2478 case True{}:
2479 {==}
2480 case False{}:
2481 {==}
2482 case False{}:
2483 match b3:
2484 case True{}:
2485 match b4:
2486 case True{}:
2487 {==}
2488 case False{}:
2489 {==}
2490 case False{}:
2491 match b4:
2492 case True{}:
2493 {==}
2494 case False{}:
2495 {==}
2496
2497def gc.aes.log.bits.s001(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}))) : U32}:
2498 match b0:
2499 case True{}:
2500 match b1:
2501 case True{}:
2502 match b2:
2503 case True{}:
2504 match b3:
2505 case True{}:
2506 match b4:
2507 case True{}:
2508 {==}
2509 case False{}:
2510 {==}
2511 case False{}:
2512 match b4:
2513 case True{}:
2514 {==}
2515 case False{}:
2516 {==}
2517 case False{}:
2518 match b3:
2519 case True{}:
2520 match b4:
2521 case True{}:
2522 {==}
2523 case False{}:
2524 {==}
2525 case False{}:
2526 match b4:
2527 case True{}:
2528 {==}
2529 case False{}:
2530 {==}
2531 case False{}:
2532 match b2:
2533 case True{}:
2534 match b3:
2535 case True{}:
2536 match b4:
2537 case True{}:
2538 {==}
2539 case False{}:
2540 {==}
2541 case False{}:
2542 match b4:
2543 case True{}:
2544 {==}
2545 case False{}:
2546 {==}
2547 case False{}:
2548 match b3:
2549 case True{}:
2550 match b4:
2551 case True{}:
2552 {==}
2553 case False{}:
2554 {==}
2555 case False{}:
2556 match b4:
2557 case True{}:
2558 {==}
2559 case False{}:
2560 {==}
2561 case False{}:
2562 match b1:
2563 case True{}:
2564 match b2:
2565 case True{}:
2566 match b3:
2567 case True{}:
2568 match b4:
2569 case True{}:
2570 {==}
2571 case False{}:
2572 {==}
2573 case False{}:
2574 match b4:
2575 case True{}:
2576 {==}
2577 case False{}:
2578 {==}
2579 case False{}:
2580 match b3:
2581 case True{}:
2582 match b4:
2583 case True{}:
2584 {==}
2585 case False{}:
2586 {==}
2587 case False{}:
2588 match b4:
2589 case True{}:
2590 {==}
2591 case False{}:
2592 {==}
2593 case False{}:
2594 match b2:
2595 case True{}:
2596 match b3:
2597 case True{}:
2598 match b4:
2599 case True{}:
2600 {==}
2601 case False{}:
2602 {==}
2603 case False{}:
2604 match b4:
2605 case True{}:
2606 {==}
2607 case False{}:
2608 {==}
2609 case False{}:
2610 match b3:
2611 case True{}:
2612 match b4:
2613 case True{}:
2614 {==}
2615 case False{}:
2616 {==}
2617 case False{}:
2618 match b4:
2619 case True{}:
2620 {==}
2621 case False{}:
2622 {==}
2623
2624def gc.aes.log.bits.s110(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}))) : U32}:
2625 match b0:
2626 case True{}:
2627 match b1:
2628 case True{}:
2629 match b2:
2630 case True{}:
2631 match b3:
2632 case True{}:
2633 match b4:
2634 case True{}:
2635 {==}
2636 case False{}:
2637 {==}
2638 case False{}:
2639 match b4:
2640 case True{}:
2641 {==}
2642 case False{}:
2643 {==}
2644 case False{}:
2645 match b3:
2646 case True{}:
2647 match b4:
2648 case True{}:
2649 {==}
2650 case False{}:
2651 {==}
2652 case False{}:
2653 match b4:
2654 case True{}:
2655 {==}
2656 case False{}:
2657 {==}
2658 case False{}:
2659 match b2:
2660 case True{}:
2661 match b3:
2662 case True{}:
2663 match b4:
2664 case True{}:
2665 {==}
2666 case False{}:
2667 {==}
2668 case False{}:
2669 match b4:
2670 case True{}:
2671 {==}
2672 case False{}:
2673 {==}
2674 case False{}:
2675 match b3:
2676 case True{}:
2677 match b4:
2678 case True{}:
2679 {==}
2680 case False{}:
2681 {==}
2682 case False{}:
2683 match b4:
2684 case True{}:
2685 {==}
2686 case False{}:
2687 {==}
2688 case False{}:
2689 match b1:
2690 case True{}:
2691 match b2:
2692 case True{}:
2693 match b3:
2694 case True{}:
2695 match b4:
2696 case True{}:
2697 {==}
2698 case False{}:
2699 {==}
2700 case False{}:
2701 match b4:
2702 case True{}:
2703 {==}
2704 case False{}:
2705 {==}
2706 case False{}:
2707 match b3:
2708 case True{}:
2709 match b4:
2710 case True{}:
2711 {==}
2712 case False{}:
2713 {==}
2714 case False{}:
2715 match b4:
2716 case True{}:
2717 {==}
2718 case False{}:
2719 {==}
2720 case False{}:
2721 match b2:
2722 case True{}:
2723 match b3:
2724 case True{}:
2725 match b4:
2726 case True{}:
2727 {==}
2728 case False{}:
2729 {==}
2730 case False{}:
2731 match b4:
2732 case True{}:
2733 {==}
2734 case False{}:
2735 {==}
2736 case False{}:
2737 match b3:
2738 case True{}:
2739 match b4:
2740 case True{}:
2741 {==}
2742 case False{}:
2743 {==}
2744 case False{}:
2745 match b4:
2746 case True{}:
2747 {==}
2748 case False{}:
2749 {==}
2750
2751def gc.aes.log.bits.s010(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}}))) : U32}:
2752 match b0:
2753 case True{}:
2754 match b1:
2755 case True{}:
2756 match b2:
2757 case True{}:
2758 match b3:
2759 case True{}:
2760 match b4:
2761 case True{}:
2762 {==}
2763 case False{}:
2764 {==}
2765 case False{}:
2766 match b4:
2767 case True{}:
2768 {==}
2769 case False{}:
2770 {==}
2771 case False{}:
2772 match b3:
2773 case True{}:
2774 match b4:
2775 case True{}:
2776 {==}
2777 case False{}:
2778 {==}
2779 case False{}:
2780 match b4:
2781 case True{}:
2782 {==}
2783 case False{}:
2784 {==}
2785 case False{}:
2786 match b2:
2787 case True{}:
2788 match b3:
2789 case True{}:
2790 match b4:
2791 case True{}:
2792 {==}
2793 case False{}:
2794 {==}
2795 case False{}:
2796 match b4:
2797 case True{}:
2798 {==}
2799 case False{}:
2800 {==}
2801 case False{}:
2802 match b3:
2803 case True{}:
2804 match b4:
2805 case True{}:
2806 {==}
2807 case False{}:
2808 {==}
2809 case False{}:
2810 match b4:
2811 case True{}:
2812 {==}
2813 case False{}:
2814 {==}
2815 case False{}:
2816 match b1:
2817 case True{}:
2818 match b2:
2819 case True{}:
2820 match b3:
2821 case True{}:
2822 match b4:
2823 case True{}:
2824 {==}
2825 case False{}:
2826 {==}
2827 case False{}:
2828 match b4:
2829 case True{}:
2830 {==}
2831 case False{}:
2832 {==}
2833 case False{}:
2834 match b3:
2835 case True{}:
2836 match b4:
2837 case True{}:
2838 {==}
2839 case False{}:
2840 {==}
2841 case False{}:
2842 match b4:
2843 case True{}:
2844 {==}
2845 case False{}:
2846 {==}
2847 case False{}:
2848 match b2:
2849 case True{}:
2850 match b3:
2851 case True{}:
2852 match b4:
2853 case True{}:
2854 {==}
2855 case False{}:
2856 {==}
2857 case False{}:
2858 match b4:
2859 case True{}:
2860 {==}
2861 case False{}:
2862 {==}
2863 case False{}:
2864 match b3:
2865 case True{}:
2866 match b4:
2867 case True{}:
2868 {==}
2869 case False{}:
2870 {==}
2871 case False{}:
2872 match b4:
2873 case True{}:
2874 {==}
2875 case False{}:
2876 {==}
2877
2878def gc.aes.log.bits.s100(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}))) : U32}:
2879 match b0:
2880 case True{}:
2881 match b1:
2882 case True{}:
2883 match b2:
2884 case True{}:
2885 match b3:
2886 case True{}:
2887 match b4:
2888 case True{}:
2889 {==}
2890 case False{}:
2891 {==}
2892 case False{}:
2893 match b4:
2894 case True{}:
2895 {==}
2896 case False{}:
2897 {==}
2898 case False{}:
2899 match b3:
2900 case True{}:
2901 match b4:
2902 case True{}:
2903 {==}
2904 case False{}:
2905 {==}
2906 case False{}:
2907 match b4:
2908 case True{}:
2909 {==}
2910 case False{}:
2911 {==}
2912 case False{}:
2913 match b2:
2914 case True{}:
2915 match b3:
2916 case True{}:
2917 match b4:
2918 case True{}:
2919 {==}
2920 case False{}:
2921 {==}
2922 case False{}:
2923 match b4:
2924 case True{}:
2925 {==}
2926 case False{}:
2927 {==}
2928 case False{}:
2929 match b3:
2930 case True{}:
2931 match b4:
2932 case True{}:
2933 {==}
2934 case False{}:
2935 {==}
2936 case False{}:
2937 match b4:
2938 case True{}:
2939 {==}
2940 case False{}:
2941 {==}
2942 case False{}:
2943 match b1:
2944 case True{}:
2945 match b2:
2946 case True{}:
2947 match b3:
2948 case True{}:
2949 match b4:
2950 case True{}:
2951 {==}
2952 case False{}:
2953 {==}
2954 case False{}:
2955 match b4:
2956 case True{}:
2957 {==}
2958 case False{}:
2959 {==}
2960 case False{}:
2961 match b3:
2962 case True{}:
2963 match b4:
2964 case True{}:
2965 {==}
2966 case False{}:
2967 {==}
2968 case False{}:
2969 match b4:
2970 case True{}:
2971 {==}
2972 case False{}:
2973 {==}
2974 case False{}:
2975 match b2:
2976 case True{}:
2977 match b3:
2978 case True{}:
2979 match b4:
2980 case True{}:
2981 {==}
2982 case False{}:
2983 {==}
2984 case False{}:
2985 match b4:
2986 case True{}:
2987 {==}
2988 case False{}:
2989 {==}
2990 case False{}:
2991 match b3:
2992 case True{}:
2993 match b4:
2994 case True{}:
2995 {==}
2996 case False{}:
2997 {==}
2998 case False{}:
2999 match b4:
3000 case True{}:
3001 {==}
3002 case False{}:
3003 {==}
3004
3005def gc.aes.log.bits.s000(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}}))) : U32}:
3006 match b0:
3007 case True{}:
3008 match b1:
3009 case True{}:
3010 match b2:
3011 case True{}:
3012 match b3:
3013 case True{}:
3014 match b4:
3015 case True{}:
3016 {==}
3017 case False{}:
3018 {==}
3019 case False{}:
3020 match b4:
3021 case True{}:
3022 {==}
3023 case False{}:
3024 {==}
3025 case False{}:
3026 match b3:
3027 case True{}:
3028 match b4:
3029 case True{}:
3030 {==}
3031 case False{}:
3032 {==}
3033 case False{}:
3034 match b4:
3035 case True{}:
3036 {==}
3037 case False{}:
3038 {==}
3039 case False{}:
3040 match b2:
3041 case True{}:
3042 match b3:
3043 case True{}:
3044 match b4:
3045 case True{}:
3046 {==}
3047 case False{}:
3048 {==}
3049 case False{}:
3050 match b4:
3051 case True{}:
3052 {==}
3053 case False{}:
3054 {==}
3055 case False{}:
3056 match b3:
3057 case True{}:
3058 match b4:
3059 case True{}:
3060 {==}
3061 case False{}:
3062 {==}
3063 case False{}:
3064 match b4:
3065 case True{}:
3066 {==}
3067 case False{}:
3068 {==}
3069 case False{}:
3070 match b1:
3071 case True{}:
3072 match b2:
3073 case True{}:
3074 match b3:
3075 case True{}:
3076 match b4:
3077 case True{}:
3078 {==}
3079 case False{}:
3080 {==}
3081 case False{}:
3082 match b4:
3083 case True{}:
3084 {==}
3085 case False{}:
3086 {==}
3087 case False{}:
3088 match b3:
3089 case True{}:
3090 match b4:
3091 case True{}:
3092 {==}
3093 case False{}:
3094 {==}
3095 case False{}:
3096 match b4:
3097 case True{}:
3098 {==}
3099 case False{}:
3100 {==}
3101 case False{}:
3102 match b2:
3103 case True{}:
3104 match b3:
3105 case True{}:
3106 match b4:
3107 case True{}:
3108 {==}
3109 case False{}:
3110 {==}
3111 case False{}:
3112 match b4:
3113 case True{}:
3114 {==}
3115 case False{}:
3116 {==}
3117 case False{}:
3118 match b3:
3119 case True{}:
3120 match b4:
3121 case True{}:
3122 {==}
3123 case False{}:
3124 {==}
3125 case False{}:
3126 match b4:
3127 case True{}:
3128 {==}
3129 case False{}:
3130 {==}
3131
3132def gc.aes.log.bits(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, +b5: Bool, +b6: Bool, +b7: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}))) : U32}:
3133 match b5 b6 b7:
3134 case True{} True{} True{}:
3135 gc.aes.log.bits.s111(b0, b1, b2, b3, b4)
3136 case True{} True{} False{}:
3137 gc.aes.log.bits.s011(b0, b1, b2, b3, b4)
3138 case True{} False{} True{}:
3139 gc.aes.log.bits.s101(b0, b1, b2, b3, b4)
3140 case True{} False{} False{}:
3141 gc.aes.log.bits.s001(b0, b1, b2, b3, b4)
3142 case False{} True{} True{}:
3143 gc.aes.log.bits.s110(b0, b1, b2, b3, b4)
3144 case False{} True{} False{}:
3145 gc.aes.log.bits.s010(b0, b1, b2, b3, b4)
3146 case False{} False{} True{}:
3147 gc.aes.log.bits.s100(b0, b1, b2, b3, b4)
3148 case False{} False{} False{}:
3149 gc.aes.log.bits.s000(b0, b1, b2, b3, b4)
3150
3151def gc.aes.log(+a: U32) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8.elt(a)), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), a)) : U32}:
3152 match a:
3153 case U32{WCon{+b0, WCon{+b1, WCon{+b2, WCon{+b3, WCon{+b4, WCon{+b5, WCon{+b6, WCon{+b7, +r}}}}}}}}}:
3154 gc.aes.log.bits(b0, b1, b2, b3, b4, b5, b6, b7)
3155
3156
3157
3158def gc.rs.ex0() -> {T.Gf8Tab.exp_table(G.Gf8.rs()) == T.gf8tab.fill.exp(510n, Array.new(U32, 9n, 0), G.Gf8.rs(), 1, 0) : Array<U32>}:
3159 {==}
3160
3161def gc.rs.el0() -> {T.Gf8Tab.log_table(G.Gf8.rs()) == T.gf8tab.fill.log(255n, Array.new(U32, 8n, 0), G.Gf8.rs(), 1, 0) : Array<U32>}:
3162 {==}
3163
3164def gc.rs.llist() -> List<&2, U32>:
3165 [0, 0, 1, 25, 2, 50, 26, 198, 3, 223, 51, 238, 27, 104, 199, 75, 4, 100, 224, 14, 52, 141, 239, 129, 28, 193, 105, 248, 200, 8, 76, 113, 5, 138, 101, 47, 225, 36, 15, 33, 53, 147, 142, 218, 240, 18, 130, 69, 29, 181, 194, 125, 106, 39, 249, 185, 201, 154, 9, 120, 77, 228, 114, 166, 6, 191, 139, 98, 102, 221, 48, 253, 226, 152, 37, 179, 16, 145, 34, 136, 54, 208, 148, 206, 143, 150, 219, 189, 241, 210, 19, 92, 131, 56, 70, 64, 30, 66, 182, 163, 195, 72, 126, 110, 107, 58, 40, 84, 250, 133, 186, 61, 202, 94, 155, 159, 10, 21, 121, 43, 78, 212, 229, 172, 115, 243, 167, 87, 7, 112, 192, 247, 140, 128, 99, 13, 103, 74, 222, 237, 49, 197, 254, 24, 227, 165, 153, 119, 38, 184, 180, 124, 17, 68, 146, 217, 35, 32, 137, 46, 55, 63, 209, 91, 149, 188, 207, 205, 144, 135, 151, 178, 220, 252, 190, 97, 242, 86, 211, 171, 20, 42, 93, 158, 132, 60, 57, 83, 71, 109, 65, 162, 31, 45, 67, 216, 183, 123, 164, 118, 196, 23, 73, 236, 127, 12, 111, 246, 108, 161, 59, 82, 41, 157, 85, 170, 251, 96, 134, 177, 187, 204, 62, 90, 203, 89, 95, 176, 156, 169, 160, 81, 11, 245, 22, 235, 122, 117, 44, 215, 79, 174, 213, 233, 230, 231, 173, 232, 116, 214, 244, 234, 168, 80, 88, 175]
3166
3167def gc.rs.lmodel() -> {GT.gt.fl(255n, List.replicate(U32, A.Arrays.slots(8n), 0), G.Gf8.rs(), 0n) == gc.rs.llist() : List<&2, U32>}:
3168 {==}
3169
3170def gc.rs.new() -> {GT.gt.tab(G.Gf8.rs(), gc.rs.llist()) == T.Gf8Tab.new(G.Gf8.rs()) : T.Gf8Tab}:
3171 GT.gt.new(G.Gf8.rs(), gc.rs.llist(), gc.rs.ex0(), gc.rs.el0(), gc.rs.lmodel())
3172
3173
3174def gc.rs.log.bits.s111(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}))) : U32}:
3175 match b0:
3176 case True{}:
3177 match b1:
3178 case True{}:
3179 match b2:
3180 case True{}:
3181 match b3:
3182 case True{}:
3183 match b4:
3184 case True{}:
3185 {==}
3186 case False{}:
3187 {==}
3188 case False{}:
3189 match b4:
3190 case True{}:
3191 {==}
3192 case False{}:
3193 {==}
3194 case False{}:
3195 match b3:
3196 case True{}:
3197 match b4:
3198 case True{}:
3199 {==}
3200 case False{}:
3201 {==}
3202 case False{}:
3203 match b4:
3204 case True{}:
3205 {==}
3206 case False{}:
3207 {==}
3208 case False{}:
3209 match b2:
3210 case True{}:
3211 match b3:
3212 case True{}:
3213 match b4:
3214 case True{}:
3215 {==}
3216 case False{}:
3217 {==}
3218 case False{}:
3219 match b4:
3220 case True{}:
3221 {==}
3222 case False{}:
3223 {==}
3224 case False{}:
3225 match b3:
3226 case True{}:
3227 match b4:
3228 case True{}:
3229 {==}
3230 case False{}:
3231 {==}
3232 case False{}:
3233 match b4:
3234 case True{}:
3235 {==}
3236 case False{}:
3237 {==}
3238 case False{}:
3239 match b1:
3240 case True{}:
3241 match b2:
3242 case True{}:
3243 match b3:
3244 case True{}:
3245 match b4:
3246 case True{}:
3247 {==}
3248 case False{}:
3249 {==}
3250 case False{}:
3251 match b4:
3252 case True{}:
3253 {==}
3254 case False{}:
3255 {==}
3256 case False{}:
3257 match b3:
3258 case True{}:
3259 match b4:
3260 case True{}:
3261 {==}
3262 case False{}:
3263 {==}
3264 case False{}:
3265 match b4:
3266 case True{}:
3267 {==}
3268 case False{}:
3269 {==}
3270 case False{}:
3271 match b2:
3272 case True{}:
3273 match b3:
3274 case True{}:
3275 match b4:
3276 case True{}:
3277 {==}
3278 case False{}:
3279 {==}
3280 case False{}:
3281 match b4:
3282 case True{}:
3283 {==}
3284 case False{}:
3285 {==}
3286 case False{}:
3287 match b3:
3288 case True{}:
3289 match b4:
3290 case True{}:
3291 {==}
3292 case False{}:
3293 {==}
3294 case False{}:
3295 match b4:
3296 case True{}:
3297 {==}
3298 case False{}:
3299 {==}
3300
3301def gc.rs.log.bits.s011(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}))) : U32}:
3302 match b0:
3303 case True{}:
3304 match b1:
3305 case True{}:
3306 match b2:
3307 case True{}:
3308 match b3:
3309 case True{}:
3310 match b4:
3311 case True{}:
3312 {==}
3313 case False{}:
3314 {==}
3315 case False{}:
3316 match b4:
3317 case True{}:
3318 {==}
3319 case False{}:
3320 {==}
3321 case False{}:
3322 match b3:
3323 case True{}:
3324 match b4:
3325 case True{}:
3326 {==}
3327 case False{}:
3328 {==}
3329 case False{}:
3330 match b4:
3331 case True{}:
3332 {==}
3333 case False{}:
3334 {==}
3335 case False{}:
3336 match b2:
3337 case True{}:
3338 match b3:
3339 case True{}:
3340 match b4:
3341 case True{}:
3342 {==}
3343 case False{}:
3344 {==}
3345 case False{}:
3346 match b4:
3347 case True{}:
3348 {==}
3349 case False{}:
3350 {==}
3351 case False{}:
3352 match b3:
3353 case True{}:
3354 match b4:
3355 case True{}:
3356 {==}
3357 case False{}:
3358 {==}
3359 case False{}:
3360 match b4:
3361 case True{}:
3362 {==}
3363 case False{}:
3364 {==}
3365 case False{}:
3366 match b1:
3367 case True{}:
3368 match b2:
3369 case True{}:
3370 match b3:
3371 case True{}:
3372 match b4:
3373 case True{}:
3374 {==}
3375 case False{}:
3376 {==}
3377 case False{}:
3378 match b4:
3379 case True{}:
3380 {==}
3381 case False{}:
3382 {==}
3383 case False{}:
3384 match b3:
3385 case True{}:
3386 match b4:
3387 case True{}:
3388 {==}
3389 case False{}:
3390 {==}
3391 case False{}:
3392 match b4:
3393 case True{}:
3394 {==}
3395 case False{}:
3396 {==}
3397 case False{}:
3398 match b2:
3399 case True{}:
3400 match b3:
3401 case True{}:
3402 match b4:
3403 case True{}:
3404 {==}
3405 case False{}:
3406 {==}
3407 case False{}:
3408 match b4:
3409 case True{}:
3410 {==}
3411 case False{}:
3412 {==}
3413 case False{}:
3414 match b3:
3415 case True{}:
3416 match b4:
3417 case True{}:
3418 {==}
3419 case False{}:
3420 {==}
3421 case False{}:
3422 match b4:
3423 case True{}:
3424 {==}
3425 case False{}:
3426 {==}
3427
3428def gc.rs.log.bits.s101(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}))) : U32}:
3429 match b0:
3430 case True{}:
3431 match b1:
3432 case True{}:
3433 match b2:
3434 case True{}:
3435 match b3:
3436 case True{}:
3437 match b4:
3438 case True{}:
3439 {==}
3440 case False{}:
3441 {==}
3442 case False{}:
3443 match b4:
3444 case True{}:
3445 {==}
3446 case False{}:
3447 {==}
3448 case False{}:
3449 match b3:
3450 case True{}:
3451 match b4:
3452 case True{}:
3453 {==}
3454 case False{}:
3455 {==}
3456 case False{}:
3457 match b4:
3458 case True{}:
3459 {==}
3460 case False{}:
3461 {==}
3462 case False{}:
3463 match b2:
3464 case True{}:
3465 match b3:
3466 case True{}:
3467 match b4:
3468 case True{}:
3469 {==}
3470 case False{}:
3471 {==}
3472 case False{}:
3473 match b4:
3474 case True{}:
3475 {==}
3476 case False{}:
3477 {==}
3478 case False{}:
3479 match b3:
3480 case True{}:
3481 match b4:
3482 case True{}:
3483 {==}
3484 case False{}:
3485 {==}
3486 case False{}:
3487 match b4:
3488 case True{}:
3489 {==}
3490 case False{}:
3491 {==}
3492 case False{}:
3493 match b1:
3494 case True{}:
3495 match b2:
3496 case True{}:
3497 match b3:
3498 case True{}:
3499 match b4:
3500 case True{}:
3501 {==}
3502 case False{}:
3503 {==}
3504 case False{}:
3505 match b4:
3506 case True{}:
3507 {==}
3508 case False{}:
3509 {==}
3510 case False{}:
3511 match b3:
3512 case True{}:
3513 match b4:
3514 case True{}:
3515 {==}
3516 case False{}:
3517 {==}
3518 case False{}:
3519 match b4:
3520 case True{}:
3521 {==}
3522 case False{}:
3523 {==}
3524 case False{}:
3525 match b2:
3526 case True{}:
3527 match b3:
3528 case True{}:
3529 match b4:
3530 case True{}:
3531 {==}
3532 case False{}:
3533 {==}
3534 case False{}:
3535 match b4:
3536 case True{}:
3537 {==}
3538 case False{}:
3539 {==}
3540 case False{}:
3541 match b3:
3542 case True{}:
3543 match b4:
3544 case True{}:
3545 {==}
3546 case False{}:
3547 {==}
3548 case False{}:
3549 match b4:
3550 case True{}:
3551 {==}
3552 case False{}:
3553 {==}
3554
3555def gc.rs.log.bits.s001(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}))) : U32}:
3556 match b0:
3557 case True{}:
3558 match b1:
3559 case True{}:
3560 match b2:
3561 case True{}:
3562 match b3:
3563 case True{}:
3564 match b4:
3565 case True{}:
3566 {==}
3567 case False{}:
3568 {==}
3569 case False{}:
3570 match b4:
3571 case True{}:
3572 {==}
3573 case False{}:
3574 {==}
3575 case False{}:
3576 match b3:
3577 case True{}:
3578 match b4:
3579 case True{}:
3580 {==}
3581 case False{}:
3582 {==}
3583 case False{}:
3584 match b4:
3585 case True{}:
3586 {==}
3587 case False{}:
3588 {==}
3589 case False{}:
3590 match b2:
3591 case True{}:
3592 match b3:
3593 case True{}:
3594 match b4:
3595 case True{}:
3596 {==}
3597 case False{}:
3598 {==}
3599 case False{}:
3600 match b4:
3601 case True{}:
3602 {==}
3603 case False{}:
3604 {==}
3605 case False{}:
3606 match b3:
3607 case True{}:
3608 match b4:
3609 case True{}:
3610 {==}
3611 case False{}:
3612 {==}
3613 case False{}:
3614 match b4:
3615 case True{}:
3616 {==}
3617 case False{}:
3618 {==}
3619 case False{}:
3620 match b1:
3621 case True{}:
3622 match b2:
3623 case True{}:
3624 match b3:
3625 case True{}:
3626 match b4:
3627 case True{}:
3628 {==}
3629 case False{}:
3630 {==}
3631 case False{}:
3632 match b4:
3633 case True{}:
3634 {==}
3635 case False{}:
3636 {==}
3637 case False{}:
3638 match b3:
3639 case True{}:
3640 match b4:
3641 case True{}:
3642 {==}
3643 case False{}:
3644 {==}
3645 case False{}:
3646 match b4:
3647 case True{}:
3648 {==}
3649 case False{}:
3650 {==}
3651 case False{}:
3652 match b2:
3653 case True{}:
3654 match b3:
3655 case True{}:
3656 match b4:
3657 case True{}:
3658 {==}
3659 case False{}:
3660 {==}
3661 case False{}:
3662 match b4:
3663 case True{}:
3664 {==}
3665 case False{}:
3666 {==}
3667 case False{}:
3668 match b3:
3669 case True{}:
3670 match b4:
3671 case True{}:
3672 {==}
3673 case False{}:
3674 {==}
3675 case False{}:
3676 match b4:
3677 case True{}:
3678 {==}
3679 case False{}:
3680 {==}
3681
3682def gc.rs.log.bits.s110(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}))) : U32}:
3683 match b0:
3684 case True{}:
3685 match b1:
3686 case True{}:
3687 match b2:
3688 case True{}:
3689 match b3:
3690 case True{}:
3691 match b4:
3692 case True{}:
3693 {==}
3694 case False{}:
3695 {==}
3696 case False{}:
3697 match b4:
3698 case True{}:
3699 {==}
3700 case False{}:
3701 {==}
3702 case False{}:
3703 match b3:
3704 case True{}:
3705 match b4:
3706 case True{}:
3707 {==}
3708 case False{}:
3709 {==}
3710 case False{}:
3711 match b4:
3712 case True{}:
3713 {==}
3714 case False{}:
3715 {==}
3716 case False{}:
3717 match b2:
3718 case True{}:
3719 match b3:
3720 case True{}:
3721 match b4:
3722 case True{}:
3723 {==}
3724 case False{}:
3725 {==}
3726 case False{}:
3727 match b4:
3728 case True{}:
3729 {==}
3730 case False{}:
3731 {==}
3732 case False{}:
3733 match b3:
3734 case True{}:
3735 match b4:
3736 case True{}:
3737 {==}
3738 case False{}:
3739 {==}
3740 case False{}:
3741 match b4:
3742 case True{}:
3743 {==}
3744 case False{}:
3745 {==}
3746 case False{}:
3747 match b1:
3748 case True{}:
3749 match b2:
3750 case True{}:
3751 match b3:
3752 case True{}:
3753 match b4:
3754 case True{}:
3755 {==}
3756 case False{}:
3757 {==}
3758 case False{}:
3759 match b4:
3760 case True{}:
3761 {==}
3762 case False{}:
3763 {==}
3764 case False{}:
3765 match b3:
3766 case True{}:
3767 match b4:
3768 case True{}:
3769 {==}
3770 case False{}:
3771 {==}
3772 case False{}:
3773 match b4:
3774 case True{}:
3775 {==}
3776 case False{}:
3777 {==}
3778 case False{}:
3779 match b2:
3780 case True{}:
3781 match b3:
3782 case True{}:
3783 match b4:
3784 case True{}:
3785 {==}
3786 case False{}:
3787 {==}
3788 case False{}:
3789 match b4:
3790 case True{}:
3791 {==}
3792 case False{}:
3793 {==}
3794 case False{}:
3795 match b3:
3796 case True{}:
3797 match b4:
3798 case True{}:
3799 {==}
3800 case False{}:
3801 {==}
3802 case False{}:
3803 match b4:
3804 case True{}:
3805 {==}
3806 case False{}:
3807 {==}
3808
3809def gc.rs.log.bits.s010(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}}))) : U32}:
3810 match b0:
3811 case True{}:
3812 match b1:
3813 case True{}:
3814 match b2:
3815 case True{}:
3816 match b3:
3817 case True{}:
3818 match b4:
3819 case True{}:
3820 {==}
3821 case False{}:
3822 {==}
3823 case False{}:
3824 match b4:
3825 case True{}:
3826 {==}
3827 case False{}:
3828 {==}
3829 case False{}:
3830 match b3:
3831 case True{}:
3832 match b4:
3833 case True{}:
3834 {==}
3835 case False{}:
3836 {==}
3837 case False{}:
3838 match b4:
3839 case True{}:
3840 {==}
3841 case False{}:
3842 {==}
3843 case False{}:
3844 match b2:
3845 case True{}:
3846 match b3:
3847 case True{}:
3848 match b4:
3849 case True{}:
3850 {==}
3851 case False{}:
3852 {==}
3853 case False{}:
3854 match b4:
3855 case True{}:
3856 {==}
3857 case False{}:
3858 {==}
3859 case False{}:
3860 match b3:
3861 case True{}:
3862 match b4:
3863 case True{}:
3864 {==}
3865 case False{}:
3866 {==}
3867 case False{}:
3868 match b4:
3869 case True{}:
3870 {==}
3871 case False{}:
3872 {==}
3873 case False{}:
3874 match b1:
3875 case True{}:
3876 match b2:
3877 case True{}:
3878 match b3:
3879 case True{}:
3880 match b4:
3881 case True{}:
3882 {==}
3883 case False{}:
3884 {==}
3885 case False{}:
3886 match b4:
3887 case True{}:
3888 {==}
3889 case False{}:
3890 {==}
3891 case False{}:
3892 match b3:
3893 case True{}:
3894 match b4:
3895 case True{}:
3896 {==}
3897 case False{}:
3898 {==}
3899 case False{}:
3900 match b4:
3901 case True{}:
3902 {==}
3903 case False{}:
3904 {==}
3905 case False{}:
3906 match b2:
3907 case True{}:
3908 match b3:
3909 case True{}:
3910 match b4:
3911 case True{}:
3912 {==}
3913 case False{}:
3914 {==}
3915 case False{}:
3916 match b4:
3917 case True{}:
3918 {==}
3919 case False{}:
3920 {==}
3921 case False{}:
3922 match b3:
3923 case True{}:
3924 match b4:
3925 case True{}:
3926 {==}
3927 case False{}:
3928 {==}
3929 case False{}:
3930 match b4:
3931 case True{}:
3932 {==}
3933 case False{}:
3934 {==}
3935
3936def gc.rs.log.bits.s100(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}))) : U32}:
3937 match b0:
3938 case True{}:
3939 match b1:
3940 case True{}:
3941 match b2:
3942 case True{}:
3943 match b3:
3944 case True{}:
3945 match b4:
3946 case True{}:
3947 {==}
3948 case False{}:
3949 {==}
3950 case False{}:
3951 match b4:
3952 case True{}:
3953 {==}
3954 case False{}:
3955 {==}
3956 case False{}:
3957 match b3:
3958 case True{}:
3959 match b4:
3960 case True{}:
3961 {==}
3962 case False{}:
3963 {==}
3964 case False{}:
3965 match b4:
3966 case True{}:
3967 {==}
3968 case False{}:
3969 {==}
3970 case False{}:
3971 match b2:
3972 case True{}:
3973 match b3:
3974 case True{}:
3975 match b4:
3976 case True{}:
3977 {==}
3978 case False{}:
3979 {==}
3980 case False{}:
3981 match b4:
3982 case True{}:
3983 {==}
3984 case False{}:
3985 {==}
3986 case False{}:
3987 match b3:
3988 case True{}:
3989 match b4:
3990 case True{}:
3991 {==}
3992 case False{}:
3993 {==}
3994 case False{}:
3995 match b4:
3996 case True{}:
3997 {==}
3998 case False{}:
3999 {==}
4000 case False{}:
4001 match b1:
4002 case True{}:
4003 match b2:
4004 case True{}:
4005 match b3:
4006 case True{}:
4007 match b4:
4008 case True{}:
4009 {==}
4010 case False{}:
4011 {==}
4012 case False{}:
4013 match b4:
4014 case True{}:
4015 {==}
4016 case False{}:
4017 {==}
4018 case False{}:
4019 match b3:
4020 case True{}:
4021 match b4:
4022 case True{}:
4023 {==}
4024 case False{}:
4025 {==}
4026 case False{}:
4027 match b4:
4028 case True{}:
4029 {==}
4030 case False{}:
4031 {==}
4032 case False{}:
4033 match b2:
4034 case True{}:
4035 match b3:
4036 case True{}:
4037 match b4:
4038 case True{}:
4039 {==}
4040 case False{}:
4041 {==}
4042 case False{}:
4043 match b4:
4044 case True{}:
4045 {==}
4046 case False{}:
4047 {==}
4048 case False{}:
4049 match b3:
4050 case True{}:
4051 match b4:
4052 case True{}:
4053 {==}
4054 case False{}:
4055 {==}
4056 case False{}:
4057 match b4:
4058 case True{}:
4059 {==}
4060 case False{}:
4061 {==}
4062
4063def gc.rs.log.bits.s000(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}}))) : U32}:
4064 match b0:
4065 case True{}:
4066 match b1:
4067 case True{}:
4068 match b2:
4069 case True{}:
4070 match b3:
4071 case True{}:
4072 match b4:
4073 case True{}:
4074 {==}
4075 case False{}:
4076 {==}
4077 case False{}:
4078 match b4:
4079 case True{}:
4080 {==}
4081 case False{}:
4082 {==}
4083 case False{}:
4084 match b3:
4085 case True{}:
4086 match b4:
4087 case True{}:
4088 {==}
4089 case False{}:
4090 {==}
4091 case False{}:
4092 match b4:
4093 case True{}:
4094 {==}
4095 case False{}:
4096 {==}
4097 case False{}:
4098 match b2:
4099 case True{}:
4100 match b3:
4101 case True{}:
4102 match b4:
4103 case True{}:
4104 {==}
4105 case False{}:
4106 {==}
4107 case False{}:
4108 match b4:
4109 case True{}:
4110 {==}
4111 case False{}:
4112 {==}
4113 case False{}:
4114 match b3:
4115 case True{}:
4116 match b4:
4117 case True{}:
4118 {==}
4119 case False{}:
4120 {==}
4121 case False{}:
4122 match b4:
4123 case True{}:
4124 {==}
4125 case False{}:
4126 {==}
4127 case False{}:
4128 match b1:
4129 case True{}:
4130 match b2:
4131 case True{}:
4132 match b3:
4133 case True{}:
4134 match b4:
4135 case True{}:
4136 {==}
4137 case False{}:
4138 {==}
4139 case False{}:
4140 match b4:
4141 case True{}:
4142 {==}
4143 case False{}:
4144 {==}
4145 case False{}:
4146 match b3:
4147 case True{}:
4148 match b4:
4149 case True{}:
4150 {==}
4151 case False{}:
4152 {==}
4153 case False{}:
4154 match b4:
4155 case True{}:
4156 {==}
4157 case False{}:
4158 {==}
4159 case False{}:
4160 match b2:
4161 case True{}:
4162 match b3:
4163 case True{}:
4164 match b4:
4165 case True{}:
4166 {==}
4167 case False{}:
4168 {==}
4169 case False{}:
4170 match b4:
4171 case True{}:
4172 {==}
4173 case False{}:
4174 {==}
4175 case False{}:
4176 match b3:
4177 case True{}:
4178 match b4:
4179 case True{}:
4180 {==}
4181 case False{}:
4182 {==}
4183 case False{}:
4184 match b4:
4185 case True{}:
4186 {==}
4187 case False{}:
4188 {==}
4189
4190def gc.rs.log.bits(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, +b5: Bool, +b6: Bool, +b7: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}))) : U32}:
4191 match b5 b6 b7:
4192 case True{} True{} True{}:
4193 gc.rs.log.bits.s111(b0, b1, b2, b3, b4)
4194 case True{} True{} False{}:
4195 gc.rs.log.bits.s011(b0, b1, b2, b3, b4)
4196 case True{} False{} True{}:
4197 gc.rs.log.bits.s101(b0, b1, b2, b3, b4)
4198 case True{} False{} False{}:
4199 gc.rs.log.bits.s001(b0, b1, b2, b3, b4)
4200 case False{} True{} True{}:
4201 gc.rs.log.bits.s110(b0, b1, b2, b3, b4)
4202 case False{} True{} False{}:
4203 gc.rs.log.bits.s010(b0, b1, b2, b3, b4)
4204 case False{} False{} True{}:
4205 gc.rs.log.bits.s100(b0, b1, b2, b3, b4)
4206 case False{} False{} False{}:
4207 gc.rs.log.bits.s000(b0, b1, b2, b3, b4)
4208
4209def gc.rs.log(+a: U32) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8.elt(a)), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), a)) : U32}:
4210 match a:
4211 case U32{WCon{+b0, WCon{+b1, WCon{+b2, WCon{+b3, WCon{+b4, WCon{+b5, WCon{+b6, WCon{+b7, +r}}}}}}}}}:
4212 gc.rs.log.bits(b0, b1, b2, b3, b4, b5, b6, b7)