def exp_log_aes.s11011

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

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

3142def exp_log_aes.s11011(+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{}, False{}, True{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, b5, b6, b7})) : U32}:
3143  match b5:
3144    case True{}:
3145      match b6:
3146        case True{}:
3147          match b7:
3148            case True{}:
3149              {==}
3150            case False{}:
3151              {==}
3152        case False{}:
3153          match b7:
3154            case True{}:
3155              {==}
3156            case False{}:
3157              {==}
3158    case False{}:
3159      match b6:
3160        case True{}:
3161          match b7:
3162            case True{}:
3163              {==}
3164            case False{}:
3165              {==}
3166        case False{}:
3167          match b7:
3168            case True{}:
3169              {==}
3170            case False{}:
3171              {==}