def gc.rs.log

bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:4209

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

4209def gc.rs.log(+a: U32) -> {A.Arrays.nth(U32, gc.rs.llist(), A.Arrays.index(8n, G.Gf8.elt(a)), 0) == U32.from_nat(G.Gf8.log(G.Gf8.rs(), a)) : U32}:
4210  match a:
4211    case U32{WCon{+b0, WCon{+b1, WCon{+b2, WCon{+b3, WCon{+b4, WCon{+b5, WCon{+b6, WCon{+b7, +r}}}}}}}}}:
4212      gc.rs.log.bits(b0, b1, b2, b3, b4, b5, b6, b7)