def mul_inv_rs.s10000

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

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

4616def mul_inv_rs.s10000(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, b5, b6, b7})))) == 1 : U32}:
4617  match b5:
4618    case True{}:
4619      match b6:
4620        case True{}:
4621          match b7:
4622            case True{}:
4623              {==}
4624            case False{}:
4625              {==}
4626        case False{}:
4627          match b7:
4628            case True{}:
4629              {==}
4630            case False{}:
4631              {==}
4632    case False{}:
4633      match b6:
4634        case True{}:
4635          match b7:
4636            case True{}:
4637              {==}
4638            case False{}:
4639              {==}
4640        case False{}:
4641          match b7:
4642            case True{}:
4643              {==}
4644            case False{}:
4645              {==}