def mul_inv_rs.s10100

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

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

4492def mul_inv_rs.s10100(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, b5, b6, b7})))) == 1 : U32}:
4493  match b5:
4494    case True{}:
4495      match b6:
4496        case True{}:
4497          match b7:
4498            case True{}:
4499              {==}
4500            case False{}:
4501              {==}
4502        case False{}:
4503          match b7:
4504            case True{}:
4505              {==}
4506            case False{}:
4507              {==}
4508    case False{}:
4509      match b6:
4510        case True{}:
4511          match b7:
4512            case True{}:
4513              {==}
4514            case False{}:
4515              {==}
4516        case False{}:
4517          match b7:
4518            case True{}:
4519              {==}
4520            case False{}:
4521              {==}