def exp_log_aes.s01011

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

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

3638def exp_log_aes.s01011(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.exp(G.Gf8.aes(), G.Gf8.log(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, b5, b6, b7})) : U32}:
3639  match b5:
3640    case True{}:
3641      match b6:
3642        case True{}:
3643          match b7:
3644            case True{}:
3645              {==}
3646            case False{}:
3647              {==}
3648        case False{}:
3649          match b7:
3650            case True{}:
3651              {==}
3652            case False{}:
3653              {==}
3654    case False{}:
3655      match b6:
3656        case True{}:
3657          match b7:
3658            case True{}:
3659              {==}
3660            case False{}:
3661              {==}
3662        case False{}:
3663          match b7:
3664            case True{}:
3665              {==}
3666            case False{}:
3667              {==}