def mul_inv_rs.s01010

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

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

4802def mul_inv_rs.s01010(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, b5, b6, b7})))) == 1 : U32}:
4803  match b5:
4804    case True{}:
4805      match b6:
4806        case True{}:
4807          match b7:
4808            case True{}:
4809              {==}
4810            case False{}:
4811              {==}
4812        case False{}:
4813          match b7:
4814            case True{}:
4815              {==}
4816            case False{}:
4817              {==}
4818    case False{}:
4819      match b6:
4820        case True{}:
4821          match b7:
4822            case True{}:
4823              {==}
4824            case False{}:
4825              {==}
4826        case False{}:
4827          match b7:
4828            case True{}:
4829              {==}
4830            case False{}:
4831              {==}