def exp_log_aes.s01010

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

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

3669def exp_log_aes.s01010(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.exp(G.Gf8.aes(), G.Gf8.log(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, b5, b6, b7})) : U32}:
3670  match b5:
3671    case True{}:
3672      match b6:
3673        case True{}:
3674          match b7:
3675            case True{}:
3676              {==}
3677            case False{}:
3678              {==}
3679        case False{}:
3680          match b7:
3681            case True{}:
3682              {==}
3683            case False{}:
3684              {==}
3685    case False{}:
3686      match b6:
3687        case True{}:
3688          match b7:
3689            case True{}:
3690              {==}
3691            case False{}:
3692              {==}
3693        case False{}:
3694          match b7:
3695            case True{}:
3696              {==}
3697            case False{}:
3698              {==}