def gc.rs.log.bits.s100

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

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

3936def gc.rs.log.bits.s100(+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{}, False{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}))) : U32}:
3937  match b0:
3938    case True{}:
3939      match b1:
3940        case True{}:
3941          match b2:
3942            case True{}:
3943              match b3:
3944                case True{}:
3945                  match b4:
3946                    case True{}:
3947                      {==}
3948                    case False{}:
3949                      {==}
3950                case False{}:
3951                  match b4:
3952                    case True{}:
3953                      {==}
3954                    case False{}:
3955                      {==}
3956            case False{}:
3957              match b3:
3958                case True{}:
3959                  match b4:
3960                    case True{}:
3961                      {==}
3962                    case False{}:
3963                      {==}
3964                case False{}:
3965                  match b4:
3966                    case True{}:
3967                      {==}
3968                    case False{}:
3969                      {==}
3970        case False{}:
3971          match b2:
3972            case True{}:
3973              match b3:
3974                case True{}:
3975                  match b4:
3976                    case True{}:
3977                      {==}
3978                    case False{}:
3979                      {==}
3980                case False{}:
3981                  match b4:
3982                    case True{}:
3983                      {==}
3984                    case False{}:
3985                      {==}
3986            case False{}:
3987              match b3:
3988                case True{}:
3989                  match b4:
3990                    case True{}:
3991                      {==}
3992                    case False{}:
3993                      {==}
3994                case False{}:
3995                  match b4:
3996                    case True{}:
3997                      {==}
3998                    case False{}:
3999                      {==}
4000    case False{}:
4001      match b1:
4002        case True{}:
4003          match b2:
4004            case True{}:
4005              match b3:
4006                case True{}:
4007                  match b4:
4008                    case True{}:
4009                      {==}
4010                    case False{}:
4011                      {==}
4012                case False{}:
4013                  match b4:
4014                    case True{}:
4015                      {==}
4016                    case False{}:
4017                      {==}
4018            case False{}:
4019              match b3:
4020                case True{}:
4021                  match b4:
4022                    case True{}:
4023                      {==}
4024                    case False{}:
4025                      {==}
4026                case False{}:
4027                  match b4:
4028                    case True{}:
4029                      {==}
4030                    case False{}:
4031                      {==}
4032        case False{}:
4033          match b2:
4034            case True{}:
4035              match b3:
4036                case True{}:
4037                  match b4:
4038                    case True{}:
4039                      {==}
4040                    case False{}:
4041                      {==}
4042                case False{}:
4043                  match b4:
4044                    case True{}:
4045                      {==}
4046                    case False{}:
4047                      {==}
4048            case False{}:
4049              match b3:
4050                case True{}:
4051                  match b4:
4052                    case True{}:
4053                      {==}
4054                    case False{}:
4055                      {==}
4056                case False{}:
4057                  match b4:
4058                    case True{}:
4059                      {==}
4060                    case False{}:
4061                      {==}