def exp_log_rs.s11001

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

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

5470def exp_log_rs.s11001(+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{}, False{}, True{}, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, b5, b6, b7})) : U32}:
5471  match b5:
5472    case True{}:
5473      match b6:
5474        case True{}:
5475          match b7:
5476            case True{}:
5477              {==}
5478            case False{}:
5479              {==}
5480        case False{}:
5481          match b7:
5482            case True{}:
5483              {==}
5484            case False{}:
5485              {==}
5486    case False{}:
5487      match b6:
5488        case True{}:
5489          match b7:
5490            case True{}:
5491              {==}
5492            case False{}:
5493              {==}
5494        case False{}:
5495          match b7:
5496            case True{}:
5497              {==}
5498            case False{}:
5499              {==}