def mul_inv_rs.s00001

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

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

5081def mul_inv_rs.s00001(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, b5, b6, b7})))) == 1 : U32}:
5082  match b5:
5083    case True{}:
5084      match b6:
5085        case True{}:
5086          match b7:
5087            case True{}:
5088              {==}
5089            case False{}:
5090              {==}
5091        case False{}:
5092          match b7:
5093            case True{}:
5094              {==}
5095            case False{}:
5096              {==}
5097    case False{}:
5098      match b6:
5099        case True{}:
5100          match b7:
5101            case True{}:
5102              {==}
5103            case False{}:
5104              {==}
5105        case False{}:
5106          match b7:
5107            case True{}:
5108              {==}
5109            case False{}:
5110              {==}