def exp_log_aes.s10010

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

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

3421def exp_log_aes.s10010(+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{}, False{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, b5, b6, b7})) : U32}:
3422  match b5:
3423    case True{}:
3424      match b6:
3425        case True{}:
3426          match b7:
3427            case True{}:
3428              {==}
3429            case False{}:
3430              {==}
3431        case False{}:
3432          match b7:
3433            case True{}:
3434              {==}
3435            case False{}:
3436              {==}
3437    case False{}:
3438      match b6:
3439        case True{}:
3440          match b7:
3441            case True{}:
3442              {==}
3443            case False{}:
3444              {==}
3445        case False{}:
3446          match b7:
3447            case True{}:
3448              {==}
3449            case False{}:
3450              {==}