def dec
import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOFimport Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
586# every byte is the sum of its bits times the basis (by cases)
587def dec(+a: G.Gf8Bits) -> {ss(bl(a), basis()) == a : G.Gf8Bits}:
588 match a:
589 case G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}:
590 match b0:
591 case True{}:
592 match b1:
593 case True{}:
594 match b2:
595 case True{}:
596 match b3:
597 case True{}:
598 match b4:
599 case True{}:
600 match b5:
601 case True{}:
602 match b6:
603 case True{}:
604 match b7:
605 case True{}:
606 {==}
607 case False{}:
608 {==}
609 case False{}:
610 match b7:
611 case True{}:
612 {==}
613 case False{}:
614 {==}
615 case False{}:
616 match b6:
617 case True{}:
618 match b7:
619 case True{}:
620 {==}
621 case False{}:
622 {==}
623 case False{}:
624 match b7:
625 case True{}:
626 {==}
627 case False{}:
628 {==}
629 case False{}:
630 match b5:
631 case True{}:
632 match b6:
633 case True{}:
634 match b7:
635 case True{}:
636 {==}
637 case False{}:
638 {==}
639 case False{}:
640 match b7:
641 case True{}:
642 {==}
643 case False{}:
644 {==}
645 case False{}:
646 match b6:
647 case True{}:
648 match b7:
649 case True{}:
650 {==}
651 case False{}:
652 {==}
653 case False{}:
654 match b7:
655 case True{}:
656 {==}
657 case False{}:
658 {==}
659 case False{}:
660 match b4:
661 case True{}:
662 match b5:
663 case True{}:
664 match b6:
665 case True{}:
666 match b7:
667 case True{}:
668 {==}
669 case False{}:
670 {==}
671 case False{}:
672 match b7:
673 case True{}:
674 {==}
675 case False{}:
676 {==}
677 case False{}:
678 match b6:
679 case True{}:
680 match b7:
681 case True{}:
682 {==}
683 case False{}:
684 {==}
685 case False{}:
686 match b7:
687 case True{}:
688 {==}
689 case False{}:
690 {==}
691 case False{}:
692 match b5:
693 case True{}:
694 match b6:
695 case True{}:
696 match b7:
697 case True{}:
698 {==}
699 case False{}:
700 {==}
701 case False{}:
702 match b7:
703 case True{}:
704 {==}
705 case False{}:
706 {==}
707 case False{}:
708 match b6:
709 case True{}:
710 match b7:
711 case True{}:
712 {==}
713 case False{}:
714 {==}
715 case False{}:
716 match b7:
717 case True{}:
718 {==}
719 case False{}:
720 {==}
721 case False{}:
722 match b3:
723 case True{}:
724 match b4:
725 case True{}:
726 match b5:
727 case True{}:
728 match b6:
729 case True{}:
730 match b7:
731 case True{}:
732 {==}
733 case False{}:
734 {==}
735 case False{}:
736 match b7:
737 case True{}:
738 {==}
739 case False{}:
740 {==}
741 case False{}:
742 match b6:
743 case True{}:
744 match b7:
745 case True{}:
746 {==}
747 case False{}:
748 {==}
749 case False{}:
750 match b7:
751 case True{}:
752 {==}
753 case False{}:
754 {==}
755 case False{}:
756 match b5:
757 case True{}:
758 match b6:
759 case True{}:
760 match b7:
761 case True{}:
762 {==}
763 case False{}:
764 {==}
765 case False{}:
766 match b7:
767 case True{}:
768 {==}
769 case False{}:
770 {==}
771 case False{}:
772 match b6:
773 case True{}:
774 match b7:
775 case True{}:
776 {==}
777 case False{}:
778 {==}
779 case False{}:
780 match b7:
781 case True{}:
782 {==}
783 case False{}:
784 {==}
785 case False{}:
786 match b4:
787 case True{}:
788 match b5:
789 case True{}:
790 match b6:
791 case True{}:
792 match b7:
793 case True{}:
794 {==}
795 case False{}:
796 {==}
797 case False{}:
798 match b7:
799 case True{}:
800 {==}
801 case False{}:
802 {==}
803 case False{}:
804 match b6:
805 case True{}:
806 match b7:
807 case True{}:
808 {==}
809 case False{}:
810 {==}
811 case False{}:
812 match b7:
813 case True{}:
814 {==}
815 case False{}:
816 {==}
817 case False{}:
818 match b5:
819 case True{}:
820 match b6:
821 case True{}:
822 match b7:
823 case True{}:
824 {==}
825 case False{}:
826 {==}
827 case False{}:
828 match b7:
829 case True{}:
830 {==}
831 case False{}:
832 {==}
833 case False{}:
834 match b6:
835 case True{}:
836 match b7:
837 case True{}:
838 {==}
839 case False{}:
840 {==}
841 case False{}:
842 match b7:
843 case True{}:
844 {==}
845 case False{}:
846 {==}
847 case False{}:
848 match b2:
849 case True{}:
850 match b3:
851 case True{}:
852 match b4:
853 case True{}:
854 match b5:
855 case True{}:
856 match b6:
857 case True{}:
858 match b7:
859 case True{}:
860 {==}
861 case False{}:
862 {==}
863 case False{}:
864 match b7:
865 case True{}:
866 {==}
867 case False{}:
868 {==}
869 case False{}:
870 match b6:
871 case True{}:
872 match b7:
873 case True{}:
874 {==}
875 case False{}:
876 {==}
877 case False{}:
878 match b7:
879 case True{}:
880 {==}
881 case False{}:
882 {==}
883 case False{}:
884 match b5:
885 case True{}:
886 match b6:
887 case True{}:
888 match b7:
889 case True{}:
890 {==}
891 case False{}:
892 {==}
893 case False{}:
894 match b7:
895 case True{}:
896 {==}
897 case False{}:
898 {==}
899 case False{}:
900 match b6:
901 case True{}:
902 match b7:
903 case True{}:
904 {==}
905 case False{}:
906 {==}
907 case False{}:
908 match b7:
909 case True{}:
910 {==}
911 case False{}:
912 {==}
913 case False{}:
914 match b4:
915 case True{}:
916 match b5:
917 case True{}:
918 match b6:
919 case True{}:
920 match b7:
921 case True{}:
922 {==}
923 case False{}:
924 {==}
925 case False{}:
926 match b7:
927 case True{}:
928 {==}
929 case False{}:
930 {==}
931 case False{}:
932 match b6:
933 case True{}:
934 match b7:
935 case True{}:
936 {==}
937 case False{}:
938 {==}
939 case False{}:
940 match b7:
941 case True{}:
942 {==}
943 case False{}:
944 {==}
945 case False{}:
946 match b5:
947 case True{}:
948 match b6:
949 case True{}:
950 match b7:
951 case True{}:
952 {==}
953 case False{}:
954 {==}
955 case False{}:
956 match b7:
957 case True{}:
958 {==}
959 case False{}:
960 {==}
961 case False{}:
962 match b6:
963 case True{}:
964 match b7:
965 case True{}:
966 {==}
967 case False{}:
968 {==}
969 case False{}:
970 match b7:
971 case True{}:
972 {==}
973 case False{}:
974 {==}
975 case False{}:
976 match b3:
977 case True{}:
978 match b4:
979 case True{}:
980 match b5:
981 case True{}:
982 match b6:
983 case True{}:
984 match b7:
985 case True{}:
986 {==}
987 case False{}:
988 {==}
989 case False{}:
990 match b7:
991 case True{}:
992 {==}
993 case False{}:
994 {==}
995 case False{}:
996 match b6:
997 case True{}:
998 match b7:
999 case True{}:
1000 {==}
1001 case False{}:
1002 {==}
1003 case False{}:
1004 match b7:
1005 case True{}:
1006 {==}
1007 case False{}:
1008 {==}
1009 case False{}:
1010 match b5:
1011 case True{}:
1012 match b6:
1013 case True{}:
1014 match b7:
1015 case True{}:
1016 {==}
1017 case False{}:
1018 {==}
1019 case False{}:
1020 match b7:
1021 case True{}:
1022 {==}
1023 case False{}:
1024 {==}
1025 case False{}:
1026 match b6:
1027 case True{}:
1028 match b7:
1029 case True{}:
1030 {==}
1031 case False{}:
1032 {==}
1033 case False{}:
1034 match b7:
1035 case True{}:
1036 {==}
1037 case False{}:
1038 {==}
1039 case False{}:
1040 match b4:
1041 case True{}:
1042 match b5:
1043 case True{}:
1044 match b6:
1045 case True{}:
1046 match b7:
1047 case True{}:
1048 {==}
1049 case False{}:
1050 {==}
1051 case False{}:
1052 match b7:
1053 case True{}:
1054 {==}
1055 case False{}:
1056 {==}
1057 case False{}:
1058 match b6:
1059 case True{}:
1060 match b7:
1061 case True{}:
1062 {==}
1063 case False{}:
1064 {==}
1065 case False{}:
1066 match b7:
1067 case True{}:
1068 {==}
1069 case False{}:
1070 {==}
1071 case False{}:
1072 match b5:
1073 case True{}:
1074 match b6:
1075 case True{}:
1076 match b7:
1077 case True{}:
1078 {==}
1079 case False{}:
1080 {==}
1081 case False{}:
1082 match b7:
1083 case True{}:
1084 {==}
1085 case False{}:
1086 {==}
1087 case False{}:
1088 match b6:
1089 case True{}:
1090 match b7:
1091 case True{}:
1092 {==}
1093 case False{}:
1094 {==}
1095 case False{}:
1096 match b7:
1097 case True{}:
1098 {==}
1099 case False{}:
1100 {==}
1101 case False{}:
1102 match b1:
1103 case True{}:
1104 match b2:
1105 case True{}:
1106 match b3:
1107 case True{}:
1108 match b4:
1109 case True{}:
1110 match b5:
1111 case True{}:
1112 match b6:
1113 case True{}:
1114 match b7:
1115 case True{}:
1116 {==}
1117 case False{}:
1118 {==}
1119 case False{}:
1120 match b7:
1121 case True{}:
1122 {==}
1123 case False{}:
1124 {==}
1125 case False{}:
1126 match b6:
1127 case True{}:
1128 match b7:
1129 case True{}:
1130 {==}
1131 case False{}:
1132 {==}
1133 case False{}:
1134 match b7:
1135 case True{}:
1136 {==}
1137 case False{}:
1138 {==}
1139 case False{}:
1140 match b5:
1141 case True{}:
1142 match b6:
1143 case True{}:
1144 match b7:
1145 case True{}:
1146 {==}
1147 case False{}:
1148 {==}
1149 case False{}:
1150 match b7:
1151 case True{}:
1152 {==}
1153 case False{}:
1154 {==}
1155 case False{}:
1156 match b6:
1157 case True{}:
1158 match b7:
1159 case True{}:
1160 {==}
1161 case False{}:
1162 {==}
1163 case False{}:
1164 match b7:
1165 case True{}:
1166 {==}
1167 case False{}:
1168 {==}
1169 case False{}:
1170 match b4:
1171 case True{}:
1172 match b5:
1173 case True{}:
1174 match b6:
1175 case True{}:
1176 match b7:
1177 case True{}:
1178 {==}
1179 case False{}:
1180 {==}
1181 case False{}:
1182 match b7:
1183 case True{}:
1184 {==}
1185 case False{}:
1186 {==}
1187 case False{}:
1188 match b6:
1189 case True{}:
1190 match b7:
1191 case True{}:
1192 {==}
1193 case False{}:
1194 {==}
1195 case False{}:
1196 match b7:
1197 case True{}:
1198 {==}
1199 case False{}:
1200 {==}
1201 case False{}:
1202 match b5:
1203 case True{}:
1204 match b6:
1205 case True{}:
1206 match b7:
1207 case True{}:
1208 {==}
1209 case False{}:
1210 {==}
1211 case False{}:
1212 match b7:
1213 case True{}:
1214 {==}
1215 case False{}:
1216 {==}
1217 case False{}:
1218 match b6:
1219 case True{}:
1220 match b7:
1221 case True{}:
1222 {==}
1223 case False{}:
1224 {==}
1225 case False{}:
1226 match b7:
1227 case True{}:
1228 {==}
1229 case False{}:
1230 {==}
1231 case False{}:
1232 match b3:
1233 case True{}:
1234 match b4:
1235 case True{}:
1236 match b5:
1237 case True{}:
1238 match b6:
1239 case True{}:
1240 match b7:
1241 case True{}:
1242 {==}
1243 case False{}:
1244 {==}
1245 case False{}:
1246 match b7:
1247 case True{}:
1248 {==}
1249 case False{}:
1250 {==}
1251 case False{}:
1252 match b6:
1253 case True{}:
1254 match b7:
1255 case True{}:
1256 {==}
1257 case False{}:
1258 {==}
1259 case False{}:
1260 match b7:
1261 case True{}:
1262 {==}
1263 case False{}:
1264 {==}
1265 case False{}:
1266 match b5:
1267 case True{}:
1268 match b6:
1269 case True{}:
1270 match b7:
1271 case True{}:
1272 {==}
1273 case False{}:
1274 {==}
1275 case False{}:
1276 match b7:
1277 case True{}:
1278 {==}
1279 case False{}:
1280 {==}
1281 case False{}:
1282 match b6:
1283 case True{}:
1284 match b7:
1285 case True{}:
1286 {==}
1287 case False{}:
1288 {==}
1289 case False{}:
1290 match b7:
1291 case True{}:
1292 {==}
1293 case False{}:
1294 {==}
1295 case False{}:
1296 match b4:
1297 case True{}:
1298 match b5:
1299 case True{}:
1300 match b6:
1301 case True{}:
1302 match b7:
1303 case True{}:
1304 {==}
1305 case False{}:
1306 {==}
1307 case False{}:
1308 match b7:
1309 case True{}:
1310 {==}
1311 case False{}:
1312 {==}
1313 case False{}:
1314 match b6:
1315 case True{}:
1316 match b7:
1317 case True{}:
1318 {==}
1319 case False{}:
1320 {==}
1321 case False{}:
1322 match b7:
1323 case True{}:
1324 {==}
1325 case False{}:
1326 {==}
1327 case False{}:
1328 match b5:
1329 case True{}:
1330 match b6:
1331 case True{}:
1332 match b7:
1333 case True{}:
1334 {==}
1335 case False{}:
1336 {==}
1337 case False{}:
1338 match b7:
1339 case True{}:
1340 {==}
1341 case False{}:
1342 {==}
1343 case False{}:
1344 match b6:
1345 case True{}:
1346 match b7:
1347 case True{}:
1348 {==}
1349 case False{}:
1350 {==}
1351 case False{}:
1352 match b7:
1353 case True{}:
1354 {==}
1355 case False{}:
1356 {==}
1357 case False{}:
1358 match b2:
1359 case True{}:
1360 match b3:
1361 case True{}:
1362 match b4:
1363 case True{}:
1364 match b5:
1365 case True{}:
1366 match b6:
1367 case True{}:
1368 match b7:
1369 case True{}:
1370 {==}
1371 case False{}:
1372 {==}
1373 case False{}:
1374 match b7:
1375 case True{}:
1376 {==}
1377 case False{}:
1378 {==}
1379 case False{}:
1380 match b6:
1381 case True{}:
1382 match b7:
1383 case True{}:
1384 {==}
1385 case False{}:
1386 {==}
1387 case False{}:
1388 match b7:
1389 case True{}:
1390 {==}
1391 case False{}:
1392 {==}
1393 case False{}:
1394 match b5:
1395 case True{}:
1396 match b6:
1397 case True{}:
1398 match b7:
1399 case True{}:
1400 {==}
1401 case False{}:
1402 {==}
1403 case False{}:
1404 match b7:
1405 case True{}:
1406 {==}
1407 case False{}:
1408 {==}
1409 case False{}:
1410 match b6:
1411 case True{}:
1412 match b7:
1413 case True{}:
1414 {==}
1415 case False{}:
1416 {==}
1417 case False{}:
1418 match b7:
1419 case True{}:
1420 {==}
1421 case False{}:
1422 {==}
1423 case False{}:
1424 match b4:
1425 case True{}:
1426 match b5:
1427 case True{}:
1428 match b6:
1429 case True{}:
1430 match b7:
1431 case True{}:
1432 {==}
1433 case False{}:
1434 {==}
1435 case False{}:
1436 match b7:
1437 case True{}:
1438 {==}
1439 case False{}:
1440 {==}
1441 case False{}:
1442 match b6:
1443 case True{}:
1444 match b7:
1445 case True{}:
1446 {==}
1447 case False{}:
1448 {==}
1449 case False{}:
1450 match b7:
1451 case True{}:
1452 {==}
1453 case False{}:
1454 {==}
1455 case False{}:
1456 match b5:
1457 case True{}:
1458 match b6:
1459 case True{}:
1460 match b7:
1461 case True{}:
1462 {==}
1463 case False{}:
1464 {==}
1465 case False{}:
1466 match b7:
1467 case True{}:
1468 {==}
1469 case False{}:
1470 {==}
1471 case False{}:
1472 match b6:
1473 case True{}:
1474 match b7:
1475 case True{}:
1476 {==}
1477 case False{}:
1478 {==}
1479 case False{}:
1480 match b7:
1481 case True{}:
1482 {==}
1483 case False{}:
1484 {==}
1485 case False{}:
1486 match b3:
1487 case True{}:
1488 match b4:
1489 case True{}:
1490 match b5:
1491 case True{}:
1492 match b6:
1493 case True{}:
1494 match b7:
1495 case True{}:
1496 {==}
1497 case False{}:
1498 {==}
1499 case False{}:
1500 match b7:
1501 case True{}:
1502 {==}
1503 case False{}:
1504 {==}
1505 case False{}:
1506 match b6:
1507 case True{}:
1508 match b7:
1509 case True{}:
1510 {==}
1511 case False{}:
1512 {==}
1513 case False{}:
1514 match b7:
1515 case True{}:
1516 {==}
1517 case False{}:
1518 {==}
1519 case False{}:
1520 match b5:
1521 case True{}:
1522 match b6:
1523 case True{}:
1524 match b7:
1525 case True{}:
1526 {==}
1527 case False{}:
1528 {==}
1529 case False{}:
1530 match b7:
1531 case True{}:
1532 {==}
1533 case False{}:
1534 {==}
1535 case False{}:
1536 match b6:
1537 case True{}:
1538 match b7:
1539 case True{}:
1540 {==}
1541 case False{}:
1542 {==}
1543 case False{}:
1544 match b7:
1545 case True{}:
1546 {==}
1547 case False{}:
1548 {==}
1549 case False{}:
1550 match b4:
1551 case True{}:
1552 match b5:
1553 case True{}:
1554 match b6:
1555 case True{}:
1556 match b7:
1557 case True{}:
1558 {==}
1559 case False{}:
1560 {==}
1561 case False{}:
1562 match b7:
1563 case True{}:
1564 {==}
1565 case False{}:
1566 {==}
1567 case False{}:
1568 match b6:
1569 case True{}:
1570 match b7:
1571 case True{}:
1572 {==}
1573 case False{}:
1574 {==}
1575 case False{}:
1576 match b7:
1577 case True{}:
1578 {==}
1579 case False{}:
1580 {==}
1581 case False{}:
1582 match b5:
1583 case True{}:
1584 match b6:
1585 case True{}:
1586 match b7:
1587 case True{}:
1588 {==}
1589 case False{}:
1590 {==}
1591 case False{}:
1592 match b7:
1593 case True{}:
1594 {==}
1595 case False{}:
1596 {==}
1597 case False{}:
1598 match b6:
1599 case True{}:
1600 match b7:
1601 case True{}:
1602 {==}
1603 case False{}:
1604 {==}
1605 case False{}:
1606 match b7:
1607 case True{}:
1608 {==}
1609 case False{}:
1610 {==}