def exp_log_rs.s01111

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

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

5780def exp_log_rs.s01111(+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{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, b5, b6, b7})) : U32}:
5781  match b5:
5782    case True{}:
5783      match b6:
5784        case True{}:
5785          match b7:
5786            case True{}:
5787              {==}
5788            case False{}:
5789              {==}
5790        case False{}:
5791          match b7:
5792            case True{}:
5793              {==}
5794            case False{}:
5795              {==}
5796    case False{}:
5797      match b6:
5798        case True{}:
5799          match b7:
5800            case True{}:
5801              {==}
5802            case False{}:
5803              {==}
5804        case False{}:
5805          match b7:
5806            case True{}:
5807              {==}
5808            case False{}:
5809              {==}