def exp_log_rs.s01011

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

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

5904def exp_log_rs.s01011(+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{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, b5, b6, b7})) : U32}:
5905  match b5:
5906    case True{}:
5907      match b6:
5908        case True{}:
5909          match b7:
5910            case True{}:
5911              {==}
5912            case False{}:
5913              {==}
5914        case False{}:
5915          match b7:
5916            case True{}:
5917              {==}
5918            case False{}:
5919              {==}
5920    case False{}:
5921      match b6:
5922        case True{}:
5923          match b7:
5924            case True{}:
5925              {==}
5926            case False{}:
5927              {==}
5928        case False{}:
5929          match b7:
5930            case True{}:
5931              {==}
5932            case False{}:
5933              {==}