def exp_log_aes.s11101

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

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

3080def exp_log_aes.s11101(+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{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, b5, b6, b7})) : U32}:
3081  match b5:
3082    case True{}:
3083      match b6:
3084        case True{}:
3085          match b7:
3086            case True{}:
3087              {==}
3088            case False{}:
3089              {==}
3090        case False{}:
3091          match b7:
3092            case True{}:
3093              {==}
3094            case False{}:
3095              {==}
3096    case False{}:
3097      match b6:
3098        case True{}:
3099          match b7:
3100            case True{}:
3101              {==}
3102            case False{}:
3103              {==}
3104        case False{}:
3105          match b7:
3106            case True{}:
3107              {==}
3108            case False{}:
3109              {==}