def exp_log_rs.s11110

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

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

5315def exp_log_rs.s11110(+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{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, b5, b6, b7})) : U32}:
5316  match b5:
5317    case True{}:
5318      match b6:
5319        case True{}:
5320          match b7:
5321            case True{}:
5322              {==}
5323            case False{}:
5324              {==}
5325        case False{}:
5326          match b7:
5327            case True{}:
5328              {==}
5329            case False{}:
5330              {==}
5331    case False{}:
5332      match b6:
5333        case True{}:
5334          match b7:
5335            case True{}:
5336              {==}
5337            case False{}:
5338              {==}
5339        case False{}:
5340          match b7:
5341            case True{}:
5342              {==}
5343            case False{}:
5344              {==}