def exp_log_rs.s01010

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

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

5935def exp_log_rs.s01010(+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{}, True{}, False{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, b5, b6, b7})) : U32}:
5936  match b5:
5937    case True{}:
5938      match b6:
5939        case True{}:
5940          match b7:
5941            case True{}:
5942              {==}
5943            case False{}:
5944              {==}
5945        case False{}:
5946          match b7:
5947            case True{}:
5948              {==}
5949            case False{}:
5950              {==}
5951    case False{}:
5952      match b6:
5953        case True{}:
5954          match b7:
5955            case True{}:
5956              {==}
5957            case False{}:
5958              {==}
5959        case False{}:
5960          match b7:
5961            case True{}:
5962              {==}
5963            case False{}:
5964              {==}