def exp_log_rs.s01001

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

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

5966def exp_log_rs.s01001(+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{}, False{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, b5, b6, b7})) : U32}:
5967  match b5:
5968    case True{}:
5969      match b6:
5970        case True{}:
5971          match b7:
5972            case True{}:
5973              {==}
5974            case False{}:
5975              {==}
5976        case False{}:
5977          match b7:
5978            case True{}:
5979              {==}
5980            case False{}:
5981              {==}
5982    case False{}:
5983      match b6:
5984        case True{}:
5985          match b7:
5986            case True{}:
5987              {==}
5988            case False{}:
5989              {==}
5990        case False{}:
5991          match b7:
5992            case True{}:
5993              {==}
5994            case False{}:
5995              {==}