def gc.rs.log.bits.s010

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

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

3809def gc.rs.log.bits.s010(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}}))) : U32}:
3810  match b0:
3811    case True{}:
3812      match b1:
3813        case True{}:
3814          match b2:
3815            case True{}:
3816              match b3:
3817                case True{}:
3818                  match b4:
3819                    case True{}:
3820                      {==}
3821                    case False{}:
3822                      {==}
3823                case False{}:
3824                  match b4:
3825                    case True{}:
3826                      {==}
3827                    case False{}:
3828                      {==}
3829            case False{}:
3830              match b3:
3831                case True{}:
3832                  match b4:
3833                    case True{}:
3834                      {==}
3835                    case False{}:
3836                      {==}
3837                case False{}:
3838                  match b4:
3839                    case True{}:
3840                      {==}
3841                    case False{}:
3842                      {==}
3843        case False{}:
3844          match b2:
3845            case True{}:
3846              match b3:
3847                case True{}:
3848                  match b4:
3849                    case True{}:
3850                      {==}
3851                    case False{}:
3852                      {==}
3853                case False{}:
3854                  match b4:
3855                    case True{}:
3856                      {==}
3857                    case False{}:
3858                      {==}
3859            case False{}:
3860              match b3:
3861                case True{}:
3862                  match b4:
3863                    case True{}:
3864                      {==}
3865                    case False{}:
3866                      {==}
3867                case False{}:
3868                  match b4:
3869                    case True{}:
3870                      {==}
3871                    case False{}:
3872                      {==}
3873    case False{}:
3874      match b1:
3875        case True{}:
3876          match b2:
3877            case True{}:
3878              match b3:
3879                case True{}:
3880                  match b4:
3881                    case True{}:
3882                      {==}
3883                    case False{}:
3884                      {==}
3885                case False{}:
3886                  match b4:
3887                    case True{}:
3888                      {==}
3889                    case False{}:
3890                      {==}
3891            case False{}:
3892              match b3:
3893                case True{}:
3894                  match b4:
3895                    case True{}:
3896                      {==}
3897                    case False{}:
3898                      {==}
3899                case False{}:
3900                  match b4:
3901                    case True{}:
3902                      {==}
3903                    case False{}:
3904                      {==}
3905        case False{}:
3906          match b2:
3907            case True{}:
3908              match b3:
3909                case True{}:
3910                  match b4:
3911                    case True{}:
3912                      {==}
3913                    case False{}:
3914                      {==}
3915                case False{}:
3916                  match b4:
3917                    case True{}:
3918                      {==}
3919                    case False{}:
3920                      {==}
3921            case False{}:
3922              match b3:
3923                case True{}:
3924                  match b4:
3925                    case True{}:
3926                      {==}
3927                    case False{}:
3928                      {==}
3929                case False{}:
3930                  match b4:
3931                    case True{}:
3932                      {==}
3933                    case False{}:
3934                      {==}