def gc.isz.bits.s000

bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:905

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

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                      {==}