def exp_log_rs.s00110

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

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

6059def exp_log_rs.s00110(+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{}, True{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, b5, b6, b7})) : U32}:
6060  match b5:
6061    case True{}:
6062      match b6:
6063        case True{}:
6064          match b7:
6065            case True{}:
6066              {==}
6067            case False{}:
6068              {==}
6069        case False{}:
6070          match b7:
6071            case True{}:
6072              {==}
6073            case False{}:
6074              {==}
6075    case False{}:
6076      match b6:
6077        case True{}:
6078          match b7:
6079            case True{}:
6080              {==}
6081            case False{}:
6082              {==}
6083        case False{}:
6084          match b7:
6085            case True{}:
6086              {==}
6087            case False{}:
6088              {==}