def exp_log_aes.s11010

bend-osdev-gf@0.1.1.0 · PROOF.bend:3173

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

3173def exp_log_aes.s11010(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.exp(G.Gf8.aes(), G.Gf8.log(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, b5, b6, b7})) : U32}:
3174  match b5:
3175    case True{}:
3176      match b6:
3177        case True{}:
3178          match b7:
3179            case True{}:
3180              {==}
3181            case False{}:
3182              {==}
3183        case False{}:
3184          match b7:
3185            case True{}:
3186              {==}
3187            case False{}:
3188              {==}
3189    case False{}:
3190      match b6:
3191        case True{}:
3192          match b7:
3193            case True{}:
3194              {==}
3195            case False{}:
3196              {==}
3197        case False{}:
3198          match b7:
3199            case True{}:
3200              {==}
3201            case False{}:
3202              {==}