def exp_log_aes.s01000

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

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

3731def exp_log_aes.s01000(+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{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, b5, b6, b7})) : U32}:
3732  match b5:
3733    case True{}:
3734      match b6:
3735        case True{}:
3736          match b7:
3737            case True{}:
3738              {==}
3739            case False{}:
3740              {==}
3741        case False{}:
3742          match b7:
3743            case True{}:
3744              {==}
3745            case False{}:
3746              {==}
3747    case False{}:
3748      match b6:
3749        case True{}:
3750          match b7:
3751            case True{}:
3752              {==}
3753            case False{}:
3754              {==}
3755        case False{}:
3756          match b7:
3757            case True{}:
3758              {==}
3759            case False{}:
3760              {==}