def gc.rs.log.bits.s000

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

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

4063def gc.rs.log.bits.s000(+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{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}}))) : U32}:
4064  match b0:
4065    case True{}:
4066      match b1:
4067        case True{}:
4068          match b2:
4069            case True{}:
4070              match b3:
4071                case True{}:
4072                  match b4:
4073                    case True{}:
4074                      {==}
4075                    case False{}:
4076                      {==}
4077                case False{}:
4078                  match b4:
4079                    case True{}:
4080                      {==}
4081                    case False{}:
4082                      {==}
4083            case False{}:
4084              match b3:
4085                case True{}:
4086                  match b4:
4087                    case True{}:
4088                      {==}
4089                    case False{}:
4090                      {==}
4091                case False{}:
4092                  match b4:
4093                    case True{}:
4094                      {==}
4095                    case False{}:
4096                      {==}
4097        case False{}:
4098          match b2:
4099            case True{}:
4100              match b3:
4101                case True{}:
4102                  match b4:
4103                    case True{}:
4104                      {==}
4105                    case False{}:
4106                      {==}
4107                case False{}:
4108                  match b4:
4109                    case True{}:
4110                      {==}
4111                    case False{}:
4112                      {==}
4113            case False{}:
4114              match b3:
4115                case True{}:
4116                  match b4:
4117                    case True{}:
4118                      {==}
4119                    case False{}:
4120                      {==}
4121                case False{}:
4122                  match b4:
4123                    case True{}:
4124                      {==}
4125                    case False{}:
4126                      {==}
4127    case False{}:
4128      match b1:
4129        case True{}:
4130          match b2:
4131            case True{}:
4132              match b3:
4133                case True{}:
4134                  match b4:
4135                    case True{}:
4136                      {==}
4137                    case False{}:
4138                      {==}
4139                case False{}:
4140                  match b4:
4141                    case True{}:
4142                      {==}
4143                    case False{}:
4144                      {==}
4145            case False{}:
4146              match b3:
4147                case True{}:
4148                  match b4:
4149                    case True{}:
4150                      {==}
4151                    case False{}:
4152                      {==}
4153                case False{}:
4154                  match b4:
4155                    case True{}:
4156                      {==}
4157                    case False{}:
4158                      {==}
4159        case False{}:
4160          match b2:
4161            case True{}:
4162              match b3:
4163                case True{}:
4164                  match b4:
4165                    case True{}:
4166                      {==}
4167                    case False{}:
4168                      {==}
4169                case False{}:
4170                  match b4:
4171                    case True{}:
4172                      {==}
4173                    case False{}:
4174                      {==}
4175            case False{}:
4176              match b3:
4177                case True{}:
4178                  match b4:
4179                    case True{}:
4180                      {==}
4181                    case False{}:
4182                      {==}
4183                case False{}:
4184                  match b4:
4185                    case True{}:
4186                      {==}
4187                    case False{}:
4188                      {==}