def exp_log_aes.s11100

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

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

3111def exp_log_aes.s11100(+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{}, True{}, True{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, b5, b6, b7})) : U32}:
3112  match b5:
3113    case True{}:
3114      match b6:
3115        case True{}:
3116          match b7:
3117            case True{}:
3118              {==}
3119            case False{}:
3120              {==}
3121        case False{}:
3122          match b7:
3123            case True{}:
3124              {==}
3125            case False{}:
3126              {==}
3127    case False{}:
3128      match b6:
3129        case True{}:
3130          match b7:
3131            case True{}:
3132              {==}
3133            case False{}:
3134              {==}
3135        case False{}:
3136          match b7:
3137            case True{}:
3138              {==}
3139            case False{}:
3140              {==}