def exp_log_rs.s10001

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

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

5718def exp_log_rs.s10001(+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{}, False{}, False{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, b5, b6, b7})) : U32}:
5719  match b5:
5720    case True{}:
5721      match b6:
5722        case True{}:
5723          match b7:
5724            case True{}:
5725              {==}
5726            case False{}:
5727              {==}
5728        case False{}:
5729          match b7:
5730            case True{}:
5731              {==}
5732            case False{}:
5733              {==}
5734    case False{}:
5735      match b6:
5736        case True{}:
5737          match b7:
5738            case True{}:
5739              {==}
5740            case False{}:
5741              {==}
5742        case False{}:
5743          match b7:
5744            case True{}:
5745              {==}
5746            case False{}:
5747              {==}