def mul_inv_rs.s01001

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

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

4833def mul_inv_rs.s01001(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, b5, b6, b7})))) == 1 : U32}:
4834  match b5:
4835    case True{}:
4836      match b6:
4837        case True{}:
4838          match b7:
4839            case True{}:
4840              {==}
4841            case False{}:
4842              {==}
4843        case False{}:
4844          match b7:
4845            case True{}:
4846              {==}
4847            case False{}:
4848              {==}
4849    case False{}:
4850      match b6:
4851        case True{}:
4852          match b7:
4853            case True{}:
4854              {==}
4855            case False{}:
4856              {==}
4857        case False{}:
4858          match b7:
4859            case True{}:
4860              {==}
4861            case False{}:
4862              {==}