def exp_log_rs.s10011

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

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

5656def exp_log_rs.s10011(+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{}, False{}, True{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, b5, b6, b7})) : U32}:
5657  match b5:
5658    case True{}:
5659      match b6:
5660        case True{}:
5661          match b7:
5662            case True{}:
5663              {==}
5664            case False{}:
5665              {==}
5666        case False{}:
5667          match b7:
5668            case True{}:
5669              {==}
5670            case False{}:
5671              {==}
5672    case False{}:
5673      match b6:
5674        case True{}:
5675          match b7:
5676            case True{}:
5677              {==}
5678            case False{}:
5679              {==}
5680        case False{}:
5681          match b7:
5682            case True{}:
5683              {==}
5684            case False{}:
5685              {==}