def exp_log_aes.s00001

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

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

3948def exp_log_aes.s00001(+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{}, False{}, False{}, False{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, b5, b6, b7})) : U32}:
3949  match b5:
3950    case True{}:
3951      match b6:
3952        case True{}:
3953          match b7:
3954            case True{}:
3955              {==}
3956            case False{}:
3957              {==}
3958        case False{}:
3959          match b7:
3960            case True{}:
3961              {==}
3962            case False{}:
3963              {==}
3964    case False{}:
3965      match b6:
3966        case True{}:
3967          match b7:
3968            case True{}:
3969              {==}
3970            case False{}:
3971              {==}
3972        case False{}:
3973          match b7:
3974            case True{}:
3975              {==}
3976            case False{}:
3977              {==}