def exp_log_rs.s11000

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

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

5501def exp_log_rs.s11000(+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{}, False{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, b5, b6, b7})) : U32}:
5502  match b5:
5503    case True{}:
5504      match b6:
5505        case True{}:
5506          match b7:
5507            case True{}:
5508              {==}
5509            case False{}:
5510              {==}
5511        case False{}:
5512          match b7:
5513            case True{}:
5514              {==}
5515            case False{}:
5516              {==}
5517    case False{}:
5518      match b6:
5519        case True{}:
5520          match b7:
5521            case True{}:
5522              {==}
5523            case False{}:
5524              {==}
5525        case False{}:
5526          match b7:
5527            case True{}:
5528              {==}
5529            case False{}:
5530              {==}