def exp_log_aes.s10011

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

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

3390def exp_log_aes.s10011(+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{}, False{}, True{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, b5, b6, b7})) : U32}:
3391  match b5:
3392    case True{}:
3393      match b6:
3394        case True{}:
3395          match b7:
3396            case True{}:
3397              {==}
3398            case False{}:
3399              {==}
3400        case False{}:
3401          match b7:
3402            case True{}:
3403              {==}
3404            case False{}:
3405              {==}
3406    case False{}:
3407      match b6:
3408        case True{}:
3409          match b7:
3410            case True{}:
3411              {==}
3412            case False{}:
3413              {==}
3414        case False{}:
3415          match b7:
3416            case True{}:
3417              {==}
3418            case False{}:
3419              {==}