def exp_log_rs.s10100

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

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

5625def exp_log_rs.s10100(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.exp(G.Gf8.rs(), G.Gf8.log(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, b5, b6, b7})) : U32}:
5626  match b5:
5627    case True{}:
5628      match b6:
5629        case True{}:
5630          match b7:
5631            case True{}:
5632              {==}
5633            case False{}:
5634              {==}
5635        case False{}:
5636          match b7:
5637            case True{}:
5638              {==}
5639            case False{}:
5640              {==}
5641    case False{}:
5642      match b6:
5643        case True{}:
5644          match b7:
5645            case True{}:
5646              {==}
5647            case False{}:
5648              {==}
5649        case False{}:
5650          match b7:
5651            case True{}:
5652              {==}
5653            case False{}:
5654              {==}