def exp_log_rs.s00001

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

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

6214def exp_log_rs.s00001(+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{}, False{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, b5, b6, b7})) : U32}:
6215  match b5:
6216    case True{}:
6217      match b6:
6218        case True{}:
6219          match b7:
6220            case True{}:
6221              {==}
6222            case False{}:
6223              {==}
6224        case False{}:
6225          match b7:
6226            case True{}:
6227              {==}
6228            case False{}:
6229              {==}
6230    case False{}:
6231      match b6:
6232        case True{}:
6233          match b7:
6234            case True{}:
6235              {==}
6236            case False{}:
6237              {==}
6238        case False{}:
6239          match b7:
6240            case True{}:
6241              {==}
6242            case False{}:
6243              {==}