def exp_log_rs.s01110

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

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

5811def exp_log_rs.s01110(+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{}, True{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, b5, b6, b7})) : U32}:
5812  match b5:
5813    case True{}:
5814      match b6:
5815        case True{}:
5816          match b7:
5817            case True{}:
5818              {==}
5819            case False{}:
5820              {==}
5821        case False{}:
5822          match b7:
5823            case True{}:
5824              {==}
5825            case False{}:
5826              {==}
5827    case False{}:
5828      match b6:
5829        case True{}:
5830          match b7:
5831            case True{}:
5832              {==}
5833            case False{}:
5834              {==}
5835        case False{}:
5836          match b7:
5837            case True{}:
5838              {==}
5839            case False{}:
5840              {==}