def gc.aes.log.bits.s001

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

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

2497def gc.aes.log.bits.s001(+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{}, False{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}))) : U32}:
2498  match b0:
2499    case True{}:
2500      match b1:
2501        case True{}:
2502          match b2:
2503            case True{}:
2504              match b3:
2505                case True{}:
2506                  match b4:
2507                    case True{}:
2508                      {==}
2509                    case False{}:
2510                      {==}
2511                case False{}:
2512                  match b4:
2513                    case True{}:
2514                      {==}
2515                    case False{}:
2516                      {==}
2517            case False{}:
2518              match b3:
2519                case True{}:
2520                  match b4:
2521                    case True{}:
2522                      {==}
2523                    case False{}:
2524                      {==}
2525                case False{}:
2526                  match b4:
2527                    case True{}:
2528                      {==}
2529                    case False{}:
2530                      {==}
2531        case False{}:
2532          match b2:
2533            case True{}:
2534              match b3:
2535                case True{}:
2536                  match b4:
2537                    case True{}:
2538                      {==}
2539                    case False{}:
2540                      {==}
2541                case False{}:
2542                  match b4:
2543                    case True{}:
2544                      {==}
2545                    case False{}:
2546                      {==}
2547            case False{}:
2548              match b3:
2549                case True{}:
2550                  match b4:
2551                    case True{}:
2552                      {==}
2553                    case False{}:
2554                      {==}
2555                case False{}:
2556                  match b4:
2557                    case True{}:
2558                      {==}
2559                    case False{}:
2560                      {==}
2561    case False{}:
2562      match b1:
2563        case True{}:
2564          match b2:
2565            case True{}:
2566              match b3:
2567                case True{}:
2568                  match b4:
2569                    case True{}:
2570                      {==}
2571                    case False{}:
2572                      {==}
2573                case False{}:
2574                  match b4:
2575                    case True{}:
2576                      {==}
2577                    case False{}:
2578                      {==}
2579            case False{}:
2580              match b3:
2581                case True{}:
2582                  match b4:
2583                    case True{}:
2584                      {==}
2585                    case False{}:
2586                      {==}
2587                case False{}:
2588                  match b4:
2589                    case True{}:
2590                      {==}
2591                    case False{}:
2592                      {==}
2593        case False{}:
2594          match b2:
2595            case True{}:
2596              match b3:
2597                case True{}:
2598                  match b4:
2599                    case True{}:
2600                      {==}
2601                    case False{}:
2602                      {==}
2603                case False{}:
2604                  match b4:
2605                    case True{}:
2606                      {==}
2607                    case False{}:
2608                      {==}
2609            case False{}:
2610              match b3:
2611                case True{}:
2612                  match b4:
2613                    case True{}:
2614                      {==}
2615                    case False{}:
2616                      {==}
2617                case False{}:
2618                  match b4:
2619                    case True{}:
2620                      {==}
2621                    case False{}:
2622                      {==}