def gc.aes.log.bits.s100
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:2878
import bend-osdev-gf@0.1.1.0/proof_tab_cases.bend as ProofTabCases
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
2878def gc.aes.log.bits.s100(+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{}, False{}, True{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, True{}}))) : U32}:
2879 match b0:
2880 case True{}:
2881 match b1:
2882 case True{}:
2883 match b2:
2884 case True{}:
2885 match b3:
2886 case True{}:
2887 match b4:
2888 case True{}:
2889 {==}
2890 case False{}:
2891 {==}
2892 case False{}:
2893 match b4:
2894 case True{}:
2895 {==}
2896 case False{}:
2897 {==}
2898 case False{}:
2899 match b3:
2900 case True{}:
2901 match b4:
2902 case True{}:
2903 {==}
2904 case False{}:
2905 {==}
2906 case False{}:
2907 match b4:
2908 case True{}:
2909 {==}
2910 case False{}:
2911 {==}
2912 case False{}:
2913 match b2:
2914 case True{}:
2915 match b3:
2916 case True{}:
2917 match b4:
2918 case True{}:
2919 {==}
2920 case False{}:
2921 {==}
2922 case False{}:
2923 match b4:
2924 case True{}:
2925 {==}
2926 case False{}:
2927 {==}
2928 case False{}:
2929 match b3:
2930 case True{}:
2931 match b4:
2932 case True{}:
2933 {==}
2934 case False{}:
2935 {==}
2936 case False{}:
2937 match b4:
2938 case True{}:
2939 {==}
2940 case False{}:
2941 {==}
2942 case False{}:
2943 match b1:
2944 case True{}:
2945 match b2:
2946 case True{}:
2947 match b3:
2948 case True{}:
2949 match b4:
2950 case True{}:
2951 {==}
2952 case False{}:
2953 {==}
2954 case False{}:
2955 match b4:
2956 case True{}:
2957 {==}
2958 case False{}:
2959 {==}
2960 case False{}:
2961 match b3:
2962 case True{}:
2963 match b4:
2964 case True{}:
2965 {==}
2966 case False{}:
2967 {==}
2968 case False{}:
2969 match b4:
2970 case True{}:
2971 {==}
2972 case False{}:
2973 {==}
2974 case False{}:
2975 match b2:
2976 case True{}:
2977 match b3:
2978 case True{}:
2979 match b4:
2980 case True{}:
2981 {==}
2982 case False{}:
2983 {==}
2984 case False{}:
2985 match b4:
2986 case True{}:
2987 {==}
2988 case False{}:
2989 {==}
2990 case False{}:
2991 match b3:
2992 case True{}:
2993 match b4:
2994 case True{}:
2995 {==}
2996 case False{}:
2997 {==}
2998 case False{}:
2999 match b4:
3000 case True{}:
3001 {==}
3002 case False{}:
3003 {==}