def exp_log_rs.s01100

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

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

5873def exp_log_rs.s01100(+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{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, b5, b6, b7})) : U32}:
5874  match b5:
5875    case True{}:
5876      match b6:
5877        case True{}:
5878          match b7:
5879            case True{}:
5880              {==}
5881            case False{}:
5882              {==}
5883        case False{}:
5884          match b7:
5885            case True{}:
5886              {==}
5887            case False{}:
5888              {==}
5889    case False{}:
5890      match b6:
5891        case True{}:
5892          match b7:
5893            case True{}:
5894              {==}
5895            case False{}:
5896              {==}
5897        case False{}:
5898          match b7:
5899            case True{}:
5900              {==}
5901            case False{}:
5902              {==}