def gc.aes.log.bits.s011

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

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

2243def gc.aes.log.bits.s011(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {A.Arrays.nth(U32, gc.aes.llist(), A.Arrays.index(8n, G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}))) : U32}:
2244  match b0:
2245    case True{}:
2246      match b1:
2247        case True{}:
2248          match b2:
2249            case True{}:
2250              match b3:
2251                case True{}:
2252                  match b4:
2253                    case True{}:
2254                      {==}
2255                    case False{}:
2256                      {==}
2257                case False{}:
2258                  match b4:
2259                    case True{}:
2260                      {==}
2261                    case False{}:
2262                      {==}
2263            case False{}:
2264              match b3:
2265                case True{}:
2266                  match b4:
2267                    case True{}:
2268                      {==}
2269                    case False{}:
2270                      {==}
2271                case False{}:
2272                  match b4:
2273                    case True{}:
2274                      {==}
2275                    case False{}:
2276                      {==}
2277        case False{}:
2278          match b2:
2279            case True{}:
2280              match b3:
2281                case True{}:
2282                  match b4:
2283                    case True{}:
2284                      {==}
2285                    case False{}:
2286                      {==}
2287                case False{}:
2288                  match b4:
2289                    case True{}:
2290                      {==}
2291                    case False{}:
2292                      {==}
2293            case False{}:
2294              match b3:
2295                case True{}:
2296                  match b4:
2297                    case True{}:
2298                      {==}
2299                    case False{}:
2300                      {==}
2301                case False{}:
2302                  match b4:
2303                    case True{}:
2304                      {==}
2305                    case False{}:
2306                      {==}
2307    case False{}:
2308      match b1:
2309        case True{}:
2310          match b2:
2311            case True{}:
2312              match b3:
2313                case True{}:
2314                  match b4:
2315                    case True{}:
2316                      {==}
2317                    case False{}:
2318                      {==}
2319                case False{}:
2320                  match b4:
2321                    case True{}:
2322                      {==}
2323                    case False{}:
2324                      {==}
2325            case False{}:
2326              match b3:
2327                case True{}:
2328                  match b4:
2329                    case True{}:
2330                      {==}
2331                    case False{}:
2332                      {==}
2333                case False{}:
2334                  match b4:
2335                    case True{}:
2336                      {==}
2337                    case False{}:
2338                      {==}
2339        case False{}:
2340          match b2:
2341            case True{}:
2342              match b3:
2343                case True{}:
2344                  match b4:
2345                    case True{}:
2346                      {==}
2347                    case False{}:
2348                      {==}
2349                case False{}:
2350                  match b4:
2351                    case True{}:
2352                      {==}
2353                    case False{}:
2354                      {==}
2355            case False{}:
2356              match b3:
2357                case True{}:
2358                  match b4:
2359                    case True{}:
2360                      {==}
2361                    case False{}:
2362                      {==}
2363                case False{}:
2364                  match b4:
2365                    case True{}:
2366                      {==}
2367                    case False{}:
2368                      {==}