def exp_log_rs.s10110

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

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

5563def exp_log_rs.s10110(+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{}, True{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, b5, b6, b7})) : U32}:
5564  match b5:
5565    case True{}:
5566      match b6:
5567        case True{}:
5568          match b7:
5569            case True{}:
5570              {==}
5571            case False{}:
5572              {==}
5573        case False{}:
5574          match b7:
5575            case True{}:
5576              {==}
5577            case False{}:
5578              {==}
5579    case False{}:
5580      match b6:
5581        case True{}:
5582          match b7:
5583            case True{}:
5584              {==}
5585            case False{}:
5586              {==}
5587        case False{}:
5588          match b7:
5589            case True{}:
5590              {==}
5591            case False{}:
5592              {==}