def exp_log_rs.s11010

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

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

5439def exp_log_rs.s11010(+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{}, False{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, b5, b6, b7})) : U32}:
5440  match b5:
5441    case True{}:
5442      match b6:
5443        case True{}:
5444          match b7:
5445            case True{}:
5446              {==}
5447            case False{}:
5448              {==}
5449        case False{}:
5450          match b7:
5451            case True{}:
5452              {==}
5453            case False{}:
5454              {==}
5455    case False{}:
5456      match b6:
5457        case True{}:
5458          match b7:
5459            case True{}:
5460              {==}
5461            case False{}:
5462              {==}
5463        case False{}:
5464          match b7:
5465            case True{}:
5466              {==}
5467            case False{}:
5468              {==}