def mul_inv_rs.s10011

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

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

4523def mul_inv_rs.s10011(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, b5, b6, b7})))) == 1 : U32}:
4524  match b5:
4525    case True{}:
4526      match b6:
4527        case True{}:
4528          match b7:
4529            case True{}:
4530              {==}
4531            case False{}:
4532              {==}
4533        case False{}:
4534          match b7:
4535            case True{}:
4536              {==}
4537            case False{}:
4538              {==}
4539    case False{}:
4540      match b6:
4541        case True{}:
4542          match b7:
4543            case True{}:
4544              {==}
4545            case False{}:
4546              {==}
4547        case False{}:
4548          match b7:
4549            case True{}:
4550              {==}
4551            case False{}:
4552              {==}