def exp_log_rs.s10000

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

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

5749def exp_log_rs.s10000(+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{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, b5, b6, b7})) : U32}:
5750  match b5:
5751    case True{}:
5752      match b6:
5753        case True{}:
5754          match b7:
5755            case True{}:
5756              {==}
5757            case False{}:
5758              {==}
5759        case False{}:
5760          match b7:
5761            case True{}:
5762              {==}
5763            case False{}:
5764              {==}
5765    case False{}:
5766      match b6:
5767        case True{}:
5768          match b7:
5769            case True{}:
5770              {==}
5771            case False{}:
5772              {==}
5773        case False{}:
5774          match b7:
5775            case True{}:
5776              {==}
5777            case False{}:
5778              {==}