def exp_log_rs.s00010

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

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

6183def exp_log_rs.s00010(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.exp(G.Gf8.rs(), G.Gf8.log(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, b5, b6, b7})) : U32}:
6184  match b5:
6185    case True{}:
6186      match b6:
6187        case True{}:
6188          match b7:
6189            case True{}:
6190              {==}
6191            case False{}:
6192              {==}
6193        case False{}:
6194          match b7:
6195            case True{}:
6196              {==}
6197            case False{}:
6198              {==}
6199    case False{}:
6200      match b6:
6201        case True{}:
6202          match b7:
6203            case True{}:
6204              {==}
6205            case False{}:
6206              {==}
6207        case False{}:
6208          match b7:
6209            case True{}:
6210              {==}
6211            case False{}:
6212              {==}