def exp_log_rs.core
bend-osdev-gf@0.1.1.0 · PROOF.bend:6403
import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
6403def exp_log_rs.core(+a: U32) -> {G.Gf8.exp(G.Gf8.rs(), G.Gf8.log(G.Gf8.rs(), fixz(G.Gf8.elt(a)))) == fixz(G.Gf8.elt(a)) : U32}:
6404 match a:
6405 case U32{WCon{+b0, WCon{+b1, WCon{+b2, WCon{+b3, WCon{+b4, WCon{+b5, WCon{+b6, WCon{+b7, +r}}}}}}}}}:
6406 %Equal.sym(U32, G.Gf8.elt(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, r}}}}}}}}}), G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}), elt_bits(b0, b1, b2, b3, b4, b5, b6, b7, r)) : {G.Gf8.exp(G.Gf8.rs(), G.Gf8.log(G.Gf8.rs(), fixz(_))) == fixz(_) : U32}
6407 exp_log_rs.bits(b0, b1, b2, b3, b4, b5, b6, b7)