def mul_inv_rs.s10010

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

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

4554def mul_inv_rs.s10010(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, b5, b6, b7})))) == 1 : U32}:
4555  match b5:
4556    case True{}:
4557      match b6:
4558        case True{}:
4559          match b7:
4560            case True{}:
4561              {==}
4562            case False{}:
4563              {==}
4564        case False{}:
4565          match b7:
4566            case True{}:
4567              {==}
4568            case False{}:
4569              {==}
4570    case False{}:
4571      match b6:
4572        case True{}:
4573          match b7:
4574            case True{}:
4575              {==}
4576            case False{}:
4577              {==}
4578        case False{}:
4579          match b7:
4580            case True{}:
4581              {==}
4582            case False{}:
4583              {==}