def exp_log_rs.s11100

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

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

5377def exp_log_rs.s11100(+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{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, b5, b6, b7})) : U32}:
5378  match b5:
5379    case True{}:
5380      match b6:
5381        case True{}:
5382          match b7:
5383            case True{}:
5384              {==}
5385            case False{}:
5386              {==}
5387        case False{}:
5388          match b7:
5389            case True{}:
5390              {==}
5391            case False{}:
5392              {==}
5393    case False{}:
5394      match b6:
5395        case True{}:
5396          match b7:
5397            case True{}:
5398              {==}
5399            case False{}:
5400              {==}
5401        case False{}:
5402          match b7:
5403            case True{}:
5404              {==}
5405            case False{}:
5406              {==}