def mul_inv_rs.s00101

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

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

4957def mul_inv_rs.s00101(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, b5, b6, b7})))) == 1 : U32}:
4958  match b5:
4959    case True{}:
4960      match b6:
4961        case True{}:
4962          match b7:
4963            case True{}:
4964              {==}
4965            case False{}:
4966              {==}
4967        case False{}:
4968          match b7:
4969            case True{}:
4970              {==}
4971            case False{}:
4972              {==}
4973    case False{}:
4974      match b6:
4975        case True{}:
4976          match b7:
4977            case True{}:
4978              {==}
4979            case False{}:
4980              {==}
4981        case False{}:
4982          match b7:
4983            case True{}:
4984              {==}
4985            case False{}:
4986              {==}