def exp_log_aes.s00111

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

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

3762def exp_log_aes.s00111(+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{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, b5, b6, b7})) : U32}:
3763  match b5:
3764    case True{}:
3765      match b6:
3766        case True{}:
3767          match b7:
3768            case True{}:
3769              {==}
3770            case False{}:
3771              {==}
3772        case False{}:
3773          match b7:
3774            case True{}:
3775              {==}
3776            case False{}:
3777              {==}
3778    case False{}:
3779      match b6:
3780        case True{}:
3781          match b7:
3782            case True{}:
3783              {==}
3784            case False{}:
3785              {==}
3786        case False{}:
3787          match b7:
3788            case True{}:
3789              {==}
3790            case False{}:
3791              {==}