def mul_inv_rs.s00010

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

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

5050def mul_inv_rs.s00010(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, b5, b6, b7})))) == 1 : U32}:
5051  match b5:
5052    case True{}:
5053      match b6:
5054        case True{}:
5055          match b7:
5056            case True{}:
5057              {==}
5058            case False{}:
5059              {==}
5060        case False{}:
5061          match b7:
5062            case True{}:
5063              {==}
5064            case False{}:
5065              {==}
5066    case False{}:
5067      match b6:
5068        case True{}:
5069          match b7:
5070            case True{}:
5071              {==}
5072            case False{}:
5073              {==}
5074        case False{}:
5075          match b7:
5076            case True{}:
5077              {==}
5078            case False{}:
5079              {==}