def exp_log_rs.s10111

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

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

5532def exp_log_rs.s10111(+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{}, True{}, True{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, b5, b6, b7})) : U32}:
5533  match b5:
5534    case True{}:
5535      match b6:
5536        case True{}:
5537          match b7:
5538            case True{}:
5539              {==}
5540            case False{}:
5541              {==}
5542        case False{}:
5543          match b7:
5544            case True{}:
5545              {==}
5546            case False{}:
5547              {==}
5548    case False{}:
5549      match b6:
5550        case True{}:
5551          match b7:
5552            case True{}:
5553              {==}
5554            case False{}:
5555              {==}
5556        case False{}:
5557          match b7:
5558            case True{}:
5559              {==}
5560            case False{}:
5561              {==}