def exp_log_aes.s10100

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

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

3359def exp_log_aes.s10100(+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{}, False{}, True{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, b5, b6, b7})) : U32}:
3360  match b5:
3361    case True{}:
3362      match b6:
3363        case True{}:
3364          match b7:
3365            case True{}:
3366              {==}
3367            case False{}:
3368              {==}
3369        case False{}:
3370          match b7:
3371            case True{}:
3372              {==}
3373            case False{}:
3374              {==}
3375    case False{}:
3376      match b6:
3377        case True{}:
3378          match b7:
3379            case True{}:
3380              {==}
3381            case False{}:
3382              {==}
3383        case False{}:
3384          match b7:
3385            case True{}:
3386              {==}
3387            case False{}:
3388              {==}