def mul_inv_rs.s00111

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

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

4895def mul_inv_rs.s00111(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, b5, b6, b7})))) == 1 : U32}:
4896  match b5:
4897    case True{}:
4898      match b6:
4899        case True{}:
4900          match b7:
4901            case True{}:
4902              {==}
4903            case False{}:
4904              {==}
4905        case False{}:
4906          match b7:
4907            case True{}:
4908              {==}
4909            case False{}:
4910              {==}
4911    case False{}:
4912      match b6:
4913        case True{}:
4914          match b7:
4915            case True{}:
4916              {==}
4917            case False{}:
4918              {==}
4919        case False{}:
4920          match b7:
4921            case True{}:
4922              {==}
4923            case False{}:
4924              {==}