def gc.aes.log.bits.s000

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

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

3005def gc.aes.log.bits.s000(+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{}, False{}})), 0) == U32.from_nat(G.Gf8.log(G.Gf8.aes(), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, False{}, False{}}))) : U32}:
3006  match b0:
3007    case True{}:
3008      match b1:
3009        case True{}:
3010          match b2:
3011            case True{}:
3012              match b3:
3013                case True{}:
3014                  match b4:
3015                    case True{}:
3016                      {==}
3017                    case False{}:
3018                      {==}
3019                case False{}:
3020                  match b4:
3021                    case True{}:
3022                      {==}
3023                    case False{}:
3024                      {==}
3025            case False{}:
3026              match b3:
3027                case True{}:
3028                  match b4:
3029                    case True{}:
3030                      {==}
3031                    case False{}:
3032                      {==}
3033                case False{}:
3034                  match b4:
3035                    case True{}:
3036                      {==}
3037                    case False{}:
3038                      {==}
3039        case False{}:
3040          match b2:
3041            case True{}:
3042              match b3:
3043                case True{}:
3044                  match b4:
3045                    case True{}:
3046                      {==}
3047                    case False{}:
3048                      {==}
3049                case False{}:
3050                  match b4:
3051                    case True{}:
3052                      {==}
3053                    case False{}:
3054                      {==}
3055            case False{}:
3056              match b3:
3057                case True{}:
3058                  match b4:
3059                    case True{}:
3060                      {==}
3061                    case False{}:
3062                      {==}
3063                case False{}:
3064                  match b4:
3065                    case True{}:
3066                      {==}
3067                    case False{}:
3068                      {==}
3069    case False{}:
3070      match b1:
3071        case True{}:
3072          match b2:
3073            case True{}:
3074              match b3:
3075                case True{}:
3076                  match b4:
3077                    case True{}:
3078                      {==}
3079                    case False{}:
3080                      {==}
3081                case False{}:
3082                  match b4:
3083                    case True{}:
3084                      {==}
3085                    case False{}:
3086                      {==}
3087            case False{}:
3088              match b3:
3089                case True{}:
3090                  match b4:
3091                    case True{}:
3092                      {==}
3093                    case False{}:
3094                      {==}
3095                case False{}:
3096                  match b4:
3097                    case True{}:
3098                      {==}
3099                    case False{}:
3100                      {==}
3101        case False{}:
3102          match b2:
3103            case True{}:
3104              match b3:
3105                case True{}:
3106                  match b4:
3107                    case True{}:
3108                      {==}
3109                    case False{}:
3110                      {==}
3111                case False{}:
3112                  match b4:
3113                    case True{}:
3114                      {==}
3115                    case False{}:
3116                      {==}
3117            case False{}:
3118              match b3:
3119                case True{}:
3120                  match b4:
3121                    case True{}:
3122                      {==}
3123                    case False{}:
3124                      {==}
3125                case False{}:
3126                  match b4:
3127                    case True{}:
3128                      {==}
3129                    case False{}:
3130                      {==}