def exp_log_aes.s00110

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

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

3793def exp_log_aes.s00110(+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{}, False{}, True{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, b5, b6, b7})) : U32}:
3794  match b5:
3795    case True{}:
3796      match b6:
3797        case True{}:
3798          match b7:
3799            case True{}:
3800              {==}
3801            case False{}:
3802              {==}
3803        case False{}:
3804          match b7:
3805            case True{}:
3806              {==}
3807            case False{}:
3808              {==}
3809    case False{}:
3810      match b6:
3811        case True{}:
3812          match b7:
3813            case True{}:
3814              {==}
3815            case False{}:
3816              {==}
3817        case False{}:
3818          match b7:
3819            case True{}:
3820              {==}
3821            case False{}:
3822              {==}