def mul_inv_rs.s01000

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

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

4864def mul_inv_rs.s01000(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, b5, b6, b7})))) == 1 : U32}:
4865  match b5:
4866    case True{}:
4867      match b6:
4868        case True{}:
4869          match b7:
4870            case True{}:
4871              {==}
4872            case False{}:
4873              {==}
4874        case False{}:
4875          match b7:
4876            case True{}:
4877              {==}
4878            case False{}:
4879              {==}
4880    case False{}:
4881      match b6:
4882        case True{}:
4883          match b7:
4884            case True{}:
4885              {==}
4886            case False{}:
4887              {==}
4888        case False{}:
4889          match b7:
4890            case True{}:
4891              {==}
4892            case False{}:
4893              {==}