def exp_log_aes.s10110

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

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

3297def exp_log_aes.s10110(+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{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, b5, b6, b7})) : U32}:
3298  match b5:
3299    case True{}:
3300      match b6:
3301        case True{}:
3302          match b7:
3303            case True{}:
3304              {==}
3305            case False{}:
3306              {==}
3307        case False{}:
3308          match b7:
3309            case True{}:
3310              {==}
3311            case False{}:
3312              {==}
3313    case False{}:
3314      match b6:
3315        case True{}:
3316          match b7:
3317            case True{}:
3318              {==}
3319            case False{}:
3320              {==}
3321        case False{}:
3322          match b7:
3323            case True{}:
3324              {==}
3325            case False{}:
3326              {==}