def exp_log_rs.s11111

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

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

5284def exp_log_rs.s11111(+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{}, True{}, True{}, True{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, b5, b6, b7})) : U32}:
5285  match b5:
5286    case True{}:
5287      match b6:
5288        case True{}:
5289          match b7:
5290            case True{}:
5291              {==}
5292            case False{}:
5293              {==}
5294        case False{}:
5295          match b7:
5296            case True{}:
5297              {==}
5298            case False{}:
5299              {==}
5300    case False{}:
5301      match b6:
5302        case True{}:
5303          match b7:
5304            case True{}:
5305              {==}
5306            case False{}:
5307              {==}
5308        case False{}:
5309          match b7:
5310            case True{}:
5311              {==}
5312            case False{}:
5313              {==}