def mul_inv_rs.s00100

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

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

4988def mul_inv_rs.s00100(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, b5, b6, b7})))) == 1 : U32}:
4989  match b5:
4990    case True{}:
4991      match b6:
4992        case True{}:
4993          match b7:
4994            case True{}:
4995              {==}
4996            case False{}:
4997              {==}
4998        case False{}:
4999          match b7:
5000            case True{}:
5001              {==}
5002            case False{}:
5003              {==}
5004    case False{}:
5005      match b6:
5006        case True{}:
5007          match b7:
5008            case True{}:
5009              {==}
5010            case False{}:
5011              {==}
5012        case False{}:
5013          match b7:
5014            case True{}:
5015              {==}
5016            case False{}:
5017              {==}