def mul_inv_rs.s11101

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

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

4213def mul_inv_rs.s11101(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, b5, b6, b7})))) == 1 : U32}:
4214  match b5:
4215    case True{}:
4216      match b6:
4217        case True{}:
4218          match b7:
4219            case True{}:
4220              {==}
4221            case False{}:
4222              {==}
4223        case False{}:
4224          match b7:
4225            case True{}:
4226              {==}
4227            case False{}:
4228              {==}
4229    case False{}:
4230      match b6:
4231        case True{}:
4232          match b7:
4233            case True{}:
4234              {==}
4235            case False{}:
4236              {==}
4237        case False{}:
4238          match b7:
4239            case True{}:
4240              {==}
4241            case False{}:
4242              {==}