def exp_log_rs.s10101

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

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

5594def exp_log_rs.s10101(+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{}, False{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, b5, b6, b7})) : U32}:
5595  match b5:
5596    case True{}:
5597      match b6:
5598        case True{}:
5599          match b7:
5600            case True{}:
5601              {==}
5602            case False{}:
5603              {==}
5604        case False{}:
5605          match b7:
5606            case True{}:
5607              {==}
5608            case False{}:
5609              {==}
5610    case False{}:
5611      match b6:
5612        case True{}:
5613          match b7:
5614            case True{}:
5615              {==}
5616            case False{}:
5617              {==}
5618        case False{}:
5619          match b7:
5620            case True{}:
5621              {==}
5622            case False{}:
5623              {==}