def gc.isz.bits.s100

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

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

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