def exp_log_aes.s11111

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

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

3018def exp_log_aes.s11111(+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{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, b5, b6, b7})) : U32}:
3019  match b5:
3020    case True{}:
3021      match b6:
3022        case True{}:
3023          match b7:
3024            case True{}:
3025              {==}
3026            case False{}:
3027              {==}
3028        case False{}:
3029          match b7:
3030            case True{}:
3031              {==}
3032            case False{}:
3033              {==}
3034    case False{}:
3035      match b6:
3036        case True{}:
3037          match b7:
3038            case True{}:
3039              {==}
3040            case False{}:
3041              {==}
3042        case False{}:
3043          match b7:
3044            case True{}:
3045              {==}
3046            case False{}:
3047              {==}