def exp_log_aes.s11110

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

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

3049def exp_log_aes.s11110(+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{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, b5, b6, b7})) : U32}:
3050  match b5:
3051    case True{}:
3052      match b6:
3053        case True{}:
3054          match b7:
3055            case True{}:
3056              {==}
3057            case False{}:
3058              {==}
3059        case False{}:
3060          match b7:
3061            case True{}:
3062              {==}
3063            case False{}:
3064              {==}
3065    case False{}:
3066      match b6:
3067        case True{}:
3068          match b7:
3069            case True{}:
3070              {==}
3071            case False{}:
3072              {==}
3073        case False{}:
3074          match b7:
3075            case True{}:
3076              {==}
3077            case False{}:
3078              {==}