def exp_log_rs.s11101

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

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

5346def exp_log_rs.s11101(+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{}, True{}, False{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, b5, b6, b7})) : U32}:
5347  match b5:
5348    case True{}:
5349      match b6:
5350        case True{}:
5351          match b7:
5352            case True{}:
5353              {==}
5354            case False{}:
5355              {==}
5356        case False{}:
5357          match b7:
5358            case True{}:
5359              {==}
5360            case False{}:
5361              {==}
5362    case False{}:
5363      match b6:
5364        case True{}:
5365          match b7:
5366            case True{}:
5367              {==}
5368            case False{}:
5369              {==}
5370        case False{}:
5371          match b7:
5372            case True{}:
5373              {==}
5374            case False{}:
5375              {==}