def exp_log_aes.s00100

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

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

3855def exp_log_aes.s00100(+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{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, b5, b6, b7})) : U32}:
3856  match b5:
3857    case True{}:
3858      match b6:
3859        case True{}:
3860          match b7:
3861            case True{}:
3862              {==}
3863            case False{}:
3864              {==}
3865        case False{}:
3866          match b7:
3867            case True{}:
3868              {==}
3869            case False{}:
3870              {==}
3871    case False{}:
3872      match b6:
3873        case True{}:
3874          match b7:
3875            case True{}:
3876              {==}
3877            case False{}:
3878              {==}
3879        case False{}:
3880          match b7:
3881            case True{}:
3882              {==}
3883            case False{}:
3884              {==}