def mul_inv_rs.s00110

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

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

4926def mul_inv_rs.s00110(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, b5, b6, b7})))) == 1 : U32}:
4927  match b5:
4928    case True{}:
4929      match b6:
4930        case True{}:
4931          match b7:
4932            case True{}:
4933              {==}
4934            case False{}:
4935              {==}
4936        case False{}:
4937          match b7:
4938            case True{}:
4939              {==}
4940            case False{}:
4941              {==}
4942    case False{}:
4943      match b6:
4944        case True{}:
4945          match b7:
4946            case True{}:
4947              {==}
4948            case False{}:
4949              {==}
4950        case False{}:
4951          match b7:
4952            case True{}:
4953              {==}
4954            case False{}:
4955              {==}