def exp_log_rs.s11011

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

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

5408def exp_log_rs.s11011(+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{}, True{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, b5, b6, b7})) : U32}:
5409  match b5:
5410    case True{}:
5411      match b6:
5412        case True{}:
5413          match b7:
5414            case True{}:
5415              {==}
5416            case False{}:
5417              {==}
5418        case False{}:
5419          match b7:
5420            case True{}:
5421              {==}
5422            case False{}:
5423              {==}
5424    case False{}:
5425      match b6:
5426        case True{}:
5427          match b7:
5428            case True{}:
5429              {==}
5430            case False{}:
5431              {==}
5432        case False{}:
5433          match b7:
5434            case True{}:
5435              {==}
5436            case False{}:
5437              {==}