def exp_log_rs.s00101

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

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

6090def exp_log_rs.s00101(+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{}, False{}, True{}, False{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, b5, b6, b7})) : U32}:
6091  match b5:
6092    case True{}:
6093      match b6:
6094        case True{}:
6095          match b7:
6096            case True{}:
6097              {==}
6098            case False{}:
6099              {==}
6100        case False{}:
6101          match b7:
6102            case True{}:
6103              {==}
6104            case False{}:
6105              {==}
6106    case False{}:
6107      match b6:
6108        case True{}:
6109          match b7:
6110            case True{}:
6111              {==}
6112            case False{}:
6113              {==}
6114        case False{}:
6115          match b7:
6116            case True{}:
6117              {==}
6118            case False{}:
6119              {==}