def exp_log_aes.s10111

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

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

3266def exp_log_aes.s10111(+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{}, False{}, True{}, True{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, b5, b6, b7})) : U32}:
3267  match b5:
3268    case True{}:
3269      match b6:
3270        case True{}:
3271          match b7:
3272            case True{}:
3273              {==}
3274            case False{}:
3275              {==}
3276        case False{}:
3277          match b7:
3278            case True{}:
3279              {==}
3280            case False{}:
3281              {==}
3282    case False{}:
3283      match b6:
3284        case True{}:
3285          match b7:
3286            case True{}:
3287              {==}
3288            case False{}:
3289              {==}
3290        case False{}:
3291          match b7:
3292            case True{}:
3293              {==}
3294            case False{}:
3295              {==}