def exp_log_rs.s00100

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

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

6121def exp_log_rs.s00100(+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{}, True{}, False{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, b5, b6, b7})) : U32}:
6122  match b5:
6123    case True{}:
6124      match b6:
6125        case True{}:
6126          match b7:
6127            case True{}:
6128              {==}
6129            case False{}:
6130              {==}
6131        case False{}:
6132          match b7:
6133            case True{}:
6134              {==}
6135            case False{}:
6136              {==}
6137    case False{}:
6138      match b6:
6139        case True{}:
6140          match b7:
6141            case True{}:
6142              {==}
6143            case False{}:
6144              {==}
6145        case False{}:
6146          match b7:
6147            case True{}:
6148              {==}
6149            case False{}:
6150              {==}