def gc.isz.bits.s010

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

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

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