def exp_log_rs.s00000

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

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

6245def exp_log_rs.s00000(+b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.exp(G.Gf8.rs(), G.Gf8.log(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, b5, b6, b7})) : U32}:
6246  match b5:
6247    case True{}:
6248      match b6:
6249        case True{}:
6250          match b7:
6251            case True{}:
6252              {==}
6253            case False{}:
6254              {==}
6255        case False{}:
6256          match b7:
6257            case True{}:
6258              {==}
6259            case False{}:
6260              {==}
6261    case False{}:
6262      match b6:
6263        case True{}:
6264          match b7:
6265            case True{}:
6266              {==}
6267            case False{}:
6268              {==}
6269        case False{}:
6270          match b7:
6271            case True{}:
6272              {==}
6273            case False{}:
6274              {==}