def gc.aes.log.bits.s010

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

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

2751def gc.aes.log.bits.s010(+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, False{}, True{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}}))) : U32}:
2752  match b0:
2753    case True{}:
2754      match b1:
2755        case True{}:
2756          match b2:
2757            case True{}:
2758              match b3:
2759                case True{}:
2760                  match b4:
2761                    case True{}:
2762                      {==}
2763                    case False{}:
2764                      {==}
2765                case False{}:
2766                  match b4:
2767                    case True{}:
2768                      {==}
2769                    case False{}:
2770                      {==}
2771            case False{}:
2772              match b3:
2773                case True{}:
2774                  match b4:
2775                    case True{}:
2776                      {==}
2777                    case False{}:
2778                      {==}
2779                case False{}:
2780                  match b4:
2781                    case True{}:
2782                      {==}
2783                    case False{}:
2784                      {==}
2785        case False{}:
2786          match b2:
2787            case True{}:
2788              match b3:
2789                case True{}:
2790                  match b4:
2791                    case True{}:
2792                      {==}
2793                    case False{}:
2794                      {==}
2795                case False{}:
2796                  match b4:
2797                    case True{}:
2798                      {==}
2799                    case False{}:
2800                      {==}
2801            case False{}:
2802              match b3:
2803                case True{}:
2804                  match b4:
2805                    case True{}:
2806                      {==}
2807                    case False{}:
2808                      {==}
2809                case False{}:
2810                  match b4:
2811                    case True{}:
2812                      {==}
2813                    case False{}:
2814                      {==}
2815    case False{}:
2816      match b1:
2817        case True{}:
2818          match b2:
2819            case True{}:
2820              match b3:
2821                case True{}:
2822                  match b4:
2823                    case True{}:
2824                      {==}
2825                    case False{}:
2826                      {==}
2827                case False{}:
2828                  match b4:
2829                    case True{}:
2830                      {==}
2831                    case False{}:
2832                      {==}
2833            case False{}:
2834              match b3:
2835                case True{}:
2836                  match b4:
2837                    case True{}:
2838                      {==}
2839                    case False{}:
2840                      {==}
2841                case False{}:
2842                  match b4:
2843                    case True{}:
2844                      {==}
2845                    case False{}:
2846                      {==}
2847        case False{}:
2848          match b2:
2849            case True{}:
2850              match b3:
2851                case True{}:
2852                  match b4:
2853                    case True{}:
2854                      {==}
2855                    case False{}:
2856                      {==}
2857                case False{}:
2858                  match b4:
2859                    case True{}:
2860                      {==}
2861                    case False{}:
2862                      {==}
2863            case False{}:
2864              match b3:
2865                case True{}:
2866                  match b4:
2867                    case True{}:
2868                      {==}
2869                    case False{}:
2870                      {==}
2871                case False{}:
2872                  match b4:
2873                    case True{}:
2874                      {==}
2875                    case False{}:
2876                      {==}