def gc.isz.bits.s110

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

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

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